XOR in assertion property

SystemVerilog
, , ,
1

Hi

How can I do xor in assertion property?
like-


    property checker(clk,enable,a,b,idx);
    @(posedge clk) 
       (enable) |-> a[idx^b] === b;
      endproperty:checker

it’s seem it do idx power b …

Thanks

2

In reply to Junior:

You are using the correct operator (^) for XOR. The power operator is (******)

3

In reply to Junior:

working as expected for me


module test();
 bit clk;
 bit en;
 bit [3:0] a[8];
 bit [3:0] b, exp_b[8];
 bit [2:0] idx, idx_xor;

  initial begin
    forever #5 clk = !clk;
  end

  assign idx_xor = idx^b;
  
  initial begin
    a['b000^'b000] = 'b000;  //a[0]=0
    a['b001^'b010] = 'b010;  //a[1]=2
    a['b011^'b001] = 'b001;  //a[2]=1
    a['b100^'b011] = 'b011;  //a[7]=3
 // a['b101^'b010] = 'b010;  //a[7]=2

    //a['b000^'b000] = 'b000;  //a[0]=0
    @(posedge clk);
    en  <= 1;
    idx <= 'b000;
    b   <= 'b000;
    
    //a['b001^'b010] = 'b010;  //a[1]=2
    repeat(2)@(posedge clk);
    idx <= 'b001;
    b   <= 'b010;
    
    //a['b011^'b001] = 'b001;  //a[2]=1
    repeat(2)@(posedge clk);
    idx <= 'b011;
    b   <= 'b001;

    //Assertion failure expected
    repeat(2)@(posedge clk); 
    idx <= 'b011;
    b   <= 'b110;
    $display("Assertion failure expected : idx='b011, b='b110");
    
    //a['b100^'b011] = 'b011;  //a[7]=3
    repeat(2)@(posedge clk);
    idx <= 'b100;
    b   <= 'b011;
    
    repeat(2)@(posedge clk);
    en <= 0;
    #50 $finish;
  end

  ap: assert property(checker(clk,en,a,b,idx));

  property checker(clk,enable,a,b,idx);
     @(posedge clk) 
     (enable, $display("%t idx=0x%x, b=0x%x, a[idx^b]=0x%x",$time, $sampled(idx), $sampled(b), a[$sampled(idx)^$sampled(b)])) 
     |-> a[idx^b] == b;
  endproperty:checker

endmodule

/*
OUTPUT:
                  15 idx=0x0, b=0x0, a[idx^b]=0x0
                  25 idx=0x0, b=0x0, a[idx^b]=0x0
                  35 idx=0x1, b=0x2, a[idx^b]=0x2
                  45 idx=0x1, b=0x2, a[idx^b]=0x2
                  55 idx=0x3, b=0x1, a[idx^b]=0x1
Assertion failure expected : idx='b011, b='b110
                  65 idx=0x3, b=0x1, a[idx^b]=0x1
                  75 idx=0x3, b=0x6, a[idx^b]=0x0
"testbench.sv", 53: test.ap: started at 75ns failed at 75ns
	Offending '(a[(idx ^ b)] == b)'
                  85 idx=0x3, b=0x6, a[idx^b]=0x0
"testbench.sv", 53: test.ap: started at 85ns failed at 85ns
	Offending '(a[(idx ^ b)] == b)'
                  95 idx=0x4, b=0x3, a[idx^b]=0x3
                 105 idx=0x4, b=0x3, a[idx^b]=0x3
*/
4

In reply to Alokpati:

Thanks guys for your help,
seem that the issue was different.

another query,
I have 1 property, that I assert to it multiply times,

and for some this working -
(A) |-> ## [0:3] ($past(sig_1) === sig_2);
and some didn’t have delay and this works fine -
(A) |-> ## [0:3] sig_1 === sig_2;

and my question is if there is can be some merge between the two?
cause I don’t want to do 2 assertions…

Thanks!!

5

In reply to Junior:

can you elaborate what is the exact scenario for which you want to write assertion?

6

In reply to Alokpati:

I have a situation that between sig 1 & sig 2 there is a delay of 1 cycle.
and for itm this assertion is working well:
(A) |-> ## [0:3] ($past(sig_1) === sig_2);

another scenario, is that the sig2 happened in the same cycle as sig 1
(A) |-> ## [0:3] sig_1 === sig_2;

now want I want to do is to do 1 property to the 2 scenarios.

7

In reply to Junior:

(A) |-> ## [0:3] $past(sig_1) === sig_2 || sig_1 === sig_2;

Please start a new question with a new topic.