Popping Queue elements as sequence_expr

SystemVerilog
, ,
1

Hi,
I was trying the following code ::

 `ifdef M1  
   always #5 clk1 = !clk1;
   always #6 clk2 = !clk2;
 `elsif M2  
   always #6 clk1 = !clk1;
   always #5 clk2 = !clk2;
 `elsif M3  
   always #5 clk1 = !clk1;
   always #5 clk2 = !clk2;
 `endif  

   bit[2:0] value_q[$] ;

   always@(posedge clk1) value_q.push_back($urandom());

   property queue_pop;
     @(posedge clk2) value_q.pop_back();
   endproperty  

   aq_pop:assert property( queue_pop ) $display("T:%0t Pass",$time); else  $display("T:%0t Fails",$time);

  initial #50 $finish();

To my surprise I observe compilation error

Error-[ETTNATE] Invalid type in temporal expression

Why is ‘value_q.pop_back()’ not considered a valid sequence expression ?

2

pop_back() is a function call.
This should work

(1, v=value_q.pop_back()) ##0 v==1

This could also be a tool issue.
In the past I had issues with associative arrays.

3

Hi Ben,
Using

   property queue_pop;
      int loc;
     @(posedge clk2) (1,loc=value_q.pop_back()) ##0 loc;
   endproperty

I am still observing compilation issues with the following msg
Tool1 ::
** Error: Queue_pop_as_Seq_Expr.sv(23): The method ‘pop_back’ is not allowed in assertions as it has side effects.

Tool2 ::
Expressions involving real, realtime, string, event and dynamic
SystemVerilog types including virtual interface references are not allowed
in local variable assignments in properties and sequences.

I checked SV LRM 2023 for this

16.6 Boolean expressions
Elements of dynamic arrays, queues, and associative arrays that are sampled for assertion expression
evaluation may get removed from the array or the array may get resized before the assertion
expression is evaluated. These specific array elements sampled for assertion expression evaluation
shall continue to exist within the scope of the assertion until the assertion expression evaluation
completes.

Sequence match items with a local variable as the variable_lvalue may use the C assignment,
increment, and decrement operators. Otherwise, evaluation of an expression shall not have any side
effects (e.g., the increment and decrement operators are not allowed).

LRM further mentions the following example

bit a;
integer b;
byte q[$];

property p1;
 $rose(a) |-> q[0];
endproperty

property p2;
 integer l_b;
 ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
endproperty

So this does tell me that using Queue element as sequence_expr is legal (provided they are of integral type)

One solution is to return value_q.pop_back() from a subroutine called on match of a seq_expr

4

The following worked with 2 tools, but gave me an error with another one.

module m(input bit valid, clk, 
               bit[31:0]  addr);
  // There is a valid,addr protocol similar to AXI. 
  // I want to write an assumption that last 16 valid addresses(with valid=1) has to be unique .
    
    int mem_aarray[*]; // associative array (AA) to be used by property
    //bit [31:0] raadata;  // data read from AA
    bit  mem_aarray_exists;  // exists at specified address
    // assign mem_aarray_exists  = mem_aarray.exists(addr); 
    function automatic void f0(); mem_aarray.delete; endfunction
    function automatic bit f1(int addr); 
       return mem_aarray.exists(addr);
    endfunction

    property m_valid_addr;
      bit v_err=0;
        @(posedge clk) ($rose(valid) , f0()) |-> 
      ((valid, v_err=f1(addr)) ##0 !v_err)[*16]; // it should not exist
    endproperty
  am_valid_addr: assume property(m_valid_addr);  

  property m_valid_addr2; // line 22
  bit v_err=0;
    @(posedge clk) ($rose(valid) , f0()) |-> 
  ((valid, v_err=mem_aarray.exists(addr)) ##0 !v_err)[*16]; // it should not exist
endproperty
am_valid_addr2: assume property(m_valid_addr2);
endmodule 
//Invalid type in local variable assign
testbench.sv, 22
m, "mem_aarray.exists(addr)"
  Expressions involving real, realtime, string, event and dynamic 
  SystemVerilog types including virtual interface references are not allowed 
  in local variable assignments in properties and sequences.
Note: Using an external user-defined function call worked.
5

My paper addresses the issues you brought up.
SVA PAPER: DYNAMIC DATA STRUCTURES IN ASSERTIONS

qmodel
qmodel1089×653 124 KB

The integration of dynamic data structures, such as queues and associative arrays, into SystemVerilog assertions has sparked ongoing discussion in the hardware verification community. While these constructs enhance assertion capabilities, their support across EDA tools is inconsistent.

This paper addresses the challenges posed by the lack of uniform support for dynamic structures in SVA among tool vendors. It examines the current state of assertion support in major EDA tools, revealing disparities in handling queues and associative arrays. This inconsistency raises questions about the necessity and practicality of these complex structures in assertions.

Despite concerns, the benefits of using queues and associative arrays in specific verification scenarios are significant. The paper explores methods to implement these data structures in assertions, even without direct tool support. It presents techniques for efficient support logic, enabling verification engineers to utilize these structures while maintaining portability and performance.

Additionally, the paper demonstrates these techniques with a simulateable example and explores synthesizable logic as an alternative approach for formal verification environments. This solution aims to bridge the gap between simulation-based and formal verification methodologies.
Activate

6

Thanks Ben.
Based on the tool error msg above, I tried a code using a virtual interface within concurrent assertion

`include "uvm_pkg.sv"
`include "uvm_macros.svh"
 import uvm_pkg::*;

interface intf;
   logic a , b;
 endinterface  

module sva(input bit clk);
   
   virtual intf  vintf;      
   
   initial begin
     #0;// To ensure get() is done after set
     if( !uvm_config_db#(virtual intf)::get(null,"top_tb","vintf_inst",vintf) ) 
        `uvm_fatal("sva","Unable to fetch vintf")
   end  
        
   sva1:assert property( @(posedge clk) $rose(vintf.a) |=> vintf.b ) 
                   else `uvm_error("sva","Assertion fails")
   
 endmodule  
                     
 module top_tb;
   
   intf intf_inst();
   
   bit clk;
   
   initial forever #5 clk = !clk;
   
   initial begin
     uvm_config_db#(virtual intf)::set(null,"top_tb","vintf_inst",intf_inst);
     // run_test();     
   end  
   
   sva   sva_(clk);
   
   initial #50 $finish();
   
   initial begin
     #30; intf_inst.a = 1 ;
   end  
   
 endmodule

Although I ensure that the virtual interface is non-null, prior to 1st clocking event, EDA tools throw an error:

Fatal: (vsim-131) testbench.sv(21): Null instance encountered when dereferencing ‘/top_tb/sva_/vintf.a’

The alternative approach would be to pass each interface via port-list in module ‘sva’

Does the LRM restrict using a virtual interface as a sequence_expression ?

1 Like
7

All the variables used in an assertion have to be static at elaboration.
Ben

8

Here is what I found in LRM

Expressions that appear in concurrent assertions shall satisfy the following requirements:
- Expressions shall not reference non-static class properties or methods