Chipress

In the last post, we mentioned that liveness properties may not be useful in simulation. Some simulation tools do not always report liveness property failure in DV tests.

In addition, liveness properties may even significantly degrade simulation speed. Simulation tools use checker threads for SVA properties. Due to its nature of “infinity”, liveness properties have long running threads.

We may workaround this deficiency while still implementing some sort of liveness check for DV.

For example, we want to prove, if valid is high, ready is eventually high to avoid deadlock. One can write a liveness property like this:

assert property (@(posedge clk) vld |-> s_eventually rdy);

In the DV environment, we can convert the check to be “if valid was ever high, ready must have been high before the last clock edge”. 

With some help of assertion modeling code and SystemVerilog final block, designers can implement the check like this:

logic check_pass;
always_ff @(posedge clk)
    if (~resetn)    check_pass <= ‘1;
    else if (rdy)   check_pass <= ‘1;
    else if (vld)   check_pass <= ‘0;

final begin
    assert (check_pass == ‘1) begin
        $info(“PASS!”);                  
    end else
        $error(“FAIL!”);
end