[FIRRTL] Add require and ensure intrinsics (#8154)

Add the `circt.verif.require` and `circt.verif.ensure` intrinsics as a
way to produce the `verif.require` and `verif.ensure` operations from
FIRRTL. At a later point we'll probably want to promote the five verif
ops `assert`, `assume`, `cover`, `require`, and `ensure` to the FIRRTL
spec and merge the functionality of the `circt.verif.assert` intrinsic
with the `firrtl.assert` operation.

Note that this requires dropping of the clock operand from
`verif.require` and `verif.ensure`. This operand was never used, so it
feels like a reasonable change. At a later point we might want to merge
`verif.clocked_assert` into `verif.assert` by adding clock operands to
the verif ops in general.

docs/Dialects/FIRRTL/FIRRTLIntrinsics.md

@@ -414,3 +414,42 @@ what the field in the bundle is.
 | elements | array  | List of AugmentedFields                                   |
 
 Creates a SystemVerilog interface for each bundle type.
+
+### circt_verif_assert
+
+Asserts that a property holds.
+The property may be an boolean, sequence, or property.
+Booleans are represented as `UInt<1>` values.
+Sequences and properties are defined by the corresponding `circt_ltl_*` intrinsics and are also represented as `UInt<1>`, but are converted into dedicated sequence and property types later in the compiler.
+
+| Parameter | Type   | Description                 |
+| --------- | ------ | --------------------------- |
+| label     | string | Optional user-defined label |
+
+| Argument | Type    | Description                                     |
+| -------- | ------- | ----------------------------------------------- |
+| property | UInt<1> | A property to be checked.                       |
+| enable   | UInt<1> | Optional enable condition.                      |
+|          |         | If 0, behaves as if the assert was not present. |
+
+### circt_verif_assume
+
+Assumes that a property holds.
+Otherwise behaves like [`circt_verif_assert`](#circt_verif_assert).
+
+### circt_verif_cover
+
+Checks that a property holds at least once, or can hold at all.
+Otherwise behaves like [`circt_verif_assert`](#circt_verif_assert).
+
+### circt_verif_require
+
+Requires that a property holds as a pre-condition to a contract.
+Gets converted into an assert if used outside of a FIRRTL `contract`.
+Otherwise behaves like [`circt_verif_assert`](#circt_verif_assert).
+
+### circt_verif_ensure
+
+Ensures that a property holds as a post-condition of a contract.
+Gets converted into an assert if used outside of a FIRRTL `contract`.
+Otherwise behaves like [`circt_verif_assert`](#circt_verif_assert).

include/circt/Dialect/FIRRTL/FIRRTLStatements.td

@@ -368,6 +368,8 @@ class VerifIntrinsicOp<string mnemonic, list<Trait> traits = []> :
 def VerifAssertIntrinsicOp : VerifIntrinsicOp<"assert">;
 def VerifAssumeIntrinsicOp : VerifIntrinsicOp<"assume">;
 def VerifCoverIntrinsicOp : VerifIntrinsicOp<"cover">;
+def VerifRequireIntrinsicOp : VerifIntrinsicOp<"require">;
+def VerifEnsureIntrinsicOp : VerifIntrinsicOp<"ensure">;
 
 //===----------------------------------------------------------------------===//
 // Layer Block Op

include/circt/Dialect/FIRRTL/FIRRTLVisitors.h

@@ -242,7 +242,8 @@ class StmtVisitor {
             PropAssignOp, RefForceOp, RefForceInitialOp, RefReleaseOp,
             RefReleaseInitialOp, FPGAProbeIntrinsicOp, VerifAssertIntrinsicOp,
             VerifAssumeIntrinsicOp, UnclockedAssumeIntrinsicOp,
-            VerifCoverIntrinsicOp, LayerBlockOp, MatchOp, ViewIntrinsicOp>(
+            VerifCoverIntrinsicOp, VerifRequireIntrinsicOp,
+            VerifEnsureIntrinsicOp, LayerBlockOp, MatchOp, ViewIntrinsicOp>(
             [&](auto opNode) -> ResultType {
               return thisCast->visitStmt(opNode, args...);
             })
@@ -289,6 +290,8 @@ class StmtVisitor {
   HANDLE(VerifAssertIntrinsicOp);
   HANDLE(VerifAssumeIntrinsicOp);
   HANDLE(VerifCoverIntrinsicOp);
+  HANDLE(VerifRequireIntrinsicOp);
+  HANDLE(VerifEnsureIntrinsicOp);
   HANDLE(UnclockedAssumeIntrinsicOp);
   HANDLE(LayerBlockOp);
   HANDLE(MatchOp);

include/circt/Dialect/Verif/VerifOps.td

@@ -405,20 +405,17 @@ def ContractOp : VerifOp<"contract", [
 }
 
 class RequireLikeOp<string mnemonic> : VerifOp<mnemonic, [
-  AttrSizedOperandSegments,
   HasParent<"verif::ContractOp">,
   DeclareOpInterfaceMethods<RequireLike>
 ]> {
   let arguments = (ins
     LTLAnyPropertyType:$property,
-    Optional<ClockType>:$clock,
     Optional<I1>:$enable,
     OptionalAttr<StrAttr>:$label
   );
   let assemblyFormat = [{
     $property
     (`if` $enable^)?
-    (`clock` $clock^)?
     (`label` $label^)?
     attr-dict `:` type($property)
   }];

lib/Conversion/FIRRTLToHW/LowerToHW.cpp

@@ -1696,6 +1696,8 @@ struct FIRRTLLowering : public FIRRTLVisitor<FIRRTLLowering, LogicalResult> {
   LogicalResult visitStmt(VerifAssertIntrinsicOp op);
   LogicalResult visitStmt(VerifAssumeIntrinsicOp op);
   LogicalResult visitStmt(VerifCoverIntrinsicOp op);
+  LogicalResult visitStmt(VerifRequireIntrinsicOp op);
+  LogicalResult visitStmt(VerifEnsureIntrinsicOp op);
   LogicalResult visitExpr(HasBeenResetIntrinsicOp op);
   LogicalResult visitStmt(UnclockedAssumeIntrinsicOp op);
 
@@ -3889,6 +3891,18 @@ LogicalResult FIRRTLLowering::visitStmt(VerifCoverIntrinsicOp op) {
   return lowerVerifIntrinsicOp<verif::CoverOp>(op);
 }
 
+LogicalResult FIRRTLLowering::visitStmt(VerifRequireIntrinsicOp op) {
+  if (!isa<verif::ContractOp>(op->getParentOp()))
+    return lowerVerifIntrinsicOp<verif::AssertOp>(op);
+  return lowerVerifIntrinsicOp<verif::RequireOp>(op);
+}
+
+LogicalResult FIRRTLLowering::visitStmt(VerifEnsureIntrinsicOp op) {
+  if (!isa<verif::ContractOp>(op->getParentOp()))
+    return lowerVerifIntrinsicOp<verif::AssertOp>(op);
+  return lowerVerifIntrinsicOp<verif::EnsureOp>(op);
+}
+
 LogicalResult FIRRTLLowering::visitExpr(HasBeenResetIntrinsicOp op) {
   auto clock = getLoweredNonClockValue(op.getClock());
   auto reset = getLoweredValue(op.getReset());

lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp

@@ -1001,6 +1001,10 @@ void FIRRTLIntrinsicLoweringDialectInterface::populateIntrinsicLowerings(
       "circt.verif.assume", "circt_verif_assume");
   lowering.add<CirctVerifConverter<VerifCoverIntrinsicOp>>("circt.verif.cover",
                                                            "circt_verif_cover");
+  lowering.add<CirctVerifConverter<VerifRequireIntrinsicOp>>(
+      "circt.verif.require", "circt_verif_require");
+  lowering.add<CirctVerifConverter<VerifEnsureIntrinsicOp>>(
+      "circt.verif.ensure", "circt_verif_ensure");
   lowering.add<CirctMux2CellConverter>("circt.mux2cell", "circt_mux2cell");
   lowering.add<CirctMux4CellConverter>("circt.mux4cell", "circt_mux4cell");
   lowering.add<CirctHasBeenResetConverter>("circt.has_been_reset",

test/Conversion/FIRRTLToHW/intrinsics.mlir

@@ -119,6 +119,21 @@ firrtl.circuit "Intrinsics" {
     firrtl.int.verif.cover %k0 : !firrtl.uint<1>
     // CHECK-NEXT: verif.cover [[K0]] label "hello" : !ltl.property
     firrtl.int.verif.cover %k0 {label = "hello"} : !firrtl.uint<1>
+    // CHECK-NEXT: verif.assert %a : i1
+    firrtl.int.verif.require %a : !firrtl.uint<1>
+    // CHECK-NEXT: verif.assert %a : i1
+    firrtl.int.verif.ensure %a : !firrtl.uint<1>
+    // CHECK-NEXT: verif.contract
+    verif.contract {
+      // CHECK-NEXT: verif.require %a : i1
+      firrtl.int.verif.require %a : !firrtl.uint<1>
+      // CHECK-NEXT: verif.require %a label "hello" : i1
+      firrtl.int.verif.require %a {label = "hello"} : !firrtl.uint<1>
+      // CHECK-NEXT: verif.ensure [[C0]] : !ltl.sequence
+      firrtl.int.verif.ensure %c0 : !firrtl.uint<1>
+      // CHECK-NEXT: verif.ensure [[C0]] label "hello" : !ltl.sequence
+      firrtl.int.verif.ensure %c0 {label = "hello"} : !firrtl.uint<1>
+    }
   }
 
   // CHECK-LABEL: hw.module @LowerIntrinsicStyle

test/Dialect/FIRRTL/lower-intrinsics.mlir

@@ -87,10 +87,14 @@ firrtl.circuit "Foo" {
     // CHECK-NEXT: firrtl.int.verif.assert %in {label = "hello"} :
     // CHECK-NEXT: firrtl.int.verif.assume %in :
     // CHECK-NEXT: firrtl.int.verif.cover %in :
+    // CHECK-NEXT: firrtl.int.verif.require %in :
+    // CHECK-NEXT: firrtl.int.verif.ensure %in :
     firrtl.int.generic "circt_verif_assert"  %in : (!firrtl.uint<1>) -> ()
     firrtl.int.generic "circt_verif_assert" <label: none = "hello"> %in : (!firrtl.uint<1>) -> ()
     firrtl.int.generic "circt_verif_assume"  %in : (!firrtl.uint<1>) -> ()
     firrtl.int.generic "circt_verif_cover"  %in : (!firrtl.uint<1>) -> ()
+    firrtl.int.generic "circt_verif_require"  %in : (!firrtl.uint<1>) -> ()
+    firrtl.int.generic "circt_verif_ensure"  %in : (!firrtl.uint<1>) -> ()
   }
 
   // CHECK-LABEL: firrtl.module private @MuxCell(

test/Dialect/Verif/basic.mlir

@@ -87,26 +87,22 @@ verif.contract {}
 verif.contract {
   // CHECK: verif.require {{%.+}} : i1
   // CHECK: verif.require {{%.+}} if {{%.+}} : i1
-  // CHECK: verif.require {{%.+}} clock {{%.+}} : i1
   // CHECK: verif.require {{%.+}} label "foo" : i1
   // CHECK: verif.require {{%.+}} : !ltl.sequence
   // CHECK: verif.require {{%.+}} : !ltl.property
   verif.require %true : i1
   verif.require %true if %true : i1
-  verif.require %true clock %d : i1
   verif.require %true label "foo" : i1
   verif.require %s : !ltl.sequence
   verif.require %p : !ltl.property
 
   // CHECK: verif.ensure {{%.+}} : i1
   // CHECK: verif.ensure {{%.+}} if {{%.+}} : i1
-  // CHECK: verif.ensure {{%.+}} clock {{%.+}} : i1
   // CHECK: verif.ensure {{%.+}} label "foo" : i1
   // CHECK: verif.ensure {{%.+}} : !ltl.sequence
   // CHECK: verif.ensure {{%.+}} : !ltl.property
   verif.ensure %true : i1
   verif.ensure %true if %true : i1
-  verif.ensure %true clock %d : i1
   verif.ensure %true label "foo" : i1
   verif.ensure %s : !ltl.sequence
   verif.ensure %p : !ltl.property