[FIRRTL] Add contract declaration

Add `contract` declaration support to the FIRRTL parser, and a
corresponding operation to the FIRRTL dialect. A contract acts like a
`node`, but allows for additional formal properties to be expressed in
the contract body. The contract can then either be treated as a node for
synthesis, where the formal properties are just discarded, or it can be
used to subdivide a larger formal problem using a combination of the
assume-guarantee and cutpointing techniques commonly used in formal
verification tools.

This has not landed in the FIRRTL spec yet. As soon as that happens, I
will replace the `missingSpecFIRVersion` use with the actual spec
version.

Actual lowering follows in a separate commit.

include/circt/Dialect/FIRRTL/FIRRTLDeclarations.td

@@ -37,8 +37,14 @@ class ReferableDeclOp<string mnemonic, list<Trait> traits = []> :
 class HardwareDeclOp<string mnemonic, list <Trait> traits = []> :
   ReferableDeclOp<mnemonic, traits # [
     ParentOneOf<[
-      "firrtl::FModuleOp", "firrtl::LayerBlockOp",
-      "firrtl::WhenOp", "firrtl::MatchOp", "sv::IfDefOp"]>]> {}
+      "firrtl::ContractOp",
+      "firrtl::FModuleOp",
+      "firrtl::LayerBlockOp",
+      "firrtl::MatchOp",
+      "firrtl::WhenOp",
+      "sv::IfDefOp",
+    ]>
+  ]> {}
 
 def InstanceOp : HardwareDeclOp<"instance", [
     DeclareOpInterfaceMethods<FInstanceLike>,
@@ -650,6 +656,27 @@ def WireOp : HardwareDeclOp<"wire", [
   }];
 }
 
+def ContractOp : FIRRTLOp<"contract", [
+  SingleBlock,
+  NoTerminator,
+  AllTypesMatch<["inputs", "outputs"]>,
+]> {
+  let summary = "Contract declaration";
+  let description = [{
+    The `firrtl.contract` operation defines values that adhere to a set of
+    formal assertions and assumptions outlined in the contract's body.
+
+    See the `verif.contract` operation for more details.
+  }];
+  let arguments = (ins Variadic<PassiveType>:$inputs);
+  let results = (outs Variadic<PassiveType>:$outputs);
+  let regions = (region SizedRegion<1>:$body);
+  let assemblyFormat = [{
+    ($inputs^ `:` type($inputs))? attr-dict-with-keyword $body
+  }];
+  let hasVerifier = 1;
+}
+
 //===----------------------------------------------------------------------===//
 // Property Ops
 //===----------------------------------------------------------------------===//

include/circt/Dialect/FIRRTL/FIRRTLVisitors.h

