From d17fa17c8487cb7bb95963b061cac8d5fc497623 Mon Sep 17 00:00:00 2001 From: Fabian Schuiki Date: Mon, 18 Nov 2024 16:46:48 -0800 Subject: [PATCH] [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 | 54 ++++++++++++++++++++- test/Conversion/FIRRTLToHW/lower-to-hw.mlir | 21 ++++++++ 2 files changed, 73 insertions(+), 2 deletions(-) diff --git a/lib/Conversion/FIRRTLToHW/LowerToHW.cpp b/lib/Conversion/FIRRTLToHW/LowerToHW.cpp index d818e1a65868..a6679471fbe7 100644 --- a/lib/Conversion/FIRRTLToHW/LowerToHW.cpp +++ b/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()); SmallVector modulesToProcess; + SmallVector formalOpsToProcess; AnnotationSet circuitAnno(circuit); moveVerifAnno(getOperation(), circuitAnno, extractAssertAnnoClass, @@ -670,6 +673,16 @@ void FIRRTLModuleLowering::runOnOperation() { state.recordModuleMapping(&op, loweredMod); return success(); }) + .Case([&](auto oldFormalOp) { + auto builder = OpBuilder::atBlockEnd(topLevelModule); + auto newFormalOp = builder.create( + 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(loweringState.getOldModule(formalOp)); + auto moduleName = oldFormalOp.getModuleNameAttr().getAttr(); + auto oldModule = cast( + loweringState.getInstanceGraph().lookup(moduleName)->getModule()); + auto newModule = + dyn_cast_or_null(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 symbolicInputs; + for (auto arg : newModule.getBody().getArguments()) + symbolicInputs.push_back( + builder.create(arg.getLoc(), arg.getType())); + + // Instantiate the module with the given symbolic inputs. + builder.create(formalOp.getLoc(), newModule, + newModule.getNameAttr(), symbolicInputs); + return success(); +} + //===----------------------------------------------------------------------===// // Module Body Lowering Pass //===----------------------------------------------------------------------===// diff --git a/test/Conversion/FIRRTLToHW/lower-to-hw.mlir b/test/Conversion/FIRRTLToHW/lower-to-hw.mlir index ed875c52962b..1b4e008a0f10 100644 --- a/test/Conversion/FIRRTLToHW/lower-to-hw.mlir +++ b/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"} +}