From bb6471f7e4928f654f4606f1e3e89df44652ea3b Mon Sep 17 00:00:00 2001 From: Amelia Dobis Date: Mon, 12 Aug 2024 10:42:06 -0700 Subject: [PATCH] [Verif] Generalize Formal Contracts (#7495) * Generalized verif contracts * updated contract op description --- include/circt/Dialect/Verif/VerifOps.td | 97 ++++++++++--------------- lib/Dialect/Verif/VerifOps.cpp | 62 +++++----------- test/Dialect/Verif/basic.mlir | 72 ++++++------------ 3 files changed, 78 insertions(+), 153 deletions(-) diff --git a/include/circt/Dialect/Verif/VerifOps.td b/include/circt/Dialect/Verif/VerifOps.td index 299f9c769eac..8333d8fe2157 100644 --- a/include/circt/Dialect/Verif/VerifOps.td +++ b/include/circt/Dialect/Verif/VerifOps.td @@ -251,7 +251,7 @@ def YieldOp : VerifOp<"yield", [ Terminator, ParentOneOf<[ "verif::LogicEquivalenceCheckingOp", "verif::BoundedModelCheckingOp", - "verif::InstanceOp" + "verif::ContractOp" ]> ]> { let summary = "yields values from a region"; @@ -313,7 +313,7 @@ def FormalOp : VerifOp<"formal", [ //===----------------------------------------------------------------------===// def SymbolicInputOp : VerifOp<"symbolic_input", [ - ParentOneOf<["verif::FormalOp", "verif::InstanceOp"]> + ParentOneOf<["verif::FormalOp"]> ]>{ let summary = "declare a symbolic input for formal verification"; let description = [{ @@ -354,70 +354,46 @@ def ConcreteInputOp : VerifOp<"concrete_input", [ // Formal Contract Ops //===----------------------------------------------------------------------===// -class ContractLikeOp traits = []> - : VerifOp, RegionKindInterface, IsolatedFromAbove - ]> { - - let arguments = (ins Variadic:$inputs); - - let regions = (region SizedRegion<1>:$body); - - let extraClassDeclaration = [{ - /// Implement RegionKindInterface. - static RegionKind getRegionKind(unsigned index) { - return RegionKind::Graph; - } - - /// Retrieves the region block arguments - BlockArgument getRegionArg(unsigned index) { - return getBody().front().getArguments()[index]; - } - - /// Retrieves the number of block arguments - unsigned getNumRegionArgs() { - return getBody().front().getNumArguments(); - } - }]; - - let hasRegionVerifier = 1; -} - - -def ContractOp : ContractLikeOp<"contract", [NoTerminator]>{ +def ContractOp : VerifOp<"contract", [ + SingleBlockImplicitTerminator<"verif::YieldOp">, + HasParent<"hw::HWModuleOp">, + RegionKindInterface +]>{ let summary = "declare a formal contract"; let description = [{ This operation declares a formal contract that is used to create precondition and postconditions on a parent module. These are used as an abstraction to better modularize formal verification such that each module containing a contract is checked exactly once. The contract contains a single block where the block arguments - represent the inputs and outputs in the same order as in the module signature. + represent the results of the code block that the contract is abstracting over. The + operands represent the SSA values that this contract's results will replace. e.g. ``` hw.module @Bar(in %foo : i8, out "" : i8, out "1" : i8) { - verif.contract (%foo) : (i8) { - ^bb0(%arg1 : i8, %bar.0 : i8, %bar.1 : i8): + %o0, %o1 = verif.contract (%to0, %to1) : (i8, i8) -> (i8, i8) { + ^bb0(%bar.0 : i8, %bar.1 : i8): %c0_8 = hw.constant 0 : i8 - %prec = comb.icmp bin ugt %arg1, %c0_8 : i8 + %prec = comb.icmp bin ugt %foo, %c0_8 : i8 verif.require %prec : i1 - %post = comb.icmp bin ugt %bar.0, %arg1 : i8 - %post1 = comb.icmp bin ult %bar.1, %arg1 : i8 + %post = comb.icmp bin ugt %bar.0, %foo : i8 + %post1 = comb.icmp bin ult %bar.1, %foo : i8 verif.ensure %post : i1 verif.ensure %post1 : i1 - } + verif.yield %bar.0, %bar.1 : i8, i8 + } /* ... Module definition ... */ } ``` This later is used to replace any instance of Bar during verification: ``` - %bar.0, %bar.1 = hw.instance "bar" @Bar("foo" : %foo : i8) -> ("" : i8, "1" : i8) + %bar.0, %bar.1 = hw.instance "bar" @Bar("foo" : %c42_8 : i8) -> ("" : i8, "1" : i8) /* ... After PrepareForFormal Pass becomes ... */ - %bar.0, %bar.1 = verif.instance (%c42_8) : (i8) -> (i8, i8) { + %bar.0, %bar.1 = verif.contract (%c42_8) : (i8) -> (i8, i8) { ^bb0(%arg1: i8): %c0_8 = hw.constant 0 : i8 %prec = comb.icmp bin ugt %arg1, %c0_8 : i8 @@ -435,29 +411,32 @@ def ContractOp : ContractLikeOp<"contract", [NoTerminator]>{ ``` }]; + let arguments = (ins Variadic:$inputs); + let results = (outs Variadic:$results); + let regions = (region SizedRegion<1>:$body); + let assemblyFormat = [{ - `(` $inputs `)` attr-dict `:` `(` type($inputs) `)` $body + `(` $inputs `)` attr-dict `:` `(` type($inputs) `)` `->` `(` type($results) `)` $body }]; -} -def InstanceOp : ContractLikeOp<"instance", [ - SingleBlockImplicitTerminator<"verif::YieldOp"> -]>{ - let summary = "declare an instance of a formal contract (replace an hw.instance)"; - let description = [{ - This operation declares an instance of an `hw.module` that contains a - `verif.contract` definition. The body of this op will be a modified version - of the body of the referenced module's contract body, with `verif.require` - ops being reoplaced with `verif.assert` and `verif.ensure` being replaced - with `verif.assume`. The `verif.result` ops are converted into `verif.symbolic_input` - and are yielded as a result of the region to be used in the rest of the module. - }]; + let extraClassDeclaration = [{ + /// Implement RegionKindInterface. + static RegionKind getRegionKind(unsigned index) { + return RegionKind::Graph; + } - let results = (outs Variadic:$results); + /// Retrieves the region block arguments + BlockArgument getRegionArg(unsigned index) { + return getBody().front().getArguments()[index]; + } - let assemblyFormat = [{ - `(` $inputs `)` attr-dict `:` functional-type($inputs, $results) $body + /// Retrieves the number of block arguments + unsigned getNumRegionArgs() { + return getBody().front().getNumArguments(); + } }]; + + let hasRegionVerifier = 1; } class RequireLikeOp traits = [ diff --git a/lib/Dialect/Verif/VerifOps.cpp b/lib/Dialect/Verif/VerifOps.cpp index 21d4e1d1af47..62a56f80de61 100644 --- a/lib/Dialect/Verif/VerifOps.cpp +++ b/lib/Dialect/Verif/VerifOps.cpp @@ -104,50 +104,26 @@ LogicalResult ContractOp::verifyRegions() { if (!parent) return emitOpError() << "parent of contract must be an hw.module!"; - auto nInputsInModule = parent.getNumInputPorts(); - auto nOutputsInModule = parent.getNumOutputPorts(); - auto nOps = (*this)->getNumOperands(); - - // Check that the region block arguments match the op's inputs - if (nInputsInModule != nOps) - return emitOpError() << "contract must have the same number of arguments " - << "as the number of inputs in the parent module!"; - - // Check that the region block arguments match the op's inputs - if (getNumRegionArgs() != (nOps + nOutputsInModule)) - return emitOpError() << "region must have the same number of arguments " - << "as the number of arguments in the parent module!"; - - // Check that the region block arguments share the same types as the inputs - if (getBody().front().getArgumentTypes() != parent.getPortTypes()) + auto nRes = (*this)->getNumResults(); + auto resTypes = (*this)->getResultTypes(); + auto *yield = getBody().front().getTerminator(); + + // Check that the region terminator yields the same number of ops as the + // number of results + if (yield->getNumOperands() != nRes) + return emitOpError() << "region terminator must yield the same number of " + << "operands as there are results!"; + + // Check that the region terminator yields the same types of ops as the + // types of results + if (yield->getOperandTypes() != resTypes) + return emitOpError() << "region terminator must yield the same types of " + << "operands as the result types!"; + + // Check that the region block arguments share the same types as the results + if (getBody().front().getArgumentTypes() != resTypes) return emitOpError() << "region must have the same type of arguments " - << "as the type of inputs!"; - - return success(); -} - -LogicalResult InstanceOp::verifyRegions() { - // Check that the region block arguments match the op's inputs - if (getNumRegionArgs() != (*this)->getNumOperands()) - return emitOpError() << "region must have the same number of arguments " - << "as the number of inputs!"; - - // Check that the region block arguments share the same types as the inputs - if (getBody().front().getArgumentTypes() != (*this)->getOperandTypes()) - return emitOpError() << "region must have the same type of arguments " - << "as the type of inputs!"; - - // Check that verif.yield yielded the expected number of operations - if ((*this)->getNumResults() != - getBody().front().getTerminator()->getNumOperands()) - return emitOpError() << "region terminator must yield the same number" - << "of operations as there are results!"; - - // Check that the yielded types match the result types - if ((*this)->getResultTypes() != - getBody().front().getTerminator()->getOperandTypes()) - return emitOpError() << "region terminator must yield the same types" - << "as the result types!"; + << "as the type of results!"; return success(); } diff --git a/test/Dialect/Verif/basic.mlir b/test/Dialect/Verif/basic.mlir index 1f53b83bd706..4a87a9ab56c8 100644 --- a/test/Dialect/Verif/basic.mlir +++ b/test/Dialect/Verif/basic.mlir @@ -58,70 +58,40 @@ verif.formal @formal1(k = 20) { // CHECK-LABEL: hw.module @Bar hw.module @Bar(in %foo : i8, out "" : i8, out "1" : i8) { - // CHECK: verif.contract(%foo) : (i8) { - verif.contract (%foo) : (i8) { - // CHECK: ^bb0(%[[ARG:.+]]: i8, %[[OUT:.+]]: i8, %[[OUT1:.+]]: i8): - ^bb0(%arg1 : i8, %bar.0 : i8, %bar.1 : i8): + // CHECK: %[[C1:.+]] = hw.constant + %c1_8 = hw.constant 1 : i8 + // CHECK: %[[O1:.+]] = comb.add + %to0 = comb.add bin %foo, %c1_8 : i8 + // CHECK: %[[O2:.+]] = comb.sub + %to1 = comb.sub bin %foo, %c1_8 : i8 + + // CHECK: %[[OUT:.+]]:2 = verif.contract(%[[O1]], %[[O2]]) : (i8, i8) -> (i8, i8) { + %o0, %o1 = verif.contract (%to0, %to1) : (i8, i8) -> (i8, i8) { + // CHECK: ^bb0(%[[BAR0:.+]]: i8, %[[BAR1:.+]]: i8): + ^bb0(%bar.0 : i8, %bar.1 : i8): // CHECK: %[[C0:.+]] = hw.constant 0 : i8 %c0_8 = hw.constant 0 : i8 - // CHECK: %[[PREC:.+]] = comb.icmp bin ugt %[[ARG]], %[[C0]] : i8 - %prec = comb.icmp bin ugt %arg1, %c0_8 : i8 + // CHECK: %[[PREC:.+]] = comb.icmp bin ugt %foo, %[[C0]] : i8 + %prec = comb.icmp bin ugt %foo, %c0_8 : i8 // CHECK: verif.require %[[PREC]] : i1 verif.require %prec : i1 - // CHECK: %[[P0:.+]] = comb.icmp bin ugt %[[OUT]], %[[ARG]] : i8 - %post = comb.icmp bin ugt %bar.0, %arg1 : i8 - // CHECK: %[[P1:.+]] = comb.icmp bin ult %[[OUT1]], %[[ARG]] : i8 - %post1 = comb.icmp bin ult %bar.1, %arg1 : i8 + // CHECK: %[[P0:.+]] = comb.icmp bin ugt %[[BAR0]], %foo : i8 + %post = comb.icmp bin ugt %bar.0, %foo : i8 + // CHECK: %[[P1:.+]] = comb.icmp bin ult %[[BAR1]], %foo : i8 + %post1 = comb.icmp bin ult %bar.1, %foo : i8 // CHECK: verif.ensure %[[P0]] : i1 verif.ensure %post : i1 // CHECK: verif.ensure %[[P1]] : i1 verif.ensure %post1 : i1 - } - // CHECK: %[[C1:.+]] = hw.constant - %c1_8 = hw.constant 1 : i8 - // CHECK: %[[O1:.+]] = comb.add - %o0 = comb.add bin %foo, %c1_8 : i8 - // CHECK: %[[O2:.+]] = comb.sub - %o1 = comb.sub bin %foo, %c1_8 : i8 + // CHECK: verif.yield %[[BAR0]], %[[BAR1]] : i8, i8 + verif.yield %bar.0, %bar.1 : i8, i8 + } + // CHECK-LABEL: hw.output hw.output %o0, %o1 : i8, i8 } -// CHECK-LABEL: hw.module @Foo1 -hw.module @Foo1(in %0 "0": i1, in %1 "1": i1, out "" : i8, out "1" : i8) { - // CHECK: %[[C42:.+]] = hw.constant 42 : i8 - %c42_8 = hw.constant 42 : i8 - // CHECK: %[[OUTS:.+]]:2 = verif.instance(%[[C42]]) : (i8) -> (i8, i8) { - %bar.0, %bar.1 = verif.instance (%c42_8) : (i8) -> (i8, i8) { - // CHECK: ^bb0(%[[ARG:.+]]: i8): - ^bb0(%arg1: i8): - // CHECK: %[[C0:.+]] = hw.constant 0 : i8 - %c0_8 = hw.constant 0 : i8 - // CHECK: %[[PREC:.+]] = comb.icmp bin ugt %[[ARG]], %[[C0]] : i8 - %prec = comb.icmp bin ugt %arg1, %c0_8 : i8 - // CHECK: verif.assert %[[PREC]] : i1 - verif.assert %prec : i1 - - // CHECK: %[[OUT0:.+]] = verif.symbolic_input : i8 - %bar.0 = verif.symbolic_input : i8 - // CHECK: %[[OUT1:.+]] = verif.symbolic_input : i8 - %bar.1 = verif.symbolic_input : i8 - // CHECK: %[[P0:.+]] = comb.icmp bin ugt %[[OUT0]], %[[ARG]] : i8 - %post = comb.icmp bin ugt %bar.0, %arg1 : i8 - // CHECK: %[[P1:.+]] = comb.icmp bin ult %[[OUT1]], %[[ARG]] : i8 - %post1 = comb.icmp bin ult %bar.1, %arg1 : i8 - // CHECK: verif.assume %[[P0]] : i1 - verif.assume %post : i1 - // CHECK: verif.assume %[[P1]] : i1 - verif.assume %post1 : i1 - // CHECK: verif.yield %[[OUT0]], %[[OUT1]] : i8, i8 - verif.yield %bar.0, %bar.1 : i8, i8 - } - // CHECK: hw.output %[[OUTS]]#0, %[[OUTS]]#1 : i8, i8 - hw.output %bar.0, %bar.1 : i8, i8 - } - //===----------------------------------------------------------------------===// // Print-related // Must be inside hw.module to ensure that the dialect is loaded.