I initially used the following property for asserting state-transitions of the FSM under normal operations
// Checking state transitions under normal operations
int state;
assign state = fsm_state;
property prop_fsm_normal_operation;
disable iff (!reset_n)
@(posedge clk) (state == FSM_SAMPLE) [*1:$] |=>
(state == FSM_STREAM) [*1:$] |=>
(state == FSM_WAIT) [*1:$] |=>
(state == FSM_IDLE);
endproperty
// Assert property
assert_FSM_normal_operation: assert property (
prop_fsm_normal_operation
);
I have a simple FSM where it follows one path in a sequential manner.
This is not working as i expected. I am getting an assertion failure. I had a look at the waveforms of where this assertion failed and it made no sense to me. All these transitions were followed in the right manner.
I played around with the antecedents and consequent ordering and the following configuration worked
property prop_fsm_normal_operation;
disable iff (!reset_n)
@(posedge clk) (state == FSM_SAMPLE) [*1:] |=>
(state == FSM_STREAM) [*1:] ##1
(state == FSM_WAIT) [*1:$] ##1
(state == FSM_IDLE);
endproperty
There is some knowledge I am possibly lacking. Help will be appreciated to understand why this is the case
In reply to ak180:
There are several concepts that seem to have missed, and you should have been taught those when you studied SVA. I strongly recommend that you thoughroughly read my paper
Delay range: A delay range, such as ##[n:m], indicates that the delay between the first sequence and the next ranges from nth cycle up to either a maximum mth cycles. For example, the sequence (a ##[3:4] b ##1 c) is equivalent to the sequence ((a ##3 b ##1 c) or (a ##4 b ##1 c)). This example represents two sequence threads, and thus multiple possible matches are possible (2 in this case because the range is 2) .
Range delays in the antecedent
Consider the following property: $rose(a) ##[1:5] b |-> ##3 c;
It states that at each end point of the sequence ($rose(a) ##[1:5] b) the variable “c” will be true three cycles later.
The issue that arises with many users is that the antecedent is multithreaded, and that can causes unanticipated errors. SVA requires that each of the threads of that antecedent with a range or a repeat statement, must be tested with its appropriate consequent
Specifically, the property rose(a) ##[1:] b |-> ##3 c; is equivalent to ($rose(a) ##[1] b) or ($rose(a) ##[2] b) or …(rose(a) ##[] b) |-> ##3 c; // where $ is infinity
This ORing in the antecedent creates multiple threads, something like:
($rose(a) ##[1] b |-> ##3 c) and // separate thread
($rose(a) ##[2] b |-> ##3 c) and // separate thread
…
(rose(a) ##[] b |-> ##3 c);//
This property can never succeed because for success ALL THREADS OF THE ANTECEDENT MUST BE TEST. Property CAN FAIL TOUGH!
Note: Any non-matched thread of the antecedent (when b==0) creates a vacuously true property result for that thread, meaning that though TRUE, it is of no significance. However, any failure of one of those property threads (Antecedent through consequent) causes the assertion to fail. That would occur if one of the treads of the antecedent is a match and its corresponding consequent is not a match (when c==0). For the property to success, there can be no property failure (vacuity is considered a vacuous true), and at least one thread of the antecedent matches along with a match of its corresponding consequent.
Ranges in repeats have the “or”: Same principles apply to the repeats on ranges. a[1:$] is equivalent to*a{*1] or a[2] or … a[n].
Attempt: At every clocking event there is an attempt. With
*@(posedge clk) (state == FSM_SAMPLE) [1:$] |=>
you are creating at every clocking event an unnecessary infinite number of “or” threads.
Use of multiple properties each with an antecedent: Do you realize that each non matched antecedent causes that property to be vacuous?
Please correct me if I have not understood correctly.
Let’s break the first line down:
(state == FSM_SAMPLE) [*1:] |=> (state == FSM_STREAM) [*1:]
So because of the unspecified range, we can say that the antecedent will spawn an arbitrary number of threads N at each sampling event. Only one of these threads would pass for each clocking events, whilst we remain in FSM_SAMPLE and then transition to FSM_STREAM.
Similarly, this can be applied to all of the lines.
Now the trouble is how all of this interacts when there are 2 implication operators in the antecedent. So, I am presuming it’s hard to decipher what case will cause this whole property to fail specifically so such a property can be assumed to never succeed.
there are 2 implication operators in the antecedent.
No, there are NOT 2 implication operators in the antecedent. Each of the properties are made up of an antecedent and consequent/
// Syntax of a property expression
property_expr ::=
sequence_expr
| ...
| ( property_expr )
| sequence_expr |-> property_expr
| sequence_expr |=> property_expr
| ..
// In this
seq1 |-> seq2 |-> seq3 |-> seq4
<---property->
<----- property ------>
<------------property -------->
// you have
seq3 |-> seq4 // a property, call it prop34
// If seq3==0, prop34 is vacuously true (vacuous)
seq2 |-> seq3 |-> seq4 // is same as
seq2 |-> prop34 // a property, call it prop234
// If prop34 is vacuous, then prop234 is vacuous
// If seq2==0 then prop234 is vacuous
seq1 |-> seq2 |-> seq3 |-> seq4 // is same as
seq1 |-> prop234 // a property, call it prop1234
//-----------------------------------------
// Comments on
a[*1:3] |-> ##1 b;
Above says, after 3 consecutive "a"s, then b
// You need to rephrase the requirements to something more realistic in designs
// After rising (a) then an "a[*2]" and then "b"
$rose(a) |-> ##1 a[*2] ##1 b;
//
// Note the following
(a) |-> ##1 a[*2] ##1 b; // says after every a then the consequent
// This is generally atypical, but possible as requirements.