[Verif] Introduce Formal Contracts (#7325)

This PR proposes a new set of ops aimed at enabling the use of formal contracts to abstract away module instances during verification.

There is still some work needed to handle these ops in PrepareForFormal, which will be done in a later PR.

include/circt/Dialect/Verif/VerifOps.h

@@ -11,6 +11,7 @@
 
 #include "circt/Dialect/HW/HWAttributes.h"
 #include "circt/Dialect/HW/HWDialect.h"
+#include "circt/Dialect/HW/HWOps.h"
 #include "circt/Dialect/HW/HWTypes.h"
 #include "circt/Dialect/Seq/SeqTypes.h"
 #include "circt/Dialect/Verif/VerifDialect.h"

include/circt/Dialect/Verif/VerifOps.td

@@ -249,7 +249,10 @@ def LogicEquivalenceCheckingOp : VerifOp<"lec", [
 
 def YieldOp : VerifOp<"yield", [
   Terminator,
-  ParentOneOf<["verif::LogicEquivalenceCheckingOp", "verif::BoundedModelCheckingOp"]>
+  ParentOneOf<[
+    "verif::LogicEquivalenceCheckingOp", "verif::BoundedModelCheckingOp",
+    "verif::InstanceOp"
+  ]>
 ]> {
   let summary = "yields values from a region";
 
@@ -309,7 +312,9 @@ def FormalOp : VerifOp<"formal", [
 // Formal Verification Ops
 //===----------------------------------------------------------------------===//
 
-def SymbolicInputOp : VerifOp<"symbolic_input", [HasParent<"verif::FormalOp">]>{
+def SymbolicInputOp : VerifOp<"symbolic_input", [
+  ParentOneOf<["verif::FormalOp", "verif::InstanceOp"]>
+]>{
   let summary = "declare a symbolic input for formal verification";
   let description = [{
     This operation declares a symbolic input that can then be used to reason 
@@ -345,4 +350,146 @@ def ConcreteInputOp : VerifOp<"concrete_input", [
   }];
 }
 
+//===----------------------------------------------------------------------===//
+// Formal Contract Ops
+//===----------------------------------------------------------------------===//
+
+class ContractLikeOp<string mnemonic, list<Trait> traits = []> 
+  : VerifOp<mnemonic, traits # [
+    HasParent<"hw::HWModuleOp">, RegionKindInterface, IsolatedFromAbove
+  ]> {
+
+  let arguments = (ins Variadic<AnyType>:$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]>{
+  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.
+
+    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): 
+          %c0_8 = hw.constant 0 : i8 
+          %prec = comb.icmp bin ugt %arg1, %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
+          verif.ensure %post : i1
+          verif.ensure %post1 : i1
+      }
+      /* ... 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)
+
+    /* ... After PrepareForFormal Pass becomes ... */
+
+    %bar.0, %bar.1 = verif.instance (%c42_8) : (i8) -> (i8, i8) {
+      ^bb0(%arg1: i8):
+        %c0_8 = hw.constant 0 : i8
+        %prec = comb.icmp bin ugt %arg1, %c0_8 : i8
+        verif.assert %prec : i1
+
+        %bar.0 = verif.symbolic_input : i8
+        %bar.1 = verif.symbolic_input : i8
+        %post = comb.icmp bin ugt %bar.0, %arg1 : i8
+        %post1 = comb.icmp bin ult %bar.1, %arg1 : i8
+        verif.assume %post : i1
+        verif.assume %post1 : i1
+        verif.yield %bar.0, %bar.1 : i8, i8
+    }
+
+    ```
+  }];
+
+  let assemblyFormat = [{
+    `(` $inputs `)` attr-dict `:` `(` type($inputs) `)` $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 results = (outs Variadic<AnyType>:$results);
+
+  let assemblyFormat = [{
+    `(` $inputs `)` attr-dict `:` functional-type($inputs, $results) $body
+  }];
+}
+
+class RequireLikeOp<string mnemonic, list<Trait> traits = [
+  HasParent<"verif::ContractOp">, AttrSizedOperandSegments
+]> : VerifOp<mnemonic, traits> {
+  let arguments = (ins LTLAnyPropertyType:$property,
+                      OptionalAttr<ClockEdgeAttr>:$edge, Optional<I1>:$clock,
+                      Optional<I1>:$enable,
+                      OptionalAttr<StrAttr>:$label);
+  let assemblyFormat = [{
+    $property (`if` $enable^)? (`,` $edge^ $clock)? 
+    (`label` $label^)? attr-dict `:` type($property)
+  }];
+}
+
+def RequireOp : RequireLikeOp<"require"> {
+  let summary = "define a precondition for the given contract";
+  let description = [{
+    This operation defines a precondition for the parent contract. 
+    Preconditions are assumed during the verification of a module and 
+    asserted during the verification of an instance of a module.
+  }];
+}
+
+
+def EnsureOp : RequireLikeOp<"ensure">{
+  let summary = "define a postcondition for the given contract";
+  let description = [{
+    This operation defines a postcondition for the parent contract. 
+    Postconditions are asserted during the verification of a module and 
+    assumed during the verification of an instance of a module.
+  }];
+}
+
 #endif // CIRCT_DIALECT_VERIF_VERIFOPS_TD

lib/Dialect/Verif/VerifOps.cpp

@@ -93,6 +93,65 @@ LogicalResult CoverOp::canonicalize(CoverOp op, PatternRewriter &rewriter) {
   return AssertLikeOp::canonicalize<ClockedCoverOp>(op, rewriter);
 }
 
+//===----------------------------------------------------------------------===//
+// Formal contract verifiers
+//===----------------------------------------------------------------------===//
+
+LogicalResult ContractOp::verifyRegions() {
+  // Retrieve the number of inputs from the parent module
+  auto parent = (*this)->getParentOfType<hw::HWModuleOp>();
+  // Sanity check: parent should always be a hw.module
+  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())
+    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!";
+
+  return success();
+}
+
 //===----------------------------------------------------------------------===//
 // LogicalEquivalenceCheckingOp
 //===----------------------------------------------------------------------===//

test/Dialect/Verif/basic.mlir

@@ -53,9 +53,75 @@ verif.formal @formal1(k = 20) {
   // CHECK: %8 = verif.concrete_input %[[C1]], %[[CLK_U]] : i1
   %8 = verif.concrete_input %c1_i1, %clk_update : i1
   // CHECK: %foo.0, %foo.1 = hw.instance "foo" @Foo("0": %6: i1, "1": %8: i1) -> ("": i1, "1": i1)
-  %foo.0, %foo.1 = hw.instance "foo" @Foo("0": %sym: i1, "1": %8 : i1)  -> ("" : i1, "1" : i1)
+  %foo.0, %foo.1 = hw.instance "foo" @Foo("0": %sym: i1, "1": %8 : i1) -> ("" : i1, "1" : i1)
 }
 
+// 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: %[[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.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: 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-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.