[FIRRTL] Accept list of parameters for formal construct

include/circt/Dialect/FIRRTL/FIRRTLDeclarations.td

@@ -41,42 +41,38 @@ class HardwareDeclOp<string mnemonic, list <Trait> traits = []> :
       "firrtl::WhenOp", "firrtl::MatchOp", "sv::IfDefOp"]>]> {}
 
 def FormalOp : FIRRTLOp<"formal", [
-    HasParent<"firrtl::CircuitOp">,
-    DeclareOpInterfaceMethods<Symbol>,
-    DeclareOpInterfaceMethods<SymbolUserOpInterface>
+  HasParent<"firrtl::CircuitOp">,
+  DeclareOpInterfaceMethods<Symbol>,
+  DeclareOpInterfaceMethods<SymbolUserOpInterface>
 ]> {
-  let summary = "A formal test definition.";
+  let summary = "Define a formal unit test";
   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. This definition marks a test harness defined as an internal module to 
-    be verified using bounded model checking.
+    The `firrtl.formal` operation defines a formal verification unit test. The
+    defines a unique symbol name that can be used to refer to it. The design to
+    be tested and any necessary test harness is defined by the separate
+    `firrtl.module` op referenced by `moduleName`. Additional parameters may be
+    specified for the unit test. Input ports of the target module are considered
+    to be symbolic values during the test; output ports are ignored.
+
+    This operation may be used to mark unit tests in a FIRRTL design, which
+    other tools may later pick up and run automatically. It is intended to lower
+    to the `verif.formal` operation. See `verif.formal` for more details.
 
     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
+    firrtl.module @MyTest(in %a: !firrtl.uint<42>) {}
+    firrtl.formal @myTestA, @MyTest {bound = 42}
+    firrtl.formal @myTestB, @MyTest {mode = "induction", userAttr = 9001}
     ```
   }];
 
-  let arguments = (ins SymbolNameAttr:$sym_name, FlatSymbolRefAttr:$moduleName, UI64Attr:$bound);
-  let results = (outs);
+  let arguments = (ins
+    SymbolNameAttr:$sym_name,
+    FlatSymbolRefAttr:$moduleName,
+    DictionaryAttr:$parameters
+  );
   let assemblyFormat = [{
-    $sym_name `of` $moduleName `bound` $bound attr-dict
+    $sym_name `,` $moduleName $parameters attr-dict-with-keyword
   }];
 }
 

lib/Dialect/FIRRTL/Export/FIREmitter.cpp

@@ -65,6 +65,8 @@ struct Emitter {
 
   void emitParamAssign(ParamDeclAttr param, Operation *op,
                        std::optional<PPExtString> wordBeforeLHS = std::nullopt);
+  void emitParamValue(Attribute value, Operation *op);
+
   void emitGenericIntrinsic(GenericIntrinsicOp op);
 
   // Statement emission
@@ -433,7 +435,11 @@ void Emitter::emitParamAssign(ParamDeclAttr param, Operation *op,
     ps << *wordBeforeLHS << PP::nbsp;
   }
   ps << PPExtString(param.getName().strref()) << PP::nbsp << "=" << PP::nbsp;
-  TypeSwitch<Attribute>(param.getValue())
+  emitParamValue(param.getValue(), op);
+}
+
+void Emitter::emitParamValue(Attribute value, Operation *op) {
+  TypeSwitch<Attribute>(value)
       .Case<IntegerAttr>([&](auto attr) { ps.addAsString(attr.getValue()); })
       .Case<FloatAttr>([&](auto attr) {
         SmallString<16> str;
@@ -442,6 +448,24 @@ void Emitter::emitParamAssign(ParamDeclAttr param, Operation *op,
       })
       .Case<StringAttr>(
           [&](auto attr) { ps.writeQuotedEscaped(attr.getValue()); })
+      .Case<ArrayAttr>([&](auto attr) {
+        ps.scopedBox(PP::bbox2, [&]() {
+          ps << "[";
+          interleaveComma(attr.getValue(),
+                          [&](auto element) { emitParamValue(element, op); });
+          ps << "]";
+        });
+      })
+      .Case<DictionaryAttr>([&](auto attr) {
+        ps.scopedBox(PP::bbox2, [&]() {
+          ps << "{";
+          interleaveComma(attr.getValue(), [&](auto field) {
+            ps << PPExtString(field.getName()) << PP::nbsp << "=" << PP::nbsp;
+            emitParamValue(field.getValue(), op);
+          });
+          ps << "}";
+        });
+      })
       .Default([&](auto attr) {
         emitOpError(op, "with unsupported parameter attribute: ") << attr;
         ps << "<unsupported-attr ";
@@ -628,16 +652,21 @@ void Emitter::emitDeclaration(OptionOp op) {
 /// 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());
-  }
+  ps.cbox(4, IndentStyle::Block);
+  ps << "formal " << PPExtString(legalize(op.getSymNameAttr()));
+  ps << " of " << PPExtString(legalize(op.getModuleNameAttr().getAttr()));
+  ps << PP::nbsp << ":" << PP::end;
+  emitLocation(op);
 
-  emitLocationAndNewLine(op);
+  ps.scopedBox(PP::bbox2, [&]() {
+    setPendingNewline();
+    for (auto param : op.getParameters()) {
+      startStatement();
+      ps << PPExtString(param.getName()) << PP::nbsp << "=" << PP::nbsp;
+      emitParamValue(param.getValue(), op);
+      setPendingNewline();
+    }
+  });
 }
 
 /// Check if an operation is inlined into the emission of their users. For