Assumption to ensure two multibit signals are never equal in any cycle

SystemVerilog
, ,
1

Hi,
I want to write a systemverilog assumption for 2 multibit signals say A[11:0] and B[11:0] such that they are never equal in ANY cycle.
Simple != is not working as it is checking only in same cycle.
Can someone please suggest a simple way.

Thanks!

2

In reply to ppatel:

I would approach this using associative arrays and the “exists” function along with support logic.
I can work this out, but this is my approach.

Ben

3

In reply to ben@SystemVerilog.us:
The following example from my SVA book will guide you toward my approach as it uses associative arrays.


module memory_data_integrity_check (
    input bit write, // memory write
    input bit read,  // memory read
    input bit[31:0] wdata, // data written to memory
    input bit[31:0]  addr,  // memory address -- small for simulation 
    input bit reset_n, // active low reset
    input bit clk);   // clock 

    timeunit 1ns;   timeprecision 100ps;
    default clocking cb_clk @ (posedge clk);  endclocking 
    int mem_aarray[*]; // associative array (AA) to be used by property
    bit [31:0] rdata;  // data read from memory
    bit  mem_aarray_exists;  // exists at specified address
    assign mem_aarray_exists  = mem_aarray.exists(addr); 
    always_comb 
        if(mem_aarray_exists) 
            rdata  = mem_aarray[addr];  //  
    always@ (posedge clk)
        if (reset_n==1'b0) mem_aarray.delete; // Clears AA elements
        else if (write) mem_aarray[addr]  = wdata; // store data

    property p_read_after_write;
        bit [31:0] v_wrdata, v_wraddr;
        (write, v_wraddr=addr, v_wrdata= wdata) |-> // if write, save data and addr
        (read && mem_aarray_exists && addr==v_wraddr) [->1] |-> // @read and data there at same written addr
        rdata==v_wrdata;  // read data is same as what was written 
    endproperty : p_read_after_write
    ap_read_after_write : assert property (p_read_after_write)
        $info("addr =%h, rdata=%h", $sampled(addr), $sampled(rdata)); else 
        $error("addr =%h, rdata=%h", $sampled(addr), $sampled(rdata)); 
        
    property p_read_before_write;
        not (read && !mem_aarray_exists); // never a read on an non written address
    endproperty : p_read_before_write
    ap_read_before_write : assert property (p_read_before_write);
endmodule : memory_data_integrity_check

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:
4

In reply to ben@SystemVerilog.us:

Hi Ben,
Actually i am using Formal Verification tool and it is only allowing synthesizable code. It is printing out an error saying it cant synthesize dynamic array.

5

In reply to ppatel:
I don’t see a way in formal verification to express an assumption that 2 multibit signals (e.g., A[11:0] and B[11:0]) are never equal in ANY cycle. Reflecting on possibilities, I see two spaces (or maps) of values that are the XOR of each other, For a moment I thought of using the $past, but the number of pasts would not work in simulation for cycles that have not occurred unless you start the evaluation after “n” cycles. Here is an assertion where “a” and “b” are unequal in the last 4 cycles. Note the ##4 in the antecedent.

 
ap_diff: assume property(@ (posedge clk) 
     ##4 1 |-> a!= b and  
               $past(a, 1) != $past(b, 1) and   
               $past(a, 2) != $past(b, 2) and   
               $past(a, 3) != $past(b, 3));

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:
6

In reply to ben@SystemVerilog.us:

Thanks Ben for the help! As you said there may not be any simple way to write such synthesizable code. Maybe i will just do A%x==0 and B%x!=0 (some constant x)to generate some disjoint traffic.