SVA: throught operator

SystemVerilog
1

Hi,
The assertion below is not working as intended.
Spec: When ‘rst_b’ goes high, signal ‘valid’ should also go high and stay high as long as ‘rst_b’ is high. ‘Valid’ should go low in the same cycle that ‘rst_b’ goes low.

Property p_valid;
@(posedge clk)
$rose(rst_b) |-> (valid throughout rst_b) ##0 !valid;

Here, the assertion passes in the second cycle and does not fail if valid goes low while rst_b is1.
Can someone help me understand why the ‘throught’ operator isn’t working in the assertion i wrote.

Thanks,
Nithya

2

From my paper

Throughout

The syntax for this sequence is: expression_or_dist throughout sequence_expr. The throughout operator specifies that a signal (expression) must hold throughout a sequence

 ( b throughout R_sequence ) is equivalent to
 ( b [*0:$] intersect R_sequence )

// You need one of these 2 identical options 
$rose(rst_b) |-> (valid [*1:$] ##1 !valid)] intersect (rst_b[*1:$])  ##1 !rst_b; 
$rose(rst_b) |->  !valid [->1]  intersect (!rst_b[->1]) ;
 rst_b            0  1  1  1  1  0
valid             x  1  1  1  1  0
 rst_b[->1]       0  0  0  0  0  1
!rst_b[->1]       1  1  1  1  1  0

Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
https://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf

2 Likes
3

Thanks a lot Ben!
Could you please help me understand why ‘throughout’ does not work here?

4

Read my paper and understand the equivalency of the trhoughtout.

$rose(rst_b) |-> (valid throughout rst_b) ##0 !valid;
Here you are saying that valid must be true throughout the length of the sequence rst_b that is ONE CYCLE long!

1 Like
5

Got it. Thanks, Ben.

6

Just another suggestion without using throughout

property pp_valid;
  @(posedge clk)
  $rose(rst_b) |-> always (valid === rst_b);
endproperty
2 Likes
7

Hi Ben,
Is the 2nd part of the requirement achievable ?
I tried the following

  property p1;
    //@(posedge clk) $rose(rst_b) |-> ( valid throughout $fell(rst_b)[->1] ) ##0 !valid;
    //@(posedge clk) $rose(rst_b) |-> ( valid until $fell(rst_b) ) ##0 !valid;
    @(posedge clk) $rose(rst_b) |-> ( valid throughout (rst_b[*1:$] ##1 $fell(rst_b)) ) ##0 !valid;
  endproperty
  
 ap1:assert property(p1) $display("T:%0t Pass",$time); else $display("T:%0t Fails",$time);

 always #5 clk = !clk;
    
  initial begin    
    #4 ; rst_b = 1; valid = 1;    
    #40; rst_b = 0;  
         valid = 0; // Irrespective of whether valid is 0/1. The assertion fails at T:45
    #2 $finish();    
  end
8

Issue?
Link to model?

9

My apologies. There are 2 requirements in the original question ::
(1) When ‘rst_b’ goes high, signal ‘valid’ should also go high and stay high as long as ‘rst_b’ is high.
(2) ‘Valid’ should go low in the same cycle that ‘rst_b’ goes low.

I tried the following : edalink
However the assertion fails at T:45

Here is one solution which works

property p1;
   @(posedge clk) $rose(rst_b) |-> ( valid throughout rst_b[*1:$] ) ##1 ( $fell(rst_b) && !valid );
endproperty
10

thethru
thethru1858×850 189 KB

EDA Playground code
EPWave Waveform Viewer wave
There is a contradiction with valid in those assertions that fail