From db08ceb418bdf6c15b837b08a1533fc0ab04ee1c Mon Sep 17 00:00:00 2001 From: Fabian Schuiki Date: Thu, 6 Feb 2025 09:44:39 -0800 Subject: [PATCH] [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 | 39 +++++++++++++++++++ .../circt/Dialect/FIRRTL/FIRRTLStatements.td | 2 + include/circt/Dialect/FIRRTL/FIRRTLVisitors.h | 5 ++- include/circt/Dialect/Verif/VerifOps.td | 3 -- lib/Conversion/FIRRTLToHW/LowerToHW.cpp | 14 +++++++ lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp | 4 ++ test/Conversion/FIRRTLToHW/intrinsics.mlir | 15 +++++++ test/Dialect/FIRRTL/lower-intrinsics.mlir | 4 ++ test/Dialect/Verif/basic.mlir | 4 -- 9 files changed, 82 insertions(+), 8 deletions(-) diff --git a/docs/Dialects/FIRRTL/FIRRTLIntrinsics.md b/docs/Dialects/FIRRTL/FIRRTLIntrinsics.md index fe07dce59d0c..fed8a58c0b44 100644 --- a/docs/Dialects/FIRRTL/FIRRTLIntrinsics.md +++ b/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). diff --git a/include/circt/Dialect/FIRRTL/FIRRTLStatements.td b/include/circt/Dialect/FIRRTL/FIRRTLStatements.td index d271e1a77881..1307e7bc667d 100644 --- a/include/circt/Dialect/FIRRTL/FIRRTLStatements.td +++ b/include/circt/Dialect/FIRRTL/FIRRTLStatements.td @@ -368,6 +368,8 @@ class VerifIntrinsicOp traits = []> : def VerifAssertIntrinsicOp : VerifIntrinsicOp<"assert">; def VerifAssumeIntrinsicOp : VerifIntrinsicOp<"assume">; def VerifCoverIntrinsicOp : VerifIntrinsicOp<"cover">; +def VerifRequireIntrinsicOp : VerifIntrinsicOp<"require">; +def VerifEnsureIntrinsicOp : VerifIntrinsicOp<"ensure">; //===----------------------------------------------------------------------===// // Layer Block Op diff --git a/include/circt/Dialect/FIRRTL/FIRRTLVisitors.h b/include/circt/Dialect/FIRRTL/FIRRTLVisitors.h index 257f32da9e56..19e5386f1f9b 100644 --- a/include/circt/Dialect/FIRRTL/FIRRTLVisitors.h +++ b/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); diff --git a/include/circt/Dialect/Verif/VerifOps.td b/include/circt/Dialect/Verif/VerifOps.td index f17b5d47e59d..48378bd28a01 100644 --- a/include/circt/Dialect/Verif/VerifOps.td +++ b/include/circt/Dialect/Verif/VerifOps.td @@ -405,20 +405,17 @@ def ContractOp : VerifOp<"contract", [ } class RequireLikeOp : VerifOp, DeclareOpInterfaceMethods ]> { let arguments = (ins LTLAnyPropertyType:$property, - Optional:$clock, Optional:$enable, OptionalAttr:$label ); let assemblyFormat = [{ $property (`if` $enable^)? - (`clock` $clock^)? (`label` $label^)? attr-dict `:` type($property) }]; diff --git a/lib/Conversion/FIRRTLToHW/LowerToHW.cpp b/lib/Conversion/FIRRTLToHW/LowerToHW.cpp index 67d0fb75616b..85ba0e3b139d 100644 --- a/lib/Conversion/FIRRTLToHW/LowerToHW.cpp +++ b/lib/Conversion/FIRRTLToHW/LowerToHW.cpp @@ -1696,6 +1696,8 @@ struct FIRRTLLowering : public FIRRTLVisitor { 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(op); } +LogicalResult FIRRTLLowering::visitStmt(VerifRequireIntrinsicOp op) { + if (!isa(op->getParentOp())) + return lowerVerifIntrinsicOp(op); + return lowerVerifIntrinsicOp(op); +} + +LogicalResult FIRRTLLowering::visitStmt(VerifEnsureIntrinsicOp op) { + if (!isa(op->getParentOp())) + return lowerVerifIntrinsicOp(op); + return lowerVerifIntrinsicOp(op); +} + LogicalResult FIRRTLLowering::visitExpr(HasBeenResetIntrinsicOp op) { auto clock = getLoweredNonClockValue(op.getClock()); auto reset = getLoweredValue(op.getReset()); diff --git a/lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp b/lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp index c2846fe9088d..b396ee9bb573 100644 --- a/lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp +++ b/lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp @@ -1001,6 +1001,10 @@ void FIRRTLIntrinsicLoweringDialectInterface::populateIntrinsicLowerings( "circt.verif.assume", "circt_verif_assume"); lowering.add>("circt.verif.cover", "circt_verif_cover"); + lowering.add>( + "circt.verif.require", "circt_verif_require"); + lowering.add>( + "circt.verif.ensure", "circt_verif_ensure"); lowering.add("circt.mux2cell", "circt_mux2cell"); lowering.add("circt.mux4cell", "circt_mux4cell"); lowering.add("circt.has_been_reset", diff --git a/test/Conversion/FIRRTLToHW/intrinsics.mlir b/test/Conversion/FIRRTLToHW/intrinsics.mlir index f7a649c28cac..d13c222e027d 100644 --- a/test/Conversion/FIRRTLToHW/intrinsics.mlir +++ b/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 diff --git a/test/Dialect/FIRRTL/lower-intrinsics.mlir b/test/Dialect/FIRRTL/lower-intrinsics.mlir index 32d0632dc91f..3735abc889ba 100644 --- a/test/Dialect/FIRRTL/lower-intrinsics.mlir +++ b/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" %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( diff --git a/test/Dialect/Verif/basic.mlir b/test/Dialect/Verif/basic.mlir index d3538878b591..d0477adfbf3c 100644 --- a/test/Dialect/Verif/basic.mlir +++ b/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