Support s_eventually (#7291)

[b-chmiel]

Implements strong eventually (s_eventually, IEEE 1800-2023 16.12.13) in the context of property expression.

The algorithm lowers this code:

module t;
  bit clk = 0;
  initial forever #1 clk = ~clk;
  bit a = 0;
  bit b = 1;
  int cyc = 0;
  always @(posedge clk) begin
    ++cyc;
    b = ~b;
    $display("%0t", $time);
    if (cyc >= 3) $finish;
  end
  assert property (@(posedge clk) s_eventually a == b) begin
    $display("success");
  end
  else begin
    $display("failure");
  end
endmodule

into:

module t;
  bit clk = 0;
  initial forever #1 clk = ~clk;
  bit a = 0;
  bit b = 1;
  int cyc = 0;
  always @(posedge clk) begin
    ++cyc;
    b = ~b;
    $display("%0t", $time);
    if (cyc >= 3) $finish;
  end
  always @(posedge clk) begin
    fork
      begin
        // Note: s_eventually requires importing std
        __VassertsActive___0[std::process::self()] = 1;
        // Note: s_eventually requires --timing
        while ((!($sampled(a) == $sampled(b)))) #1;

        $display("success");
        __VassertsActive___0.delete(std::process::self());
      end
    join_none
  end
  bit __VassertsActive___0[std::process];
  final begin
    int __VassertCount;
    __VassertCount = __VassertsActive___0.size();
    while ((__VassertCount != 32'h0)) begin
      if (($sampled(a) == $sampled(b))) $display("success");
      else $display("failure");
      __VassertCount = (__VassertCount - 32'h1);
    end
  end
endmodule

Resolves #7291

[wsnyder]

  always @(posedge clk) begin
    fork
      begin
        // Note: s_eventually requires importing std
        __VassertsActive___0[std::process::self()] = 1;
        // Note: s_eventually requires --timing
        while ((!($sampled(a) == $sampled(b)))) #1;

Why is any fork required and more so why fork every cycle? I'd think this can become a SERE that determines match (or not)?

Why the #1 - that certainly doesn't make sense it's at least clock edge related.

[b-chmiel]

On every posedge clk new assertion is "started" and every single one of them either waits on clock events (#1 which in fact is waiting for a assertion's clocking block event) or terminates successfully when condition is fulfilled. To track those running assertions we already use forks, see:

verilator/src/V3Assert.cpp

Line 303 in bb1bfab

AstFork* const forkp = new AstFork{nodep->fileline(), VJoinType::JOIN_NONE};

[wsnyder]

Anything should be convertable to an appropriate state machine, but I guess I'll accept the we already fork argument and punt the performance down the road.

[wsnyder]

Add verilog format on/off around these please

[wsnyder]

Please remove line number from message so is less sensitive to small changes in .v file.

[wsnyder]

Suggest a test where have say 1000 cycles and each s_eventually terminates after say 2 cycles. This is to make sure we clean up properly (e.g. don't for some reason get 1000 forks every cycle).

[wsnyder]

Please make a rootp()->stdPackageProcessp and stdPackageClassp and use here and in V3LinkJump where this seems to have come from, to avoid duplication.

[wsnyder]

Just inline these.

[wsnyder]

Is there a test for this? I'll turn on coverage.

[verilator-ci]

Patch coverage from PR workflow #2450 (code coverage of lines changed relative to 5d1b4fe):

  lines: 98.25% (112 of 114 lines)
  branches: 90.00% (18 of 20 branches)

Report: 25050153549