Assertion with priority

SystemVerilog
,
1

Hi,
I’m trying to implement some priority based assertion like below,

event clear_e;
bit d0,d1,d0_hit,d1_hit;

always @ (posedge L0_CLK or clear_e) begin
    if(clear_e) d0 = 0;
    else if($rose(Det0)) d0 = 1;
end
always @ (posedge L1_CLK or clear_e) begin
    if(clear_e) d1 = 0;
    else if ($rose(Det1)) d1 = 1;
end
always@(posedge L0_CLK or posedge L1_CLK or clear_e) begin
    if (clear_e) begin 
        d0_hit = 0; 
        d1_hit = 0;
    end 
    else if (d0==1 && d1 == 0) d0_hit=1;
    else if(d1==1 && d0 == 0) d1_hit=1;
end

property l0_chk_p;
    @(posedge CLK3)(d0_hit == 1) && !($stable(p0_l0)) |-> (rcv_p0 == p0_l0);
endproperty

l0_chk_a : assert property(l0_chk_p) begin
    `uvm_info("ASSERT_PASS", $psprintf("@[%0t] PASS for L0 ", $time), UVM_LOW)
    ->clear_e;
end else begin
    `uvm_error("IF_ASSERT", $psprintf("@[%0t] ASSET_ERR :L0 : Assertion FAILED !! \n", $time))
    ->clear_e;
end

property l1_chk_p;
    @(posedge CLK3)(d1_hit == 1) && !($stable(p0_l1)) |-> (rcv_p0 == p0_l1);
endproperty

l1_chk_a : assert property(l1_chk_p) begin
    `uvm_info("ASSERT_PASS", $psprintf("@[%0t] PASS for L1 ", $time), UVM_LOW)
    ->clear_e;
end else begin
    `uvm_error("IF_ASSERT", $psprintf("@[%0t] ASSET_ERR :L1 : Assertion FAILED !! \n", $time))
    ->clear_e;
end

Here, if d0 comes first it should ignore d1 even if it hits and then after some cycles of CLK3 rcv_p0 should be equal to p0_l0 else vice versa.
I see that the d0_hit/d1_hit itself is not getting asserted.
could some one help me what I’m missing here…?

2

In reply to kurma Tejendra:

There are a number of problems with the code shown.

if(clear_e)

The above is illegal because
clear_e is not an integral value. Unfortunately, some tools treat this as

if(clear_e != null)

which would always be true for this code. You need

if(clear_e.triggered)

Regardless, the third
always block is in a race with the first and second reading the values of d0 and d1. And without knowing the relationships between all the clocks there could be more race conditions.

Also
$rose(Det0) uses both L0_CLK and clear_e as implicit sampling events.

There are probably very different approaches to writing this, but it would help to have a clearer explanation of the requirements.

3

Hi Dave,

The requirement is priority in assertions.
Det0 is sampled on L0_CLK and Det1 is sampled on L1_CLK.
These signals are driven onto DUT and I want to check a condition which samples on CLK3.
Here, L0_CLK and L1_CLK has same frequency but have some phase difference(sometimes no phase difference).
So, when Det1 comes first, its corresponding value p0_l0(sampled on CLK3) should be equal to rcv_p0 value else assertion fails. vice versa for Det0.

Assume, det1 came first then det0 came later.
p0_l0 = 'h4 and p0_l1 = 'h7
rcv_p0 == 'h7
Here, I need to check this condition.