System verilog assertion

SystemVerilog
,
1

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.

2

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);
3

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?..

4

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.

5

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 );