[FIRRTL] Add Inline Formal Test ops

include/circt/Dialect/FIRRTL/FIRRTLDeclarations.td

@@ -36,10 +36,49 @@ class ReferableDeclOp<string mnemonic, list<Trait> traits = []> :
 /// located in a hardware-creating context, such as the body of a module.
 class HardwareDeclOp<string mnemonic, list <Trait> traits = []> :
   ReferableDeclOp<mnemonic, traits # [
-    ParentOneOf<[
+    ParentOneOf<[ 
       "firrtl::FModuleOp", "firrtl::LayerBlockOp",
       "firrtl::WhenOp", "firrtl::MatchOp", "sv::IfDefOp"]>]> {}
 
+def FormalOp : ReferableDeclOp<"formal", [
+    HasParent<"firrtl::CircuitOp">,
+    DeclareOpInterfaceMethods<SymbolUserOpInterface>
+]> {
+  let summary = "A formal test definition.";
+  let description = [{
+    The `firrtl.formal` operation defines a formal verification problem in the same 
+    context as the rest of the design. This problem is solved using bounded model 
+    checking and should be given a bound k, which represents the number of cycles considered 
+    during model checking.
+
+    Example:
+    ```mlir
+
+    // DUT
+    firrtl.module @Foo(in %bar: !firrtl.uint<8>, out %out: !firrtl.uint<8>) { ... }
+
+    // Test harness
+    firrtl.module @FooTest(in %bar_s: !firrtl.uint<8>) {
+      %bar, %out = firrtl.instance foo @Foo(in bar: %bar_s: !firrtl.uint<8>, out out: !firrtl.uint<8>) 
+      %c42_8 = firrtl.constant 42 : !firrtl.uint<8>
+      firrtl.connect %bar, %c42_8: !firrtl.uint<8>, !firrtl.uint<8>
+      %c69_8 = firrtl.constant 69 : !firrtl.uint<8>
+      %cond = firrtl.eq %c69_8, %out : (!firrtl.uint<8>, !firrtl.uint<8>) -> !firrtl.uint<1>
+      firrtl.assert %cond
+    }
+
+    // Mark test harness as formal test
+    firrtl.formal @formal1 of @FooTest bound 20
+    ```
+  }];
+
+  let arguments = (ins SymbolNameAttr:$sym_name, FlatSymbolRefAttr:$moduleName, UI64Attr:$bound);
+  let results = (outs);
+  let assemblyFormat = [{
+    $sym_name `of` $moduleName `bound` $bound attr-dict
+  }];
+}
+
 def InstanceOp : HardwareDeclOp<"instance", [
     DeclareOpInterfaceMethods<FInstanceLike>,
     DeclareOpInterfaceMethods<SymbolUserOpInterface>,

lib/Dialect/FIRRTL/Export/FIREmitter.cpp

@@ -60,6 +60,7 @@ struct Emitter {
   void emitModuleParameters(Operation *op, ArrayAttr parameters);
   void emitDeclaration(LayerOp op);
   void emitDeclaration(OptionOp op);
+  void emitDeclaration(FormalOp op);
   void emitEnabledLayers(ArrayRef<Attribute> layers);
 
   void emitParamAssign(ParamDeclAttr param, Operation *op,
@@ -406,6 +407,7 @@ void Emitter::emitCircuit(CircuitOp op) {
           })
           .Case<LayerOp>([&](auto op) { emitDeclaration(op); })
           .Case<OptionOp>([&](auto op) { emitDeclaration(op); })
+          .Case<FormalOp>([&](auto op) { emitDeclaration(op); })
           .Default([&](auto op) {
             emitOpError(op, "not supported for emission inside circuit");
           });
@@ -623,6 +625,21 @@ void Emitter::emitDeclaration(OptionOp op) {
   ps << PP::newline << PP::newline;
 }
 
+/// Emit a formal test definition.
+void Emitter::emitDeclaration(FormalOp op) {
+  startStatement();
+  ps << "formal " << PPExtString(op.getSymName()) << " of "
+     << PPExtString(op.getModuleName()) << ", bound = ";
+  ps.addAsString(op.getBound());
+
+  if (auto outputFile = op->getAttrOfType<hw::OutputFileAttr>("output_file")) {
+    ps << ", ";
+    ps.writeQuotedEscaped(outputFile.getFilename().getValue());
+  }
+
+  emitLocationAndNewLine(op);
+}
+
 /// Check if an operation is inlined into the emission of their users. For
 /// example, subfields are always inlined.
 static bool isEmittedInline(Operation *op) {

lib/Dialect/FIRRTL/FIRRTLOps.cpp

@@ -3360,6 +3360,40 @@ void RegResetOp::getAsmResultNames(OpAsmSetValueNameFn setNameFn) {
   return forceableAsmResultNames(*this, getName(), setNameFn);
 }
 
+//===----------------------------------------------------------------------===//
+// FormalOp
+//===----------------------------------------------------------------------===//
+
+LogicalResult
+FormalOp::verifySymbolUses(::mlir::SymbolTableCollection &symbolTable) {
+  auto referencedModule = symbolTable.lookupNearestSymbolFrom<FModuleLike>(
+      *this, getModuleNameAttr());
+  if (!referencedModule) {
+    return (*this)->emitOpError("invalid symbol reference");
+  }
+
+  // Check this is not a class.
+  if (isa<ClassOp>(referencedModule))
+    return (*this)
+               ->emitOpError("must instantiate a module not a class")
+               .attachNote(referencedModule.getLoc())
+           << "class declared here";
+  return success();
+}
+
+std::optional<size_t> FormalOp::getTargetResultIndex() {
+  // Inner symbols on instance operations target the op not any result.
+  return std::nullopt;
+}
+
+void FormalOp::getAsmResultNames(OpAsmSetValueNameFn setNameFn) {
+  /* Don't do anything because Formal doesn't have any results */
+}
+
+//===----------------------------------------------------------------------===//
+// WireOp
+//===----------------------------------------------------------------------===//
+
 void WireOp::getAsmResultNames(OpAsmSetValueNameFn setNameFn) {
   return forceableAsmResultNames(*this, getName(), setNameFn);
 }
@@ -3382,6 +3416,10 @@ LogicalResult WireOp::verifySymbolUses(SymbolTableCollection &symbolTable) {
       symbolTable, Twine("'") + getOperationName() + "' op is");
 }
 
+//===----------------------------------------------------------------------===//
+// ObjectOp
+//===----------------------------------------------------------------------===//
+
 void ObjectOp::build(OpBuilder &builder, OperationState &state, ClassLike klass,
                      StringRef name) {
   build(builder, state, klass.getInstanceType(),

lib/Dialect/FIRRTL/Import/FIRParser.cpp

@@ -4585,6 +4585,7 @@ struct FIRCircuitParser : public FIRParser {
   ParseResult parseExtModule(CircuitOp circuit, unsigned indent);
   ParseResult parseIntModule(CircuitOp circuit, unsigned indent);
   ParseResult parseModule(CircuitOp circuit, bool isPublic, unsigned indent);
+  ParseResult parseFormal(CircuitOp circuit, unsigned indent);
 
   ParseResult parseLayerName(SymbolRefAttr &result);
   ParseResult parseOptionalEnabledLayers(ArrayAttr &result);
@@ -4890,6 +4891,7 @@ ParseResult FIRCircuitParser::skipToModuleEnd(unsigned indent) {
     case FIRToken::kw_extclass:
     case FIRToken::kw_extmodule:
     case FIRToken::kw_intmodule:
+    case FIRToken::kw_formal:
     case FIRToken::kw_module:
     case FIRToken::kw_public:
     case FIRToken::kw_layer:
@@ -5153,6 +5155,41 @@ ParseResult FIRCircuitParser::parseModule(CircuitOp circuit, bool isPublic,
   return success();
 }
 
+ParseResult FIRCircuitParser::parseFormal(CircuitOp circuit, unsigned indent) {
+  auto startLoc = getToken().getLoc();
+  consumeToken(FIRToken::kw_formal);
+  StringRef id, moduleName, boundSpelling;
+  int64_t bound = -1;
+  LocWithInfo info(getToken().getLoc(), this);
+
+  // Parse the formal operation
+  if (parseId(id, "expected a formal test name") ||
+      parseToken(FIRToken::kw_of,
+                 "expected keyword 'of' after formal test name") ||
+      parseId(moduleName, "expected the name of a module") ||
+      parseToken(FIRToken::comma, "expected ','") ||
+      parseGetSpelling(boundSpelling) ||
+      parseToken(FIRToken::identifier,
+                 "expected parameter 'bound' after ','") ||
+      parseToken(FIRToken::equal, "expected '=' after 'bound'") ||
+      parseIntLit(bound, "expected integer in bound specification") ||
+      info.parseOptionalInfo())
+    return failure();
+
+  // Check that the parameter is valid
+  if (boundSpelling != "bound" || bound <= 0)
+    return emitError("Invalid parameter given to formal test: ")
+               << boundSpelling << " = " << bound,
+           failure();
+
+  // Build out the firrtl mlir op
+  auto builder = circuit.getBodyBuilder();
+  auto formal =
+      builder.create<firrtl::FormalOp>(info.getLoc(), id, moduleName, bound);
+
+  return success();
+}
+
 ParseResult FIRCircuitParser::parseToplevelDefinition(CircuitOp circuit,
                                                       unsigned indent) {
   switch (getToken().getKind()) {
@@ -5167,6 +5204,10 @@ ParseResult FIRCircuitParser::parseToplevelDefinition(CircuitOp circuit,
     return parseExtClass(circuit, indent);
   case FIRToken::kw_extmodule:
     return parseExtModule(circuit, indent);
+  case FIRToken::kw_formal:
+    if (requireFeature({4, 0, 0}, "inline formal tests"))
+      return failure();
+    return parseFormal(circuit, indent);
   case FIRToken::kw_intmodule:
     if (removedFeature({4, 0, 0}, "intrinsic modules"))
       return failure();
@@ -5514,6 +5555,7 @@ ParseResult FIRCircuitParser::parseCircuit(
     case FIRToken::kw_extmodule:
     case FIRToken::kw_intmodule:
     case FIRToken::kw_layer:
+    case FIRToken::kw_formal:
     case FIRToken::kw_module:
     case FIRToken::kw_option:
     case FIRToken::kw_public:

lib/Dialect/FIRRTL/Import/FIRTokenKinds.def

@@ -117,6 +117,7 @@ TOK_KEYWORD(extclass)
 TOK_KEYWORD(extmodule)
 TOK_KEYWORD(false)
 TOK_KEYWORD(flip)
+TOK_KEYWORD(formal)
 TOK_KEYWORD(group)
 TOK_KEYWORD(infer)
 TOK_KEYWORD(input)
@@ -151,6 +152,7 @@ TOK_KEYWORD(regreset)
 TOK_KEYWORD(reset)
 TOK_KEYWORD(skip)
 TOK_KEYWORD(smem)
+TOK_KEYWORD(symbolic)
 TOK_KEYWORD(true)
 TOK_KEYWORD(type)
 TOK_KEYWORD(undefined)

test/Dialect/FIRRTL/parse-basic.fir

@@ -1907,3 +1907,41 @@ circuit GenericIntrinsics:
     ; CHECK-NEXT: %[[SZ:.+]] = firrtl.int.generic "circt_isX"
     ; CHECK-NEXT: "circt_verif_assert" %[[SZ]]
     intrinsic(circt_verif_assert, intrinsic(circt_isX: UInt<1>, data))
+
+;// -----
+FIRRTL version 4.0.0
+; CHECK-LABEL: circuit "Foo"
+circuit Foo:
+
+  ; CHECK-LABEL: firrtl.module @Foo(in %data: !firrtl.uint<32>, in %c: !firrtl.uint<1>, out %out: !firrtl.uint<32>)
+  public module Foo:
+    input data : UInt<32>
+    input c : UInt<1>
+    output out : UInt<32>
+
+    when c:
+      node add1 = add(data, UInt<32>(1))
+      out <= add1
+    else:
+      out <= data
+
+  ; CHECK-LABEL: firrtl.module @FooTest(in %s_foo_c: !firrtl.uint<1>, in %s_foo_data: !firrtl.uint<32>)
+  public module FooTest:
+    input s_foo_c : UInt<1>
+    input s_foo_data : UInt<32>
+
+    ; CHECK-NEXT: %foo_data, %foo_c, %foo_out = firrtl.instance foo interesting_name @Foo(in data: !firrtl.uint<32>, in c: !firrtl.uint<1>, out out: !firrtl.uint<32>)
+    inst foo of Foo
+    ; CHECK-NEXT: firrtl.matchingconnect %foo_c, %s_foo_c : !firrtl.uint<1>
+    connect foo.c, s_foo_c
+    ; CHECK-NEXT: firrtl.matchingconnect %foo_data, %s_foo_data : !firrtl.uint<32>
+    connect foo.data, s_foo_data
+    ; CHECK-NEXT: %0 = firrtl.eq %foo_out, %s_foo_data : (!firrtl.uint<32>, !firrtl.uint<32>) -> !firrtl.uint<1>
+    ; CHECK-NEXT: %1 = firrtl.int.generic "circt_ltl_implication"  %s_foo_c, %0 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
+    ; CHECK-NEXT: firrtl.int.generic "circt_verif_assert"  %1 : (!firrtl.uint<1>) -> ()
+    intrinsic(circt_verif_assert, intrinsic(circt_ltl_implication : UInt<1>, s_foo_c, eq(foo.out, s_foo_data)))
+
+  ; CHECK: firrtl.formal @testFormal of @FooTest bound 20
+  formal testFormal of FooTest, bound = 20
+
+