Writing an SVA for 3 signals

SystemVerilog
1

Hi,

How do i write an assertion for “signal_a and signal_b may only be asserted if signal_c was asserted before”

Thanks
Sujith

2

Please share some examples of passing and failing cases as per your expectations

3

Passing:
signal_c is asserted and de-asserted. Later on signal_a and signal_b are asserted (any order)
signal_c is asserted and de-asserted. signal_a and signal_b are not asserted.

Failing:
signal_a or/and signal_b are asserted before signal_c was asserted.

4

A few questions

  1. What if signal_c remains asserted when signal_a or/and signal_b are asserted (any order) ?
  2. signal_c is asserted and de-asserted once but signal_a or/and signal_b are asserted twice
    Is the expectation is that assertion should fail for the 2nd assertion of signal_a or/and signal_b ?
5

Both the cases can be considered as pass.

6

So if signal_c is asserted ( does not need to de-assert ) only once during the entire simulation and then at the same clock/after ‘X’ clocks signal_a or/and signal_b are asserted ‘N’ times,
the assertion would pass ‘N’ times

7

signal_a/signal_b asserted 1 cycle after signal_c asserted N times, it should pass N times.

8 
  assert property (@(posedge clk) (!signal_a && !signal_b) until signal_c);

This will not fail if a,b,c never asserts. If you want that, use s_until.

9

Using this the assertion would pass without waiting for assertion of either signal_a / signal_b.

bit flag;

sva1:assert property( @(posedge clk) $rose(signal_c) ) flag = 1;

sva2:assert property( @(posedge clk) $rose(signal_a || signal_c ) |-> (flag == 1) );

If all 3 signals are asserted on same clock the assertion fails as pre-poned value of ‘flag’ would be 0.

EDIT ::

  1. Since sva1 executes on every clock, I would rather write it within initial procedural block
  2. sva1 fails if $rose(signal_c) is false
 initial  begin
   // Replacing 'sva1' with 
   sva1_new:assert property( @(posedge clk) $rose(signal_c) |-> 1 ) flag = 1;
 end
10

You cannot use a function directly as an expression. DO this instead

property check_a_b;
   bit v;
  @(posedge clk) (1, v=gate(c)) ##0 v |-> (!a && !b) until_with c;
endproperty
11

Thanks @dave_59 @Have_A_Doubt and @ben2 for your response.

I have used a function as an antecedent gating condition and it works for my case.

function bit gate(bit c);
  bit flag;

  if(c && !flag) begin 
    flag = 1;
    return 1;
   end

   else if(flag) return 0;

   else return 1;

endfunction

property check_a_b;
  @(posedge clk)  gate(c) |-> (!a && !b) until_with c;
endproperty

Any downside of using a function call?
12

You’re correct on functions being used as an expression. I was under the impression that they had to be in sequence_matched_items.
1800:16.6 Boolean expressions
Expressions that appear in concurrent assertions shall satisfy the following requirements:
…
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).
—Functions that appear in expressions shall not contain output or ref arguments (const ref is
allowed).
—Functions shall be automatic (or preserve no state information) and have no side effects.
[Ben] Your function relies on a static value!
Is that what you want?

function bit gate(bit c);
  bit flag;  // initialized to 0 
  if(c && !flag) begin // flag is always equal to 0 here 
    flag = 1;
    return 1;
   end
   else if(flag) return 0; // same as if(!c)
   else return 1; // useless 
endfunction
13

Though 1800: 16.6 states: Functions shall be automatic a quick check on how tools follow the ‘letter of the law’ demonstrated again that SystemVerilog is extremely flexible (meaning it does not always follow the rules).
Speaking of tools checking for 1800 !

14

For calling subroutine as a sequence_match_item , shouldn’t it be attached to a sequence expression ?

LRM 13.2

A nonvoid function can be used as an operand in an expression; the value of that operand is the value returned by the function.

My understanding is return value of gate(c) is used as a sequence_expression

15

You can split into two assertion:
sva_siga: assert property (@(posedge clk) (!signal_a ) |-> (!signal_a ) until signal_c);
sva_sigb: assert property (@(posedge clk) (!signal_b ) |-> (!signal_b ) until signal_c);