SV assertion

SystemVerilog
,
1

Hi,
I have an assertion that there I do something like that-
(evt) |=> signal[idx] === b

and I have 2 signals, that I want to send both for the src, like that:

assert property…
.signal(signal_1 & signal_2)
but I have an error of -“Illegal bit or part select” (both signals are 4 bits and the idx<4)

and another question, I have 4 signals of 1 bit, and I want to chain them for 1 signal of 4 bit (for the signal…)
I did something like that-
.signal({signal_1 , signal_2 , signal_3 , signal_4})
and I have the same error as above…

please, anyone have an idea how I have to do these things?

thanks!
I write in sv with uvm…

2

In reply to Junior:
If I understand you correctly, you are trying to do something like:


(evt) |=> .signal(signal_1 & signal_2)[idx]==b;  //  signal[idx] === b

//Weird! .signal(signal_1 & signal_2) results is a vector of bits, like 4'b1010
// I don't believe that 4'b1010[idx] is legal 
// At least, I never used it that way
// Try this instead
wire temp[`SIZE:0];
assign temp=(signal_1 & signal_2);
(evt) |=> .signal(temp)[idx]==b;  //  signal[idx] === b
3

In reply to ben@SystemVerilog.us:

A reply from a colleague:
No the result is an expression, it is not evaluated when substituting for formal, hence the result is index on an expression - not legal.

4

In reply to ben@SystemVerilog.us:

//Instead of 
(signal_1 & signal_2)[idx]==b;
// do 
(signal_1[idx] && signal_2[idx])=b;
5

In reply to ben@SystemVerilog.us:

what I wanted to do it that this logic will stay:
(evt) |=> signal[idx] === b

and when I send the signal to the property,
I want to send signal_a & signal_b

what I finally did, it like you said,
(with the wire)
but I thought that there is easier way…

Thank you for your help!

6

In reply to Junior:


property p_s1s2x(s1, s2, idx);
 @(posedge clk) evt) |=> s1[idx] && s2[idx] === b
endproperty 
ap_s1s2x: assert property(p(signal_a, signal_b, idx));
7

In reply to ben@SystemVerilog.us:

but I can do something like that:

property p_s1s2x(s, idx);
 @(posedge clk) evt) |=> s[idx] === b
endproperty 
ap_s1s2x: assert property(p(.s(signal_a & signal_b), idx))

;

because I use with this property also for 1 signal… (ap_s1s1x: assert property(p(signal, idx)))

8

In reply to Junior:

When the actual argument is an expression rather than a signal, extracting a bit out of an argument is illegal. Thus, if the result of (signal_a & signal_b) is 4’b1010
4’b1010[2] is illegal. Same issue if you pass as actual (signal_a==4’b1001); you are passing an expression, not a signal that can be sampled.
If you need to extract bit 2 out of this value, you could from within the assertion call a function that right shift that value by 2, and then AND the right shift result by 4’b0001.


// Untested, nned to test
  function bit f(bit[3:0] v, idx);
    f=(v>>idx) & 4'b0001;
  endfunction
  
property p_s1s2x(s, idx);
  bit[3:0] v; 
 @(posedge clk) evt) |=> (1, v=f(s, idx)) ##0 v== b;
endproperty 
ap_s1s2x: assert property(p(.s(signal_a & signal_b), idx))
9

In reply to ben@SystemVerilog.us:

ok,
Thanks a lot for your help!