CIRCT  20.0.0git
VerifOps.cpp
Go to the documentation of this file.
1 //===- VerifOps.cpp -------------------------------------------------------===//
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 
15 #include "mlir/IR/Builders.h"
16 #include "mlir/IR/OpImplementation.h"
17 #include "mlir/IR/PatternMatch.h"
18 #include "mlir/IR/SymbolTable.h"
19 #include "mlir/IR/TypeRange.h"
20 #include "mlir/Interfaces/FunctionImplementation.h"
21 #include "mlir/Interfaces/SideEffectInterfaces.h"
22 #include "llvm/ADT/MapVector.h"
23 
24 using namespace circt;
25 using namespace verif;
26 using namespace mlir;
27 
28 static ClockEdge ltlToVerifClockEdge(ltl::ClockEdge ce) {
29  switch (ce) {
30  case ltl::ClockEdge::Pos:
31  return ClockEdge::Pos;
32  case ltl::ClockEdge::Neg:
33  return ClockEdge::Neg;
34  case ltl::ClockEdge::Both:
35  return ClockEdge::Both;
36  }
37  llvm_unreachable("Unknown event control kind");
38 }
39 
40 //===----------------------------------------------------------------------===//
41 // HasBeenResetOp
42 //===----------------------------------------------------------------------===//
43 
44 OpFoldResult HasBeenResetOp::fold(FoldAdaptor adaptor) {
45  // Fold to zero if the reset is a constant. In this case the op is either
46  // permanently in reset or never resets. Both mean that the reset never
47  // finishes, so this op never returns true.
48  if (adaptor.getReset())
49  return BoolAttr::get(getContext(), false);
50 
51  // Fold to zero if the clock is a constant and the reset is synchronous. In
52  // that case the reset will never be started.
53  if (!adaptor.getAsync() && adaptor.getClock())
54  return BoolAttr::get(getContext(), false);
55 
56  return {};
57 }
58 
59 //===----------------------------------------------------------------------===//
60 // AssertLikeOps Canonicalizations
61 //===----------------------------------------------------------------------===//
62 
63 namespace AssertLikeOp {
64 // assertlike(ltl.clock(prop, clk), en) -> clocked_assertlike(prop, en, clk)
65 template <typename TargetOp, typename Op>
66 static LogicalResult canonicalize(Op op, PatternRewriter &rewriter) {
67  // If the property is a block argument, then no canonicalization is possible
68  Value property = op.getProperty();
69  auto clockOp = property.getDefiningOp<ltl::ClockOp>();
70  if (!clockOp)
71  return failure();
72 
73  // Check for clock operand
74  // If it exists, fold it into a clocked assertlike
75  rewriter.replaceOpWithNewOp<TargetOp>(
76  op, clockOp.getInput(), ltlToVerifClockEdge(clockOp.getEdge()),
77  clockOp.getClock(), op.getEnable(), op.getLabelAttr());
78 
79  return success();
80 }
81 
82 } // namespace AssertLikeOp
83 
84 LogicalResult AssertOp::canonicalize(AssertOp op, PatternRewriter &rewriter) {
85  return AssertLikeOp::canonicalize<ClockedAssertOp>(op, rewriter);
86 }
87 
88 LogicalResult AssumeOp::canonicalize(AssumeOp op, PatternRewriter &rewriter) {
89  return AssertLikeOp::canonicalize<ClockedAssumeOp>(op, rewriter);
90 }
91 
92 LogicalResult CoverOp::canonicalize(CoverOp op, PatternRewriter &rewriter) {
93  return AssertLikeOp::canonicalize<ClockedCoverOp>(op, rewriter);
94 }
95 
96 //===----------------------------------------------------------------------===//
97 // LogicalEquivalenceCheckingOp
98 //===----------------------------------------------------------------------===//
99 
100 LogicalResult LogicEquivalenceCheckingOp::verifyRegions() {
101  if (getFirstCircuit().getArgumentTypes() !=
102  getSecondCircuit().getArgumentTypes())
103  return emitOpError() << "block argument types of both regions must match";
104  if (getFirstCircuit().front().getTerminator()->getOperandTypes() !=
105  getSecondCircuit().front().getTerminator()->getOperandTypes())
106  return emitOpError()
107  << "types of the yielded values of both regions must match";
108 
109  return success();
110 }
111 
112 //===----------------------------------------------------------------------===//
113 // BoundedModelCheckingOp
114 //===----------------------------------------------------------------------===//
115 
116 LogicalResult BoundedModelCheckingOp::verifyRegions() {
117  if (!getInit().getArgumentTypes().empty())
118  return emitOpError() << "init region must have no arguments";
119  auto *initYieldOp = getInit().front().getTerminator();
120  auto *loopYieldOp = getLoop().front().getTerminator();
121  if (initYieldOp->getOperandTypes() != loopYieldOp->getOperandTypes())
122  return emitOpError()
123  << "init and loop regions must yield the same types of values";
124  if (initYieldOp->getOperandTypes() != getLoop().front().getArgumentTypes())
125  return emitOpError()
126  << "loop region arguments must match the types of the values "
127  "yielded by the init and loop regions";
128  size_t totalClocks = 0;
129  auto circuitArgTy = getCircuit().getArgumentTypes();
130  for (auto input : circuitArgTy)
131  if (isa<seq::ClockType>(input))
132  totalClocks++;
133  auto initYields = initYieldOp->getOperands();
134  // We know init and loop yields match, so only need to check one
135  if (initYields.size() < totalClocks)
136  return emitOpError()
137  << "init and loop regions must yield at least as many clock "
138  "values as there are clock arguments to the circuit region";
139  for (size_t i = 0; i < totalClocks; i++) {
140  if (!isa<seq::ClockType>(initYieldOp->getOperand(i).getType()))
141  return emitOpError()
142  << "init and loop regions must yield as many clock values as "
143  "there are clock arguments in the circuit region "
144  "before any other values";
145  }
146  auto initialValues = getInitialValues();
147  if (initialValues.size() != getNumRegs()) {
148  return emitOpError()
149  << "number of initial values must match the number of registers";
150  }
151  for (auto attr : initialValues) {
152  if (!isa<IntegerAttr, UnitAttr>(attr))
153  return emitOpError()
154  << "initial values must be integer or unit attributes";
155  }
156  return success();
157 }
158 
159 //===----------------------------------------------------------------------===//
160 // Generated code
161 //===----------------------------------------------------------------------===//
162 
163 #define GET_OP_CLASSES
164 #include "circt/Dialect/Verif/Verif.cpp.inc"
static InstancePath empty
static ClockEdge ltlToVerifClockEdge(ltl::ClockEdge ce)
Definition: VerifOps.cpp:28
static LogicalResult canonicalize(Op op, PatternRewriter &rewriter)
Definition: VerifOps.cpp:66
Direction get(bool isOutput)
Returns an output direction if isOutput is true, otherwise returns an input direction.
Definition: CalyxOps.cpp:55
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
Definition: DebugAnalysis.h:21
Definition: verif.py:1