|->SUPPORTEDOverlapping implication
When the antecedent matches, start the consequent on the same cycle.
req |-> ackTHE ENGINEER'S FIELD GUIDE
A language for behavior.
Your quick reference to the AssertionQuest educational SVA subset.
&&SUPPORTEDLogical AND
Both Boolean conditions must be true.
req && !busy!SUPPORTEDNegation
Invert a Boolean condition.
!busy||SUPPORTEDLogical OR
At least one condition must be true.
a || b==SUPPORTEDEquality
Compare the sampled Boolean values.
b == $past(a)!=SUPPORTEDInequality
The two Boolean values must differ.
a != b##NSUPPORTEDCycle delay
Move exactly N sampled cycles forward.
req |-> ##2 ack|=>SUPPORTEDNon-overlapping implication
Start the consequent one cycle after the antecedent.
req |=> ack$past()SUPPORTEDPast value
Read a signal from an earlier sample; default history is one cycle.
b == $past(a, 2)$rose()SUPPORTEDRising edge
Detect a sampled transition from zero to one.
$rose(req) |-> ack$fell()SUPPORTEDFalling edge
Detect a sampled transition from one to zero.
$fell(req) |-> ack$stable()SUPPORTEDStable value
True when a signal equals its previous sampled value.
busy |-> $stable(data)##[N:M]SUPPORTEDDelay range
Match at any endpoint within an inclusive cycle window.
req |-> ##[1:3] ack[*N]FUTUREConsecutive repetition
Future extension: repeat a sequence.
a[*3]throughoutFUTUREThroughout
Future extension: hold a condition across a sequence.
a throughout b[*3]untilFUTUREUntil
Future extension: hold a condition until another occurs.
a until buntil_withFUTUREUntil with
Future extension: an inclusive until condition.
a until_with bHow this lab interprets time
All values are sampled at the rising edge of an implicit clock. Properties are checked at every cycle. An implication passes vacuously when its antecedent never triggers.
$past(x,N) returns zero when history is missing. At cycle zero, $rose, $fell and $stable return false. A delay range succeeds if any permitted endpoint satisfies the sequence.
An obligation with no successful endpoint before the trace ends fails. Studio rejects reference tests with unresolved obligations; pad the trace and remove late triggers. Matching an available endpoint in a range succeeds even if later endpoints extend beyond the trace.
Boolean expressions support 0 1 ! && || == != and nested parentheses. One optional Boolean antecedent may precede |-> or |=>. Consequents can chain Boolean expressions with fixed or ranged delays. Temporal sequences inside parentheses, nested implications, repetition, reset disabling, and full IEEE SVA are not implemented. Enter the body only.
Limits: 2,000 characters, 256 tokens, 32 levels of expression nesting, 128 cycles, 16 binary signals. Knowing an operator early is welcome—toolbox locks never restrict valid syntax.