Formal Assumption

SystemVerilog
,
1

Hi,
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 .
Please help on what can be different ways. I can think of writing 16 deep memory in auxiliary code and using the values pushed to constrain my code.

2

You can use associative arrays. Partialcode:

module m;
  // 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 .
    bit valid, clk; 
    bit[31:0]  addr;  
    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]; //I thinkyou need the "!"
    endproperty
  am_valid_addr: assume property(m_valid_addr);  
  endmodule

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

3

I will try this.
But where are you storing addr entry in associative area. YOu need to edit the code

4

I said it was partial code to demonstrate the concepts. For formal, addr is an input, and formal should consider the assume in electing values for analysis. For simulation, you can write a constraint in the randomization.
I updated the code

5

I was trying to say, you are not storing the value in associative array
mem_aarray[addr] = 1

6

Use support logic to do that.
I said, it was partial code.

7

If the goal is for the FV tool to assume that addr has values that are different at every cycle when valid==1, it would seem that we can create different values for a variable “q” and assume that addr==q.

We can use an LFSR to generate those values.

From my donated ($3, AMZN fee) I write:

"Linear Feedback Shift Registers (LFSR) are also referred to as “maximal count” counters (a counter that counts (2n)-1) unique states. LFSR counters are very fast counters because the counter is made up of a shift register with a few EXCLUSIVE-OR taps, which is unlike binary counters that include of an adder. LFSRs do not count sequentially. Several methods can be used to force an LFSR to count to 2n states: "

(I used AI to get the unverified algorithm)

module m(input bit valid, clk,

    bit[15:0] addr); // untestedcode

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

let SEED = 16’hABCD; // Initial seed

bit[15:0] q;

// Define the feedback polynomial (x^16 + x^13 + x^4 + x^1)

let FEEDBACK_POLY = 16’hD00B;

function automatic bit[15:0] lfsr16bits(bit[15:0] lfsr);

 if (lfsr == 0) lfsr16bits = 1;

 else lfsr16bits = (q >> 1) ^ (FEEDBACK_POLY & q);

endfunction

always_ff @(posedge clk) if(valid) q<= lfsr16bits(q);

am_valid_addr: assume property(@(posedge clk) $rose(valid) |->

(valid ##0 addr==q)[*16]); // the value of valid is different at every cycle

endmodule