[MooreToCore] Support assert, assume, cover ops

[mingzheTerapines]

Add conversion patterns from moore.{assert,assume,cover} to the corresponding verif.* op in MooreToConv.
Consider rejecting deferred assertions for now. https://chipsalliance.github.io/sv-tests-results/?v=circt_verilog+16.2+assert_test
Fix issue #7630

[mingzheTerapines]

@fabianschuiki What should I deal with final assert

moore.module @Assert(in %cond : !moore.l1)  {
  moore.procedure always {
  moore.assert final %cond : l1
  moore.return
  }
}

can be converted to

module {
  hw.module @Assert(in %cond : i1) {
    llhd.process {
      cf.br ^bb1
    ^bb1:  // 2 preds: ^bb0, ^bb1
      cf.br ^bb1
    }
    llhd.final {
      verif.assert %cond label "" : i1
      llhd.halt
    }
    hw.output
  }
}

But

moore.module @Assert()  {
  moore.procedure always {
    %0 = moore.constant 0 : l1
  moore.assert final %0 : l1
  moore.return
  }
}

This will has problem with passing local variables.

[fabianschuiki]

Hey @mingzheTerapines, thanks for working on this 🙌! Looking at the SV standard, IEEE 1800-2017 § 16.4 "Deferred assertions" says:

As with all immediate assertions, a deferred assertion’s expression is evaluated at the time the deferred assertion statement is processed. However, in order to facilitate glitch avoidance, the reporting or action blocks are scheduled at a later point in the current time step.

So the condition being checked is handled the same way for assert, assert #0, and assert final. You don't even need to put it into an llhd.final. Instead, you can just generate the code for the checking in the same way as you do for regular assert. The only difference is when the action block will be executed:

• For an observed deferred assertion, the subroutine shall be scheduled in the Reactive region. Actual argument expressions that are passed by reference use or assign the current values of the underlying variables in the Reactive region.
• For a final deferred assertion, the subroutine shall be scheduled in the Postponed region. Actual argument expressions that are passed by reference use the current values of the underlying variables in the Postponed region.

We don't currently differentiate between the different scheduling regions in SV. In the future we'll definitely want to do that, though. Doing so requires us to figure out how we can describe the regions in the LLHD dialect and how we can make them work in a simulator like Arcilator.

Maybe for the time being you can just treat #0 and final assertions the exact same way as regular assertions? Once we have figure out how to deal with the subtleties of scheduling regions, we can revisit this lowering and improve it.

[mingzheTerapines]

@fabianschuiki Well, that will make coding easier.
But in verilator, assert may trigger $ERROR or something, do we need this trigger explictly in operations and terminate the program?
such as

%err = moore.assert immediate %cond : l1
moore.conditional  %err{
moore.error
}

[fabianschuiki]

LGTM, thanks!

[fabianschuiki]

I suggest we leave the termination on asserts up to how the simulator, e.g. arcilator, interprets the verif.assert op you create 😃