@@ -309,7 +309,7 @@ class DeclVisitor {
     auto *thisCast = static_cast<ConcreteType *>(this);
     return TypeSwitch<Operation *, ResultType>(op)
         .template Case<InstanceOp, InstanceChoiceOp, ObjectOp, MemOp, NodeOp,
-                       RegOp, RegResetOp, WireOp, VerbatimWireOp>(
+                       RegOp, RegResetOp, WireOp, VerbatimWireOp, ContractOp>(
             [&](auto opNode) -> ResultType {
               return thisCast->visitDecl(opNode, args...);
             })
@@ -344,6 +344,7 @@ class DeclVisitor {
   HANDLE(RegResetOp);
   HANDLE(WireOp);
   HANDLE(VerbatimWireOp);
+  HANDLE(ContractOp);
 #undef HANDLE
 };
 

lib/Dialect/FIRRTL/FIRRTLOps.cpp

@@ -3429,6 +3429,16 @@ LogicalResult WireOp::verifySymbolUses(SymbolTableCollection &symbolTable) {
       symbolTable, Twine("'") + getOperationName() + "' op is");
 }
 
+//===----------------------------------------------------------------------===//
+// ContractOp
+//===----------------------------------------------------------------------===//
+
+LogicalResult ContractOp::verify() {
+  if (getBody().getArgumentTypes() != getInputs().getType())
+    return emitOpError("result types and region argument types must match");
+  return success();
+}
+
 //===----------------------------------------------------------------------===//
 // ObjectOp
 //===----------------------------------------------------------------------===//

lib/Dialect/FIRRTL/Import/FIRParser.cpp

@@ -1935,6 +1935,7 @@ struct FIRStmtParser : public FIRParser {
   ParseResult parseWire();
   ParseResult parseRegister(unsigned regIndent);
   ParseResult parseRegisterWithReset();
+  ParseResult parseContract(unsigned blockIndent);
 
   // Helper to fetch a module referenced by an instance-like statement.
   FModuleLike getReferencedModule(SMLoc loc, StringRef moduleName);
@@ -2667,6 +2668,7 @@ ParseResult FIRStmtParser::parseSimpleStmt(unsigned stmtIndent) {
 ///      ::= cmem | smem | mem
 ///      ::= node | wire
 ///      ::= register
+///      ::= contract
 ///
 ParseResult FIRStmtParser::parseSimpleStmtImpl(unsigned stmtIndent) {
   auto kind = getToken().getKind();
@@ -2776,6 +2778,8 @@ ParseResult FIRStmtParser::parseSimpleStmtImpl(unsigned stmtIndent) {
     return parseRegister(stmtIndent);
   case FIRToken::kw_regreset:
     return parseRegisterWithReset();
+  case FIRToken::kw_contract:
+    return parseContract(stmtIndent);
   }
 }
 
@@ -4731,6 +4735,79 @@ ParseResult FIRStmtParser::parseRegisterWithReset() {
   return moduleContext.addSymbolEntry(id, result, startTok.getLoc());
 }
 
+/// contract ::= 'contract' (id,+ '=' exp,+) ':' info? contract_body
+/// contract_body ::= simple_stmt | INDENT simple_stmt+ DEDENT
+ParseResult FIRStmtParser::parseContract(unsigned blockIndent) {
+  if (requireFeature(missingSpecFIRVersion, "contracts"))
+    return failure();
+
+  auto startTok = consumeToken(FIRToken::kw_contract);
+
+  // Parse the contract results and expressions.
+  SmallVector<StringRef> ids;
+  SmallVector<SMLoc> locs;
+  SmallVector<Value> values;
+  SmallVector<Type> types;
+  if (!consumeIf(FIRToken::colon)) {
+    auto parseContractId = [&] {
+      StringRef id;
+      locs.push_back(getToken().getLoc());
+      if (parseId(id, "expected contract result name"))
+        return failure();
+      ids.push_back(id);
+      return success();
+    };
+    auto parseContractValue = [&] {
+      Value value;
+      if (parseExp(value, "expected expression for contract result"))
+        return failure();
+      values.push_back(value);
+      types.push_back(value.getType());
+      return success();
+    };
+    if (parseListUntil(FIRToken::equal, parseContractId) ||
+        parseListUntil(FIRToken::colon, parseContractValue))
+      return failure();
+  }
+  if (parseOptionalInfo())
+    return failure();
+
+  // Each result must have a corresponding expression assigned.
+  if (ids.size() != values.size())
+    return emitError(startTok.getLoc())
+           << "contract requires same number of results and expressions; got "
+           << ids.size() << " results and " << values.size()
+           << " expressions instead";
+
+  locationProcessor.setLoc(startTok.getLoc());
+
+  // Add block arguments for each result and declare their names in a subscope
+  // for the contract body.
+  auto contract = builder.create<ContractOp>(types, values);
+  auto &block = contract.getBody().emplaceBlock();
+
+  // Parse the contract body.
+  {
+    FIRModuleContext::ContextScope scope(moduleContext, &block);
+    for (auto [id, loc, type] : llvm::zip(ids, locs, types)) {
+      auto arg = block.addArgument(type, LocWithInfo(loc, this).getLoc());
+      if (failed(moduleContext.addSymbolEntry(id, arg, loc)))
+        return failure();
+    }
+    if (getIndentation() > blockIndent)
+      if (parseSubBlock(block, blockIndent, SymbolRefAttr{}))
+        return failure();
+  }
+
+  // Declare the results.
+  for (auto [id, loc, value, result] :
+       llvm::zip(ids, locs, values, contract.getResults()))
+    if (failed(moduleContext.addSymbolEntry(id, result, loc)))
+      return failure();
+
+  return success();
+}
+
 //===----------------------------------------------------------------------===//
 // FIRCircuitParser
 //===----------------------------------------------------------------------===//

lib/Dialect/FIRRTL/Import/FIRTokenKinds.def

@@ -37,7 +37,8 @@
 #define TOK_LPKEYWORD(SPELLING)
 #endif
 #ifndef TOK_LPKEYWORD_PRIM
-#define TOK_LPKEYWORD_PRIM(SPELLING, CLASS, NUMOPERANDS, NUMATTRIBUTES) TOK_LPKEYWORD(SPELLING)
+#define TOK_LPKEYWORD_PRIM(SPELLING, CLASS, NUMOPERANDS, NUMATTRIBUTES)        \
+  TOK_LPKEYWORD(SPELLING)
 #endif
 
 // Markers
@@ -108,6 +109,7 @@ TOK_KEYWORD(class)
 TOK_KEYWORD(cmem)
 TOK_KEYWORD(connect)
 TOK_KEYWORD(const)
+TOK_KEYWORD(contract)
 TOK_KEYWORD(declgroup)
 TOK_KEYWORD(define)
 TOK_KEYWORD(defname)

test/Dialect/FIRRTL/errors.mlir

@@ -279,7 +279,7 @@ firrtl.circuit "Foo" {
 
 firrtl.circuit "Foo" {
   firrtl.extmodule @Foo()
-  // expected-error @+1 {{'firrtl.instance' op expects parent op to be one of 'firrtl.module, firrtl.layerblock, firrtl.when, firrtl.match, sv.ifdef'}}
+  // expected-error @+1 {{'firrtl.instance' op expects parent op to be one of 'firrtl.contract, firrtl.module, firrtl.layerblock, firrtl.match, firrtl.when, sv.ifdef'}}
   firrtl.instance "" @Foo()
 }
 
@@ -1819,7 +1819,7 @@ firrtl.circuit "ClassCannotHaveHardwarePorts" {
 firrtl.circuit "ClassCannotHaveWires" {
   firrtl.module @ClassCannotHaveWires() {}
   firrtl.class @ClassWithWire() {
-    // expected-error @below {{'firrtl.wire' op expects parent op to be one of 'firrtl.module, firrtl.layerblock, firrtl.when, firrtl.match, sv.ifdef'}}
+    // expected-error @below {{'firrtl.wire' op expects parent op to be one of 'firrtl.contract, firrtl.module, firrtl.layerblock, firrtl.match, firrtl.when, sv.ifdef'}}
     %w = firrtl.wire : !firrtl.uint<8>
   }
 }
@@ -2626,3 +2626,36 @@ firrtl.circuit "MultipleDUTModules" {
     ]
   } {}
 }
+
+// -----
+
+firrtl.circuit "Foo" {
+  firrtl.module @Foo(in %a: !firrtl.uint<42>) {
+    // expected-error @below {{result types and region argument types must match}}
+    firrtl.contract %a : !firrtl.uint<42> {
+    ^bb0:
+    }
+  }
+}
+
+// -----
+
+firrtl.circuit "Foo" {
+  firrtl.module @Foo(in %a: !firrtl.uint<42>) {
+    // expected-error @below {{result types and region argument types must match}}
+    firrtl.contract {
+    ^bb0(%arg0: !firrtl.uint<1337>):
+    }
+  }
+}
+
+// -----
+
+firrtl.circuit "Foo" {
+  firrtl.module @Foo(in %a: !firrtl.uint<42>) {
+    // expected-error @below {{result types and region argument types must match}}
+    firrtl.contract %a : !firrtl.uint<42> {
+    ^bb0(%arg0: !firrtl.uint<1337>):
+    }
+  }
+}

test/Dialect/FIRRTL/parse-basic.fir

@@ -1978,3 +1978,48 @@ circuit Foo:
     bar is invalid
 
     b <= a
+
+;// -----
+FIRRTL version 4.2.0
+; CHECK-LABEL: firrtl.circuit "Contracts"
+circuit Contracts:
+  ; CHECK-LABEL: firrtl.module @Contracts(
+  ; CHECK-SAME:    in %a: !firrtl.uint<42>
+  ; CHECK-SAME:    in %b: !firrtl.uint<1337>
+  ; CHECK-SAME:    in %c: !firrtl.bundle<x: uint<4>, y: uint<5>>
+  ; CHECK-SAME:  )
+  public module Contracts:
+    input a : UInt<42>
+    input b : UInt<1337>
+    input c : {x: UInt<4>, y: UInt<5>}
+
+    ; CHECK:      firrtl.contract {
+    ; CHECK-NEXT: }
+    contract: @[FooBar.scala 369:27]
+
+    ; CHECK:      [[C1:%.+]] = firrtl.contract %a : !firrtl.uint<42> {
+    ; CHECK-NEXT: ^bb0(%arg0: !firrtl.uint<42>):
+    ; CHECK-NEXT:   %t2 = firrtl.node {{.+}} %arg0 : !firrtl.uint<42>
+    ; CHECK-NEXT: }
+    contract t = a:
+      node t2 = t
+
+    ; CHECK:      [[C2:%.+]]:3 = firrtl.contract %a, %b, %c : !firrtl.uint<42>, !firrtl.uint<1337>, !firrtl.bundle<x: uint<4>, y: uint<5>> {
+    ; CHECK-NEXT: ^bb0(%arg0: !firrtl.uint<42>, %arg1: !firrtl.uint<1337>, %arg2: !firrtl.bundle<x: uint<4>, y: uint<5>>):
+    ; CHECK-NEXT:   %u2 = firrtl.node {{.+}} %arg0 : !firrtl.uint<42>
+    ; CHECK-NEXT:   %v2 = firrtl.node {{.+}} %arg1 : !firrtl.uint<1337>
+    ; CHECK-NEXT:   %w2 = firrtl.node {{.+}} %arg2 : !firrtl.bundle<x: uint<4>, y: uint<5>>
+    ; CHECK-NEXT: }
+    contract u, v, w = a, b, c:
+      node u2 = u
+      node v2 = v
+      node w2 = w
+
+    ; CHECK: %t3 = firrtl.node {{.+}} [[C1]] : !firrtl.uint<42>
+    ; CHECK: %u3 = firrtl.node {{.+}} [[C2]]#0 : !firrtl.uint<42>
+    ; CHECK: %v3 = firrtl.node {{.+}} [[C2]]#1 : !firrtl.uint<1337>
+    ; CHECK: %w3 = firrtl.node {{.+}} [[C2]]#2 : !firrtl.bundle<x: uint<4>, y: uint<5>>
+    node t3 = t
+    node u3 = u
+    node v3 = v
+    node w3 = w

test/Dialect/FIRRTL/parse-errors.fir

@@ -1660,3 +1660,10 @@ circuit Foo:
   ; expected-error @below {{inline layers are a FIRRTL 4.1.0+ feature}}
   layer A, inline:
   public module Foo:
+
+;// -----
+FIRRTL version 4.1.0
+circuit Top:
+  public module Top:
+    ; expected-error @below {{contracts are a FIRRTL 4.2.0+ feature}}
+    contract:

test/Dialect/FIRRTL/round-trip.mlir

@@ -162,4 +162,18 @@ firrtl.formal @myTestB, @Top {bound = 42 : i19}
 // CHECK: firrtl.formal @myTestC, @Top {} attributes {foo}
 firrtl.formal @myTestC, @Top {} attributes {foo}
 
+// CHECK-LABEL: firrtl.module @Contracts
+firrtl.module @Contracts(in %a: !firrtl.uint<42>, in %b: !firrtl.bundle<x: uint<1337>>) {
+  // CHECK: firrtl.contract {
+  // CHECK: }
+  firrtl.contract {}
+
+  // CHECK: {{%.+}}:2 = firrtl.contract %a, %b : !firrtl.uint<42>, !firrtl.bundle<x: uint<1337>> {
+  // CHECK: ^bb0(%arg0: !firrtl.uint<42>, %arg1: !firrtl.bundle<x: uint<1337>>):
+  // CHECK: }
+  firrtl.contract %a, %b : !firrtl.uint<42>, !firrtl.bundle<x: uint<1337>> {
+  ^bb0(%arg0: !firrtl.uint<42>, %arg1: !firrtl.bundle<x: uint<1337>>):
+  }
+}
+
 }