@@ -575,6 +575,8 @@ struct FIRRTLModuleLowering
575
575
CircuitLoweringState &loweringState);
576
576
LogicalResult lowerFormalBody (verif::FormalOp formalOp,
577
577
CircuitLoweringState &loweringState);
578
+ LogicalResult lowerSimulationBody (verif::SimulationOp simulationOp,
579
+ CircuitLoweringState &loweringState);
578
580
};
579
581
580
582
} // end anonymous namespace
@@ -618,6 +620,7 @@ void FIRRTLModuleLowering::runOnOperation() {
618
620
619
621
SmallVector<hw::HWModuleOp, 32 > modulesToProcess;
620
622
SmallVector<verif::FormalOp> formalOpsToProcess;
623
+ SmallVector<verif::SimulationOp> simulationOpsToProcess;
621
624
622
625
AnnotationSet circuitAnno (circuit);
623
626
moveVerifAnno (getOperation (), circuitAnno, extractAssertAnnoClass,
@@ -668,14 +671,26 @@ void FIRRTLModuleLowering::runOnOperation() {
668
671
state.recordModuleMapping (&op, loweredMod);
669
672
return success ();
670
673
})
671
- .Case <FormalOp>([&](auto oldFormalOp ) {
674
+ .Case <FormalOp>([&](auto oldOp ) {
672
675
auto builder = OpBuilder::atBlockEnd (topLevelModule);
673
- auto newFormalOp = builder.create <verif::FormalOp>(
674
- oldFormalOp.getLoc (), oldFormalOp.getNameAttr (),
675
- oldFormalOp.getParametersAttr ());
676
- newFormalOp.getBody ().emplaceBlock ();
677
- state.recordModuleMapping (oldFormalOp, newFormalOp);
678
- formalOpsToProcess.push_back (newFormalOp);
676
+ auto newOp = builder.create <verif::FormalOp>(
677
+ oldOp.getLoc (), oldOp.getNameAttr (),
678
+ oldOp.getParametersAttr ());
679
+ newOp.getBody ().emplaceBlock ();
680
+ state.recordModuleMapping (oldOp, newOp);
681
+ formalOpsToProcess.push_back (newOp);
682
+ return success ();
683
+ })
684
+ .Case <SimulationOp>([&](auto oldOp) {
685
+ auto loc = oldOp.getLoc ();
686
+ auto builder = OpBuilder::atBlockEnd (topLevelModule);
687
+ auto newOp = builder.create <verif::SimulationOp>(
688
+ loc, oldOp.getNameAttr (), oldOp.getParametersAttr ());
689
+ auto &body = newOp.getRegion ().emplaceBlock ();
690
+ body.addArgument (seq::ClockType::get (builder.getContext ()), loc);
691
+ body.addArgument (builder.getI1Type (), loc);
692
+ state.recordModuleMapping (oldOp, newOp);
693
+ simulationOpsToProcess.push_back (newOp);
679
694
return success ();
680
695
})
681
696
.Default ([&](Operation *op) {
@@ -748,6 +763,13 @@ void FIRRTLModuleLowering::runOnOperation() {
748
763
if (failed (result))
749
764
return signalPassFailure ();
750
765
766
+ // Lower all simulation op bodies.
767
+ result = mlir::failableParallelForEach (
768
+ &getContext (), simulationOpsToProcess,
769
+ [&](auto op) { return lowerSimulationBody (op, state); });
770
+ if (failed (result))
771
+ return signalPassFailure ();
772
+
751
773
// Move binds from inside modules to outside modules.
752
774
for (auto bind : state.binds ) {
753
775
bind->moveBefore (bind->getParentOfType <hw::HWModuleOp>());
@@ -1418,22 +1440,18 @@ LogicalResult FIRRTLModuleLowering::lowerModulePortsAndMoveBody(
1418
1440
// / Run on each `verif.formal` to populate its body based on the original
1419
1441
// / `firrtl.formal` operation.
1420
1442
LogicalResult
1421
- FIRRTLModuleLowering::lowerFormalBody (verif::FormalOp formalOp ,
1443
+ FIRRTLModuleLowering::lowerFormalBody (verif::FormalOp newOp ,
1422
1444
CircuitLoweringState &loweringState) {
1423
- auto builder = OpBuilder::atBlockEnd (&formalOp .getBody ().front ());
1445
+ auto builder = OpBuilder::atBlockEnd (&newOp .getBody ().front ());
1424
1446
1425
1447
// Find the module targeted by the `firrtl.formal` operation. The `FormalOp`
1426
1448
// verifier guarantees the module exists and that it is an `FModuleOp`. This
1427
1449
// we can then translate to the corresponding `HWModuleOp`.
1428
- auto oldFormalOp = cast<FormalOp>(loweringState.getOldModule (formalOp ));
1429
- auto moduleName = oldFormalOp .getModuleNameAttr ().getAttr ();
1450
+ auto oldOp = cast<FormalOp>(loweringState.getOldModule (newOp ));
1451
+ auto moduleName = oldOp .getModuleNameAttr ().getAttr ();
1430
1452
auto oldModule = cast<FModuleOp>(
1431
1453
loweringState.getInstanceGraph ().lookup (moduleName)->getModule ());
1432
- auto newModule =
1433
- dyn_cast_or_null<hw::HWModuleOp>(loweringState.getNewModule (oldModule));
1434
- if (!newModule)
1435
- return oldFormalOp->emitOpError ()
1436
- << " could not find module " << oldModule.getSymNameAttr ();
1454
+ auto newModule = cast<hw::HWModuleOp>(loweringState.getNewModule (oldModule));
1437
1455
1438
1456
// Create a symbolic input for every input of the lowered module.
1439
1457
SmallVector<Value> symbolicInputs;
@@ -1442,11 +1460,36 @@ FIRRTLModuleLowering::lowerFormalBody(verif::FormalOp formalOp,
1442
1460
builder.create <verif::SymbolicValueOp>(arg.getLoc (), arg.getType ()));
1443
1461
1444
1462
// Instantiate the module with the given symbolic inputs.
1445
- builder.create <hw::InstanceOp>(formalOp .getLoc (), newModule,
1463
+ builder.create <hw::InstanceOp>(newOp .getLoc (), newModule,
1446
1464
newModule.getNameAttr (), symbolicInputs);
1447
1465
return success ();
1448
1466
}
1449
1467
1468
+ // / Run on each `verif.simulation` to populate its body based on the original
1469
+ // / `firrtl.simulation` operation.
1470
+ LogicalResult
1471
+ FIRRTLModuleLowering::lowerSimulationBody (verif::SimulationOp newOp,
1472
+ CircuitLoweringState &loweringState) {
1473
+ auto builder = OpBuilder::atBlockEnd (newOp.getBody ());
1474
+
1475
+ // Find the module targeted by the `firrtl.simulation` operation.
1476
+ auto oldOp = cast<SimulationOp>(loweringState.getOldModule (newOp));
1477
+ auto moduleName = oldOp.getModuleNameAttr ().getAttr ();
1478
+ auto oldModule = cast<FModuleLike>(
1479
+ *loweringState.getInstanceGraph ().lookup (moduleName)->getModule ());
1480
+ auto newModule =
1481
+ cast<hw::HWModuleLike>(loweringState.getNewModule (oldModule));
1482
+
1483
+ // Instantiate the module with the simulation op's block arguments as inputs,
1484
+ // and yield the module's outputs.
1485
+ SmallVector<Value> inputs (newOp.getBody ()->args_begin (),
1486
+ newOp.getBody ()->args_end ());
1487
+ auto instOp = builder.create <hw::InstanceOp>(newOp.getLoc (), newModule,
1488
+ newModule.getNameAttr (), inputs);
1489
+ builder.create <verif::YieldOp>(newOp.getLoc (), instOp.getResults ());
1490
+ return success ();
1491
+ }
1492
+
1450
1493
// ===----------------------------------------------------------------------===//
1451
1494
// Module Body Lowering Pass
1452
1495
// ===----------------------------------------------------------------------===//
0 commit comments