[SystemVerilog] How to create an assertion property for an asynchronous reset when using clocking blocks?

SystemVerilog’s assertion system lets you describe your circuit’s expected behaviour with time-based expressions. These can run concurrently and verify the circuit operation at each clock cycle.

I had some trouble creating an assertion for an asynchonous reset with a clocking block. The solution is to use multi-clock sequences or properties¹.

I’ll walk through an example with an active-low reset.

// Assume this is driven elsewhere
logic reset_n;

clocking @ cb (posedge clk);
    default input #1step output #0;
    input my_data;
endclocking

property check_async_reset;
    @ (negedge reset_n) 1'b1
    ##1 @(posedge reset_n) 1'b1
    ##1 @(posedge clk) 1'b1
    ##1 (my_value_to_check == '0)
endproperty

Let’s go through the property line by line.

@ (negedge reset_n) 1'b1

We begin the assertion with the flag being pulled low. We don’t care about anything else so our assertion expression is 1'b1 so it will always pass.

##1 @(posedge reset_n) 1'b1

The ##1 expression here says to continue on with the sequence until we detect a positive edge of reset_n. The reset is de-asserted but we can’t sample the value yet as the clocking block cb hasn’t triggered an event yet. At this point in the sequence, the property’s “clock” is now posedge reset_n.

##1 @(cb) 1'b1

We do the same trick again to move to the clocking block’s clock domain. We still can’t safely check my_data because the assertion sees the value from last clock edge. As this is our first cb sampling event, my_data will likely be X.

##1 (my_value_to_check == '0)

With one more cb cycle the property will be able to see my_data from the previous cb event. We can now verify that the reset worked correctly.

The same functionality can be implemented with the implication operator. I’d argue it’s more readable but a slower to type.

property check_async_reset;
    @ (negedge reset_n) 1'b1
    |=> @(posedge reset_n) 1'b1
    |=> @(posedge clk) 1'b1
    |=> (my_value_to_check == '0)
endproperty