[FIRRTL] Lower firrtl.formal to verif.formal

Add a lowering from `firrtl.formal` to `verif.formal` in the
FIRRTL-to-HW conversion. The lowering creates a `verif.formal` op that
simply instantiates the module pointed to by `firrtl.formal`, with
symbolic values providing the inputs to the module. We may want to
inline the instance in the future, but that is purely cosmetic.

This now allows FIR files to contain `formal` unti tests that can be
lowered to HW through `firtool` and then executed using `circt-test`.

lib/Conversion/FIRRTLToHW/LowerToHW.cpp

@@ -578,6 +578,8 @@ struct FIRRTLModuleLowering
                               CircuitLoweringState &loweringState);
   LogicalResult lowerModuleOperations(hw::HWModuleOp module,
                                       CircuitLoweringState &loweringState);
+  LogicalResult lowerFormalBody(verif::FormalOp formalOp,
+                                CircuitLoweringState &loweringState);
 };
 
 } // end anonymous namespace
@@ -620,6 +622,7 @@ void FIRRTLModuleLowering::runOnOperation() {
                              &getAnalysis<NLATable>());
 
   SmallVector<hw::HWModuleOp, 32> modulesToProcess;
+  SmallVector<verif::FormalOp> formalOpsToProcess;
 
   AnnotationSet circuitAnno(circuit);
   moveVerifAnno(getOperation(), circuitAnno, extractAssertAnnoClass,
@@ -670,6 +673,16 @@ void FIRRTLModuleLowering::runOnOperation() {
               state.recordModuleMapping(&op, loweredMod);
               return success();
             })
+            .Case<FormalOp>([&](auto oldFormalOp) {
+              auto builder = OpBuilder::atBlockEnd(topLevelModule);
+              auto newFormalOp = builder.create<verif::FormalOp>(
+                  oldFormalOp.getLoc(), oldFormalOp.getNameAttr());
+              newFormalOp->setDiscardableAttrs(oldFormalOp.getParametersAttr());
+              newFormalOp.getBody().emplaceBlock();
+              state.recordModuleMapping(oldFormalOp, newFormalOp);
+              formalOpsToProcess.push_back(newFormalOp);
+              return success();
+            })
             .Default([&](Operation *op) {
               // We don't know what this op is.  If it has no illegal FIRRTL
               // types, we can forward the operation.  Otherwise, we emit an
@@ -725,13 +738,18 @@ void FIRRTLModuleLowering::runOnOperation() {
         ->setAttr(moduleHierarchyFileAttrName,
                   ArrayAttr::get(&getContext(), testHarnessHierarchyFiles));
 
-  // Finally, lower all operations.
+  // Lower all module bodies.
   auto result = mlir::failableParallelForEachN(
       &getContext(), 0, modulesToProcess.size(), [&](auto index) {
         return lowerModuleOperations(modulesToProcess[index], state);
       });
+  if (failed(result))
+    return signalPassFailure();
 
-  // If any module bodies failed to lower, return early.
+  // Lower all formal op bodies.
+  result = mlir::failableParallelForEach(
+      &getContext(), formalOpsToProcess,
+      [&](auto op) { return lowerFormalBody(op, state); });
   if (failed(result))
     return signalPassFailure();
 
@@ -1390,6 +1408,38 @@ LogicalResult FIRRTLModuleLowering::lowerModulePortsAndMoveBody(
   return success();
 }
 
+/// Run on each `verif.formal` to populate its body based on the original
+/// `firrtl.formal` operation.
+LogicalResult
+FIRRTLModuleLowering::lowerFormalBody(verif::FormalOp formalOp,
+                                      CircuitLoweringState &loweringState) {
+  auto builder = OpBuilder::atBlockEnd(&formalOp.getBody().front());
+
+  // Find the module targeted by the `firrtl.formal` operation. The `FormalOp`
+  // verifier guarantees the module exists and that it is an `FModuleOp`. This
+  // we can then translate to the corresponding `HWModuleOp`.
+  auto oldFormalOp = cast<FormalOp>(loweringState.getOldModule(formalOp));
+  auto moduleName = oldFormalOp.getModuleNameAttr().getAttr();
+  auto oldModule = cast<FModuleOp>(
+      loweringState.getInstanceGraph().lookup(moduleName)->getModule());
+  auto newModule =
+      dyn_cast_or_null<hw::HWModuleOp>(loweringState.getNewModule(oldModule));
+  if (!newModule)
+    return oldFormalOp->emitOpError()
+           << "could not find module " << oldModule.getSymNameAttr();
+
+  // Create a symbolic input for every input of the lowered module.
+  SmallVector<Value> symbolicInputs;
+  for (auto arg : newModule.getBody().getArguments())
+    symbolicInputs.push_back(
+        builder.create<verif::SymbolicValueOp>(arg.getLoc(), arg.getType()));
+
+  // Instantiate the module with the given symbolic inputs.
+  builder.create<hw::InstanceOp>(formalOp.getLoc(), newModule,
+                                 newModule.getNameAttr(), symbolicInputs);
+  return success();
+}
+
 //===----------------------------------------------------------------------===//
 // Module Body Lowering Pass
 //===----------------------------------------------------------------------===//

test/Conversion/FIRRTLToHW/lower-to-hw.mlir

@@ -1699,3 +1699,24 @@ firrtl.circuit "Directories" attributes {
     firrtl.instance dut_A @Directories_A()
   }
 }
+
+// -----
+
+firrtl.circuit "Foo" {
+  // CHECK-LABEL: hw.module @Foo
+  // CHECK-SAME:    in %a : i42
+  // CHECK-SAME:    out z : i42
+  firrtl.module @Foo(in %a: !firrtl.uint<42>, out %z: !firrtl.uint<42>) {
+    firrtl.connect %z, %a : !firrtl.uint<42>
+  }
+  // CHECK: verif.formal @MyTest1
+  // CHECK-SAME: {hello = 42 : i64} {
+  // CHECK-NEXT: [[A:%.+]] = verif.symbolic_value : i42
+  // CHECK-NEXT: hw.instance "Foo" @Foo(a: [[A]]: i42) -> (z: i42)
+  firrtl.formal @MyTest1, @Foo {hello = 42 : i64}
+  // CHECK: verif.formal @MyTest2
+  // CHECK-SAME: {world = "abc"} {
+  // CHECK-NEXT: [[A:%.+]] = verif.symbolic_value : i42
+  // CHECK-NEXT: hw.instance "Foo" @Foo(a: [[A]]: i42) -> (z: i42)
+  firrtl.formal @MyTest2, @Foo {world = "abc"}
+}