does Chisel have any property matching "final" in SV?

[phelixmw]

I am wondering if Chisel has a way to write something similar to final block in SV.
final and assert are a good way to verify credited protocol.

[jackkoenig]

Chisel has eventually which I think can be used to model similar things. @fabianschuiki may know more.

[phelixmw]

my understanding of eventually is SV's implication with indefinite window (until it satisfies once).
final block will check the given condition once at $finish.

[fabianschuiki]

I don't think we have support for this as of today. If I understand you correctly, you are looking for something like

module Foo;
  final begin
    // do stuff on termination
  end
endmodule

to execute arbitrary code once the simulation terminates. There are also final flavors of the common immediate assertions, like

module Foo;
  always @(something) begin
    assert final (condition);
    assume final (condition);
    cover final (condition);
  end
endmodule

which are scheduled to execute at the end of the current timestep (postponed region), but you probably don't mean these.

The closest you can come to this today in Chisel is to use assert property (@(posedge clk) s_eventually(condition)), which may work under certain circumstances. For a credit-based interface, you may want to assert the property that the credits will eventually fully replenish, or will replenish to a certain degree. Maybe something like this:

assert property (@(posedge clk) credit == 0 |-> s_eventually(credit > 0));

I am not sure how the equivalent of a final block would look like in Chisel. Or if there should be some form of assert that gets emitted into a final block 🤔