CIRCT  19.0.0git
VerifyClockedAssertLike.cpp
Go to the documentation of this file.
1 //===- VerifyClockedAssertLike.cpp - Check Clocked Asserts -------*- C++-*-===//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //===----------------------------------------------------------------------===//
7 //
8 // Checks that clocked assert-like ops are constructed correctly.
9 //
10 //===----------------------------------------------------------------------===//
11 
12 #include "PassDetails.h"
15 #include "circt/Dialect/HW/HWOps.h"
23 #include "mlir/Pass/Pass.h"
24 #include "llvm/ADT/TypeSwitch.h"
25 
26 using namespace circt;
27 using namespace verif;
28 
29 namespace {
30 // Verify function for clocked assert / assume / cover ops.
31 // This checks that they do not contiain any nested clocks or disable operations
32 // Clocked assertlike ops are a simple form of assertions that only
33 // contain one clock and one disable condition.
34 struct VerifyClockedAssertLikePass
35  : VerifyClockedAssertLikeBase<VerifyClockedAssertLikePass> {
36 private:
37  // Used to perform a DFS search through the module to visit all operands
38  // before they are used
39  llvm::SmallMapVector<Operation *, OperandRange::iterator, 16> worklist;
40 
41  // Keeps track of operations that have been visited
42  llvm::DenseSet<Operation *> handledOps;
43 
44 public:
45  void runOnOperation() override;
46 
47 private:
48  void verify(Operation *clockedAssertLikeOp) {
49 
50  Operation *property = clockedAssertLikeOp->getOperand(0).getDefiningOp();
51 
52  // Fill in our worklist
53  worklist.insert({property, property->operand_begin()});
54 
55  // Process the elements in our worklist
56  while (!worklist.empty()) {
57  auto &[op, operandIt] = worklist.back();
58 
59  if (operandIt == op->operand_end()) {
60  // Check that our property doesn't contain any illegal ops
61  if (isa<ltl::ClockOp, ltl::DisableOp>(op)) {
62  op->emitError("Nested clock or disable operations are not "
63  "allowed for clock_assertlike operations.");
64  return;
65  }
66 
67  // Record that our op has been visited
68  handledOps.insert(op);
69  worklist.pop_back();
70  continue;
71  }
72 
73  // Send the operands of our op to the worklist in case they are still
74  // un-visited
75  Value operand = *(operandIt++);
76  auto *defOp = operand.getDefiningOp();
77 
78  // Make sure that we don't visit the same operand twice
79  if (!defOp || handledOps.contains(defOp))
80  continue;
81 
82  // This is triggered if our operand is already in the worklist and
83  // wasn't handled
84  if (!worklist.insert({defOp, defOp->operand_begin()}).second) {
85  op->emitError("dependency cycle");
86  return;
87  }
88  }
89 
90  // Clear worklist and such
91  worklist.clear();
92  handledOps.clear();
93  }
94 };
95 } // namespace
96 
97 void VerifyClockedAssertLikePass::runOnOperation() {
98  getOperation()->walk([&](Operation *op) {
99  llvm::TypeSwitch<Operation *, void>(op)
100  .Case<verif::ClockedAssertOp, verif::ClockedAssumeOp,
101  verif::ClockedCoverOp>([&](auto clockedOp) { verify(clockedOp); })
102  .Default([&](auto) {});
103  });
104 }
105 
106 std::unique_ptr<mlir::Pass> circt::verif::createVerifyClockedAssertLikePass() {
107  return std::make_unique<VerifyClockedAssertLikePass>();
108 }
std::unique_ptr< mlir::Pass > createVerifyClockedAssertLikePass()
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
Definition: DebugAnalysis.h:21
Definition: verif.py:1