Hi,
iam new to sva, please help to write assertion.
How can you write an assertion to ensure that a signal ‘error’ is never asserted while ‘valid’ is low?
Thank you help to provide.
Hi,
iam new to sva, please help to write assertion.
How can you write an assertion to ensure that a signal ‘error’ is never asserted while ‘valid’ is low?
Thank you help to provide.
In reply to Madhu C:
I am assuming the starting point of the check would be when ‘valid’ goes high->low i.e $fell(valid)
Now once ‘valid’ is low , signal ‘error’ shouldn’t be high till the time ‘valid’ goes low->high
i.e we need to check that ‘error’ is low throughout when ‘valid’ is low
property p1;
$fell(valid) |=> ( !error ) throughout $rose(valid)[->1];
endproperty
assert property( p1 ) $display("T:%0t Pass",$time); else $display("T:%0t Fails",$time);
Note that if error is high on the same clock that valid is re-asserted then the assertion fails !!
// Eg:
bit valid = 1;
bit clk , error ;
always #5 clk = !clk;
initial begin
#14; valid = 0;
#50 ; valid = 1; error = 1; // Both are asserted at T:65 so SVA fails at T:65
#2 ; $finish();
end
If the requirement is that ‘error’ is don’t care ( 0/1 ) on the clock that ‘valid’ is re-asserted (0->1) , the solution would be to use until/s_until :
property p2;
$fell(valid) |=> ( !error ) until $rose(valid); // Goto repetition removed from RHS sequence
endproperty
assert property( p2 ) $display("T:%0t Pass",$time); else $display("T:%0t Fails",$time);
In reply to Have_A_Doubt:
my approach is
1.A1: assert property(@(posedge clk) fell(valid) |->!error[*1:] intersect !valid [*1:$] ##1 valid) $info(“pass @%0t”,$time);
2.A2:assert property(@(posedge clk) !valid |-> !error );
which one is correct?..
In reply to Madhu C:
For each attempt (1) checks across multiple clocks whereas (2) checks only for 1 clock
So (1) is a better approach.
Also consider re-writing (1) as :
$fell(valid) |-> (!error)[*1:$] intersect $rose(valid)[->1];
Note that (1) too throws assertion failure at T:65 for above stimulus
Also for (1) ‘error’ must be low on the clock tick when valid goes 1->0 , else the assertion fails.
In reply to Madhu C:
A2 is the correct assertion for the requirement you stated
assert property(@(posedge clk) !valid |-> !error );
Which is the same as the Boolean expression
assert property(@(posedge clk) valid || !error );