Hello,
I have written the assertion for the following scenario and for some clock ticks the assertions are failing ,please correct me if i have written the assertion wrong.
consider these signals [15:0]signal,[4:0]a,b,c
a= signal[0:4] i.e 5bits
b= signal[5:9] i.e 5bits
c =signal[10:14] 5bits
scenario:**when a is equal to any value from o to 31 ,then in the next 4 cycles ,either b or c should be equal to a and in these 4 cycles a value should not be equal to previous value.
**
example : when a==25, then in the next 4 cycles ,either b==25 or c==25 and in these 4 cycles a !=25
In reply to vinayks:
How is (a==5’d1||a==5’b0) anywhere close to meaning “a is equal to any value from 0 to 31”
Based on your example, I think you meant to say:
“When a is equal to any value from 0 to 31 ,then in the next 4 cycles ,either b or c should be equal to what a was in the first cycle, and a cannot be the same as it was in the first cycle.”
property p;
int v;
@(posedge CLK) (a inside {0:31]}, v = a) |=> (v inside {b,c} && a != v)[*4];
endproperty
// "When a is equal to any value from 0 to 31 ,then in the next 4 cycles ,
//either b or c should be equal to what a was in the first cycle,
// and a cannot be the same as it was in the first cycle."
property p_a4bc;
int v;
@(posedge clk) (a inside {[0:31]}, v = a) |-> ##[1:4] (v == b || v==c) and
##1 (a != v)[*4];
endproperty
ap_p_a4bc: assert property(p_a4bc);
Is this the correct SVA based on the problem statement?
we store a value in cycle1 and then in
cycle2,3,4,5 we have one of b or c matching the a value in cycle1 and we also ensured ‘a’ value in cycles 2-5 is not matching it’s value in cycle1
we use [*4] as we are maintaining the check for 4 cycles from 2-5. Based on the problem statement it looks like a hard constraint to maintain the check for 4 consecutive cycles and is not optional. If it was optional then using ##[m:n] was appropriate.
Please correct me if I am wrong.
property p_a4bc;
int v;
@(posedge clk) (a inside {[0:31]}, v = a) |=> ((v == b || v==c) and (a != v))[*4];
//cycle1 //cycle2,3,4,5
endproperty
ap_p_a4bc: assert property(p_a4bc);
|=> ((v == b || v==c) and (a != v))[*4];
// Above says the 1 cycle sequence (v == b || v==c) is sequence ANDed
// with the 1 cycle sequence (a != v)
// That ANDing is repeated 4 times.
// For success, the match MUST occur at everyone of those cycles.
// Note: Because these are 1 cycle occurrences, I claim that the consequent is equivalent to
((v == b || v==c) && (a != v))[*4];
// This is not you intent, per your requirements
//
##[1:4] (v == b || v==c) and
##1 (a != v)[*4];
// Says, I have 2 concurrent sequences, each lasts 4 cycles.
// In these 4 cycles, two things must occur:
// 1) v == b || v==c) must occur at least once
// 2) (a != v) must occur during all these 4 cycles.
//
// .. Based on the problem statement it looks like a hard constraint to maintain
// the check for 4 consecutive cycles and is not optional.
// If it was optional then using ##[m:n] was appropriate.
property p_a4bc_optional;
int v;
@(posedge clk) (a inside {[0:31]}, v = a) |->
##[1:4] (v == b || v==c) and // (v == b || v==c) occurs at least once
##[1:4] (a != v); // a !=v occurss at least once
endproperty
ap_p_a4b_optional: assert property(p_a4bc_optional)
You use the non-overlapping implication operator |=>
I generally prefer to use the overlapping implication operator |-> Note:****|=> is equivalent to ##1 |->
This is because the consequent is a property. Using the incorrect equivalent of |-> ##1
you would get antecedent |-> ##1 property. and that is illegal
The reason I prefer (personal preference) to use the |-> ##1 sequence
is because it read better. It’s similar to if(antecedent_is _a_match) then at next cycle.
There is no mental effort to go through the conversion of what this |=> is, though I know what it is. For example,
a |=> ##[0:3] b; // reads as at next, then from that current point to the next 3 cycles
a |-> ##[1:4] b; // reads as the next 1 to 4 cycles
