Assertion objective : check that a signal will only be de-asserted for only one clk cycle when a specific condition occurs i.e. hready_cpu signal shall be de-asserted when read_trans and wr_trans occurs at the same time where read_trans is a declared sequence and wr_trans is a flag
I got the following error :
Expected a sequence expression as an operand to the sequence implication ‘|=>’ operator !
When i removed “|-> `true” it worked correctly ! but i couldn’t figure out what is the error in the assertion
In reply to aehsan:
Just looking at the syntax, 1800 defines what a property is, and one of the property expressions is:
property_expr ::=
sequence_expr |-> property_expr
From that, you deduce that the following is also legal:
sequence_expr |->
sequence_expr |-> property_expr
You have:
$fell(hready_cpu) |-> // sequence
(read_trans and (wr_trans |-> `true)) // ANDing of 2 properties
|=> $rose(hready_cpu)) // another property (followed by |=> )
That is a violation of the definition of a property
property |=> property // IS NOT a property expression
If the first part didn’t occur ( i.e. sequence_expr1 happened but sequence_expr2 didn’t occur ). If the first |-> failed, shall the entire property fail ?
In reply to ben@SystemVerilog.us:
I’d like to ask about the following scenario :
sequence_expr1 |->
sequence_expr2 |-> property_expr
If the first part didn’t occur ( i.e. sequence_expr1 happened but sequence_expr2 didn’t occur ). If the first |-> failed, shall the entire property fail ?
Since the consequent is a property expression, and that can be a sequence or another property with the implication operator, the following can also be expressed for a property:
sequence_expr |-> sequence_expr |-> property_expr
----- property ----------------
sequence_expr |-> sequence_expr |-> sequence_expr |-> property_expr
----- property ----------------
----------------------------property ----------------
sequence_expr1 |-> sequence_expr2 |-> property_expr
Consider the following cases and the results
1'b1 |-> 1'b0 |-> whatever_property // Result is vacuous because the
// antecedent of the whatever_property is no match (a zero).
1'b0 |-> whatever_seq |-> whatever // Result is vacuous because the antecedent is no match.
1'b1 |-> 1'b1 |-> 1'b0 // fail, failed property
1'b1 |-> 1'b1 |-> 1'b1 // PASS
Note: By 1'b0 or 1'b1, I mean the pass or fail of a sequence. For simplicity,
I am using a sequence of 1 term.
Be careful of multi-threaded antecedents! I explained the following from my book:> An assertion with a multi-threaded sequence is processed differently if that sequence is used as an antecedent rather than a consequent of the property. …
An assertion started with a multi-threaded sequence has the following criteria for its outcome:
All threads must be exercised in search of a matched antecedent /consequent pair, unless the assertion fails. In that case, the search is short-circuited (i.e., stopped).
The assertion is considered failed if there is a matched antecedent with a failed consequent.
For the assertion to be successful, two requirements must be met:
There must be no failure in the search of a matched antecedent with a consequent.
All threads of the antecedent and consequent must be successful. There are two types of successes: vacuous and nonvacuous.
a. VACUOUS SUCCESS:
i. If all the threads of the antecedent result in a no match, then the assertion is considered vacuously true (also referred to as vacuous success, or simply vacuous).
ii. Vacuity can also occur if a thread has a matched (i.e., true) antecedent but its consequent is vacuous (see 3.9 for discussion of vacuous properties).
b. PASS / NON-VACUOUS: For a nonvacuous pass (or success), there must be at least one matched antecedent with its successful nonvacuous property, which represents the consequent. There must also be no failures in the consequent. Some threads may however be vacuous.
For sequence_expr1 |-> sequence_expr2 |-> property_expr
If sequence_expr1 is multi-threaded, you may need a first_match(sequence_expr1)
If sequence_expr2 is multi-threaded, you may need a first_match(sequence_expr2)
If property_expr is a sequence with multi-threads, you do NOT need a first_match() as the property would succeed upon a match.
This rule is important because unexpected result may occur. This is also particularly true when multiple threads update a common local variable as each thread carries its own set of local variables. Those issues are explained, with examples, in Section 2.7.9.
The first_match() DOES NOT NECESSARILY GUARANTEE EXCLUSIVITY IN FIRST MATCHES