Conditional assertion

SystemVerilog
,
1

Hi All,

How do I specify a conditional assertion based on p_event.

If p_event goes high , If a=0 and b=0 c should be equal to d

$rose(p_event) → if ((a=0) && (b==0)) |-> ( c == d);

Thanks
JeffD

2

In reply to dvuvmsv:

$rose(p_event) && (a==0) && (b==0) |-> ( c == d);

Will this work?

3

property p0_c0_0;
@(posedge clk)
disable iff (!resetn)
($rose(p_event) && (a==0) && (b==0)) → (c == d);
endproperty
a1: assert property(p0_c0_0);

is not working.

I even tried this one below. It is not working.

property p0_c0_1;
@(posedge clk)
disable iff (!resetn)
$rose(p_event) |-> if ((a==0) && (b==0)) (c == d);
endproperty

a1: assert property(p0_c0_1);

Thanks
JeffD

4

In reply to dvuvmsv:

I experimented in edaplayground. it seems to be working

5

Hi,

Thanks for the example. In my case p_event is generated from clk.

I do not see the assertion getting triggered.

property p0_c0_0;
@(posedge clk)
disable iff (!resetn)
($rose(p_event) && (a==0) && (b==0)) → (c == d);
endproperty
a1: assert property(p0_c0_0);

Do the assertion gets triggered if rising edge of p_event is generated from clk.
In your example p_event is independent of clk.

Thanks
JeffD

6

In reply to dvuvmsv:

The assertion is evaluated every raising edge of the clk.
And the antecedent is successful when there is raising_edge in p_event, a & b being zero.

7

Thanks
JeffD