SVA Table

Note

Sampled value functions (except for some global clocking future sampled value functions), triggered, matched, and local variables need to be handled outside of Property IR. Some of these features might be added in later revisions.

Declarations

concept	SVA keyword	Property IR statement		SV Standard
declaring sequences	sequence … endsequence	declare		16.8 Declaring sequences (p. 402)
declaring properties	property … endproperty			16.12 Declaring properties (p. 439)
recursive properties	property … endproperty	declare-rec		16.12.17 Recursive properties (p. 459)

Assertions

concept	SVA statement	Property IR statement	SV Standard
assert	assert	assert-property	16.14.1 Assert statement (p. 476)
assume	assume	assume-property	16.14.2 Assume statement (p. 477)
cover	cover	cover-property	16.14.3 Cover statement (p. 479)
	cover	cover-sequence
restrict	restrict	restrict-property	16.14.4 Restrict statement (p. 480)
disable condition	disable iff	assertion statement parameter :disable-iff	16.12 Declaring properties (p. 441) 16.14.6.4 Disabling procedural concurrent assertions (p. 487)
enabling condition	always @(clk_expr) begin	assertion statement parameter :enable pir_clk_expr	16.14.6 Embedding concurrent assertions in procedural code (p. 481) F.5.3.1 Neutral satisfaction (p. 1247)
	always @(clk_expr) begin if (bool) begin	:enable (and pir_clk_expr bool)
vacuity	assertion control system tasks $assertnonvacuouson $assertnonvacuousoff	assertion statement parameter :mode satisfied nonvacuously-satisfied nonvacuous	16.14.8 Nonvacuous evaluations 20.11 Assertion control system tasks F.5.3.3 Vacuity
output sequence matches		trigger-sequence

Note

The enable condition depends on the specific location of the assertion in procedural code. We gave two common examples. The Property IR clock expression pir_clk_expr is obtained as described in the table Clock Control below.

When embedding a concurrent assertion in procedural code, the inferred clock needs to be set explicitly in the property using clk-prop-clocked, regardless of whether an enabling condition is specified.

Clock Control

The Property IR primitives in this table have return type bool.

