[Verif] Add has_been_reset op

[fabianschuiki]

Add the verif.has_been_reset operation to detect if a circuit has been properly reset. Useful to disable assertions before and during reset.

The result of verif.has_been_reset reads as 0 immediately after simulation startup and after each power-cycle in a power-aware simulation. The result remains 0 before and during reset and only switches to 1 after the reset is deasserted again.

This is a useful utility to disable the evaluation of assertions and other verification constructs in the IR before the circuit being tested has been properly reset. Verification failures due to uninitialized or randomized initial state can thus be prevented.

Using the result of verif.has_been_reset to enable verification is more powerful and proper than just disabling verification during reset. The latter does not properly handle the period of time between simulation startup or power-cycling and the start of reset. verif.has_been_reset is guaranteed to produce a 0 value in that period, as well as during the reset.

Example:

hw.module @HasBeenResetAsync(%clock: i1, %reset: i1) -> (out: i1) {
  %0 = verif.has_been_reset %clock, async %reset
  hw.output %0 : i1
}

The above produces the following Verilog:

module HasBeenResetAsync(input clock, reset, output out);
  reg hasBeenResetReg;
  initial begin
    if (reset)
      hasBeenResetReg = 1'h1;
    else
      hasBeenResetReg = 1'bx;
  end
  always @(posedge reset) hasBeenResetReg <= 1'h1;
  assign out = hasBeenResetReg === 1'h1 & reset === 1'h0;
endmodule

Future work: This is a verification-only construct. It lowers to a register that will not behave in the right way in actual silicon. Tools like firtool may need a linting pass that ensures the results of this op don't leak into synthesizable parts of the IR.

[uenoku]

Nice! Changes in foldUtil, KeywordBool and firtool look great and can be landed separately.
I have one question about the behavior when has_been_reset op is assigned to different registers. In that case the has_been_reset value can be used in a different always block even when both always statements are triggered at the same time, e.g:

sv.macro.decl @RANDOM
hw.module @HasBeenResetAsync(%clock: i1, %reset: i1, %v: i1) -> (out: i1) {
  %0 = verif.has_been_reset %clock, async %reset
  %1 = seq.firreg %v clock %clock reset async %reset, %0 : i1
  hw.output %1: i1
}

  always @(posedge reset)
    hasBeenResetReg = 1'h1;
  wire hasBeenReset = hasBeenResetReg === 1'h1 & reset === 1'h0;
  reg  _GEN;
  always @(posedge clock or posedge reset) begin
    if (reset)
      _GEN <= hasBeenReset;
    else
      _GEN <= v;

In this case what's the value of hasBeenReset in the second alway block?

Future work: This is a verification-only construct. It lowers to a register that will not behave in the right way in actual silicon. Tools like firtool may need a linting pass that ensures the results of this op don't leak into synthesizable parts of the IR.

ETC should automatically extract these ops if has_been_reset ops are used only verification constructs. They could remain in synthesizable parts if used by design outputs but it should be users' responsibility to avoid such uses.

[uenoku]

Async firreg adds a clock to the sensitive list so I'm curios whether we need to follow that style here.

always @(posedge clock or posedge reset) {
  if(reset)
      hashBeenReset <= 1;
}

[fabianschuiki]

This shouldn't be necessary here, since this is a simulation-only construct when emitted as Verilog.

[fabianschuiki]

FPGA-based emulation flows that want to synthesize asserts and have a hasBeenReset available would have to add a dedicated FPGA lowering of the operation anyway.

[fabianschuiki]

@uenoku I just now realized that I've picked the wrong assigment. Wanted to go for the non-blocking <= assignment. Your example should then see reg _GEN assigned to 0 since always @(posedge reset) hasBeenResetReg <= 1'h1 only schedules the value of the register to change in the next delta time step.

[uenoku]

Wanted to go for the non-blocking <= assignment

I see! If this is non-blocking assignment then it looks fine to me 👍

[jackkoenig]

I would also note that it doesn't really make sense to asynchronously reset a register with the value from hasBeenReset, if the semantics are clear that's fine but it would also be fine to just error since you should express that code differently (at posedge reset, hasBeenReset will always be 0 so just asynchronously reset to 0).

[fabianschuiki]

@uenoku Ready for re-review. Factored out the utility stuff and switched to non-blocking assignments as I originally intended 😀

[uenoku]

One question about non-blocking assignment in initial block. Otherwise, LGTM