Systemverilog assertion what is the difference between "A throughout B" and "B throughout A"?

SystemVerilog
,
1

Hi,

A throughout B" is used to specify that property A holds continuously throughout the duration of property B. In other words, A is expected to be true for the entire time that B is true.

This is the waveform

[Album] imgur.com

I’m trying to make an assertion checker as the below,
But “Busy[*1:2] throughout DRdy” and “DRdy throughout Busy[*1:2]” are working differently.
why are CHK_BPE1 and CHK_BPE2 working differently?

property BPE1; 
  @(posedge clk)

    (GntA) |=> DRdy throughout Busy[*1:2] ##0 Done;
endproperty    
               
CHK_BPE1 : assert property (BPE1);

property BPE2; 2
  @(posedge clk)
    (GntA) |=> Busy[*1:2] throughout DRdy ##0 Done;

endproperty    
               
CHK_BPE2 : assert property (BPE2);
2

In reply to UVM_LOVE:

See my paper Reflections on Users’ Experiences with SVA, part 2 https://verificationacademy.com/verification-horizons/july-2022-volume-18-issue-2/reflections-on-users-e xperiences-with-sva-part-2 Addresses the usage of these four relationship operators: throughout, until, intersect, implies

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

3

In reply to ben@SystemVerilog.us:

Hi ben,
I understand the behavior of throughout.

Thankfully… so I tried to another example.

[Album] imgur.com


Your text to link here…

property CHK02;
@(posedge clk)
$rose(idle) |=> stable(!reset) throughout (idle [*0:] ##1 !idle ##1 idle);
endproperty

CHK02_P : assert property (CHK02);

But this makes fail at 23NS. Could you give me a clue for resolve this?

4

In reply to UVM_LOVE:

SHould work per your waveform.
The throughout operator specifies that a signal (expression) must hold throughout a sequence. ( b throughout R ) is equivalent to ( b [*0:$] intersect R )

show your code

5

In reply to ben@SystemVerilog.us:

sorry for late Ben.

module Testbench;                               
            
  // DUT signals                                
  logic clk;
            
  logic GntA=0;                                 
  logic Busy=0;                                 
  logic DRdy=0;                                 
  logic Done=0;                                 
            
            
  initial begin                                 
  clk = 0;  
  end       
  // Instantiate assertion checkers             
  initial begin                                 
    // Initialize signals                       
     repeat(3)                                  
     @(posedge clk);                            
    /////////////////////////////////////////////////////////////////                           
    GntA = 1;                                   
     repeat(1)                                  
     @(posedge clk);                            
    GntA = 0;                                   
    Busy = 1;                                   
    DRdy = 1;                                   
     repeat(1)                                  
     @(posedge clk);                            
    Done =1;
     repeat(1)                                  
     @(posedge clk);                            
    Done =0;
    Busy =0;
    DRdy = 0;                                   
            
     repeat(14)                                 
     @(posedge clk);                            
            
    // Finish simulation                        
    #100;   
    $finish;
  end       
always #1 clk = ~clk;                           
            
initial begin                                   
        $shm_open("wave.shm");                  
        $shm_probe("AS");                       
end

   
property BPE1;
  @(posedge clk)
    (GntA) |=> Busy[*1:2] throughout DRdy ##0 Done;
endproperty
CHK_BPE1 : assert property (BPE1);



property BPE2;
  @(posedge clk)
    (GntA) |=> DRdy throughout Busy[*1:2] ##0 Done;
endproperty
CHK_BPE2 : assert property (BPE2);
   
endmodule

From BPE1, I get the error " Expected a verilog expression as operand to throughout operator."

6

In reply to UVM_LOVE:
You have to look at the syntax!
1800’2017 page 378

sequence_expr ::= 
 ...
| sequence_expr intersect sequence_expr 
| sequence_expr or sequence_expr 
| first_match ( sequence_expr {, sequence_match_item} ) 
| expression_or_dist throughout sequence_expr  // <<<<<<<<<<<<
| sequence_expr within sequence_expr

The throughoutrequires an expression in the LHS
you have
(GntA) |=> Busy[*1:2] throughout DRdy ##0 Done;
Busy[*1:2] is a sequence