concept	SVA operation	Property IR primitive	SV Standard
global clock	@($global_clock)	(constant true)	9.4.2 Event control (p. 232) 16.9.4 Global clocking past and future sampled value functions (p. 418) F.3.1 Clock control (p. 1235) F.3.4.4 Derived sampled value functions (p. 1240)
rising edge	@(posedge clk)	rising-gclk
falling edge	@(negedge clk)	falling-gclk
any edge	@(edge clk)	(or (rising-gclk clk clk_def) (falling-gclk clk clk_def)
changing clock (clk not global clock)	@(clk)	changing-gclk
conditional clock	@(clk_expr iff bool)	(and pir_clk_expr bool)	9.4.2.3 Conditional event controls (p.235)
clock disjunction	@(clk_expr1 or clk_expr2) @(clk_expr1, clk_expr2)	(or pir_clk_expr1 pir_clk_expr2)	9.4.2.1 Event OR operator (p. 232)

Note

The corresponding Property IR clock expressions pir_clk_expr etc. in conditional clock and clock disjunction need to use the correct primitives necessary for the SVA clock expressions clk_expr etc. For example, @(posedge clk iff bool) corresponds to (and (rising-gclk clk clk_def) bool). Also take note of the details on the global clocking future sampled value functions.

Boolean Operations

concept	SVA operation	Property IR primitive	SV Standard
logical not	!	not	11.4.7 Logical operators (p. 280)
logical and	&&	and
logical or	||	or
true	1'b1	(constant true) (true)
false	1'b0	(constant false) (false)
logical equality	==	eq	11.4.5 Equality operators (p. 279)
logical inequality	!=	xor
true in initial cycle		initial

Sequence Operations

concept	SVA operation	Property IR primitive	SV Standard
sequence clock	@(c)	clk-seq-clocked	14. Clocking blocks (p. 354) 16.13.3 Clock flow (p. 468) 16.16 Clock resolution (p. 495) F.3.1 Clock control (p. 1235)
delay	##m ##[m:n] ##[m:$]	clk-seq-delay	16.7 Sequences (p. 399–401)
concatenation	##1	clk-seq-concat
fusion	##0	clk-seq-fusion
consecutive repetition	[*m] [*m:n] [*n:$]	clk-seq-repeat	16.9.2 Repetition in sequences (p. 410)
goto repetition	[->m] [->m:n] [->m:$]	clk-seq-goto-repeat
nonconsecutive repetition	[=m] [=m:n] [->m:$]	clk-seq-nonconsecutive-repeat
and	and	clk-seq-and	16.9.5 AND operation (p. 421)
intersection	intersect	clk-seq-intersect	16.9.6 Intersection (AND with length restriction) (p. 423)
or	or	clk-seq-or	16.9.7 OR operation (p. 424)
first match	first_match	clk-seq-first-match	16.9.8 First_match operation (p. 427)
throughout	throughout	clk-seq-throughout	16.9.9 Conditions over sequences (p. 428)
within	within	clk-seq-within	16.9.10 Sequence contained within another sequence (p. 430)
sequence of length 1		clk-seq-bool
simple sequence to globally clocked sequence		clk-seq-seq

Property Operations

concept	SVA operation	Property IR primitive			SV Standard
property clock	@(c)	clk-prop-clocked			14. Clocking blocks (p. 354) 16.13.3 Clock flow (p. 468) 16.16 Clock resolution (p. 495) F.3.1 Clock control (p. 1235)
sequence properties	strong	clk-prop-strong clk-prop-strong-bool			16.12.2 Sequence property (p. 443) 16.12.15 Weak and strong operators (p. 458)
	weak	clk-prop-weak clk-prop-weak-bool
		clk-prop-seq clk-prop-bool
negation	not	clk-prop-not			16.12.3 Negation property (p. 444)
disjunction	or	clk-prop-or			16.12.4 Disjunction property (p. 444)
conjunction	and	clk-prop-and			16.12.5 Conjunction property (p. 444)
if-else and case	if	clk-prop-if			16.12.6 If-else property (p. 444) 16.12.16 Case (p. 458)
	if … else case … endcase	clk-prop-if-else
implication	|->	clk-prop-overlapped-implication			16.12.7 Implication (p. 445)
	|=>	clk-prop-non-overlapped-implication
implies	implies	clk-prop-implies			16.12.9 Implies and iff properties (p. 449)
iff	iff	clk-prop-iff
followed-by	#-#	clk-prop-overlapped-followed-by			16.12.9 Followed-by property (p. 449)
	#=#	clk-prop-non-overlapped-followed-by
nexttime	nexttime nexttime[m]	clk-prop-nexttime			16.12.10 Nexttime property (p.450)
	s_nexttime s_nexttime[m]	clk-prop-strong-nexttime
always	always	clk-prop-always			16.12.11 Always property (p. 452)
	always[m:n] always[m:$]	clk-prop-always-ranged
	s_always[m:n]	clk-prop-strong-always
until	until	clk-prop-until			16.12.12 Until property (p. 453)
	s_until	clk-prop-strong-until
	until_with	clk-prop-until-with
	s_until_with	clk-prop-strong-until
eventually	eventually[m:n]	clk-prop-eventually			16.12.13 Eventually property (p. 454)
	s_eventually	clk-prop-strong-eventually
	s_eventually[m:n] s_eventually[m:$]	clk-prop-strong-eventually-ranged
abort properties	accept_on	clk-prop-accept-on			16.12.14 Abort properties (p. 465)
	reject_on	clk-prop-reject-on
	sync_accept_on	clk-prop-sync-accept-on
	sync_reject_on	clk-prop-sync-reject-on
simple property to globally clocked property		clk-prop-prop