22 #include "mlir/Pass/Pass.h"
23 #include "llvm/ADT/TypeSwitch.h"
27 #define GEN_PASS_DEF_VERIFYCLOCKEDASSERTLIKE
28 #include "circt/Dialect/Verif/Passes.h.inc"
32 using namespace circt;
33 using namespace verif;
40 struct VerifyClockedAssertLikePass
41 : circt::verif::impl::VerifyClockedAssertLikeBase<
42 VerifyClockedAssertLikePass> {
46 llvm::SmallMapVector<Operation *, OperandRange::iterator, 16> worklist;
49 llvm::DenseSet<Operation *> handledOps;
52 void runOnOperation()
override;
55 void verify(Operation *clockedAssertLikeOp) {
57 Operation *
property = clockedAssertLikeOp->getOperand(0).getDefiningOp();
60 worklist.insert({property,
property->operand_begin()});
63 while (!worklist.empty()) {
64 auto &[op, operandIt] = worklist.back();
66 if (operandIt == op->operand_end()) {
68 if (isa<ltl::ClockOp>(op)) {
69 op->emitError(
"Nested clock or disable operations are not "
70 "allowed for clock_assertlike operations.");
75 handledOps.insert(op);
82 Value operand = *(operandIt++);
83 auto *defOp = operand.getDefiningOp();
86 if (!defOp || handledOps.contains(defOp))
89 worklist.insert({defOp, defOp->operand_begin()});
99 void VerifyClockedAssertLikePass::runOnOperation() {
100 getOperation()->walk([&](Operation *op) {
101 llvm::TypeSwitch<Operation *, void>(op)
102 .Case<verif::ClockedAssertOp, verif::ClockedAssumeOp,
103 verif::ClockedCoverOp>([&](
auto clockedOp) {
verify(clockedOp); })
104 .Default([&](
auto) {});
109 return std::make_unique<VerifyClockedAssertLikePass>();
static LogicalResult verify(Value clock, bool eventExists, mlir::Location loc)
std::unique_ptr< mlir::Pass > createVerifyClockedAssertLikePass()
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.