Loading [MathJax]/extensions/tex2jax.js
CIRCT 22.0.0git
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
AssertionExpr.cpp
Go to the documentation of this file.
1//===- AssertionExpr.cpp - Slang assertion expression conversion ----------===//
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
9#include "slang/ast/expressions/AssertionExpr.h"
13#include "circt/Support/LLVM.h"
14#include "mlir/IR/BuiltinAttributes.h"
15#include "mlir/Support/LLVM.h"
16
17#include <optional>
18#include <utility>
19
20using namespace circt;
21using namespace ImportVerilog;
22
23// NOLINTBEGIN(misc-no-recursion)
24namespace {
25struct AssertionExprVisitor {
26 Context &context;
27 Location loc;
28 OpBuilder &builder;
29
30 AssertionExprVisitor(Context &context, Location loc)
31 : context(context), loc(loc), builder(context.builder) {}
32
33 /// Helper to convert a range (min, optional max) to MLIR integer attributes
34 std::pair<mlir::IntegerAttr, mlir::IntegerAttr>
35 convertRangeToAttrs(uint32_t min,
36 std::optional<uint32_t> max = std::nullopt) {
37 auto minAttr = builder.getI64IntegerAttr(min);
38 mlir::IntegerAttr rangeAttr;
39 if (max.has_value()) {
40 rangeAttr = builder.getI64IntegerAttr(max.value() - min);
41 }
42 return {minAttr, rangeAttr};
43 }
44
45 /// Add repetition operation to a sequence
46 Value createRepetition(Location loc,
47 const slang::ast::SequenceRepetition &repetition,
48 Value &inputSequence) {
49 // Extract cycle range
50 auto [minRepetitions, repetitionRange] =
51 convertRangeToAttrs(repetition.range.min, repetition.range.max);
52
53 using slang::ast::SequenceRepetition;
54
55 // Check if repetition range is required
56 if ((repetition.kind == SequenceRepetition::Nonconsecutive ||
57 repetition.kind == SequenceRepetition::GoTo) &&
58 !repetitionRange) {
59 mlir::emitError(loc,
60 repetition.kind == SequenceRepetition::Nonconsecutive
61 ? "Nonconsecutive repetition requires a maximum value"
62 : "GoTo repetition requires a maximum value");
63 return {};
64 }
65
66 switch (repetition.kind) {
67 case SequenceRepetition::Consecutive:
68 return ltl::RepeatOp::create(builder, loc, inputSequence, minRepetitions,
69 repetitionRange);
70 case SequenceRepetition::Nonconsecutive:
71 return ltl::NonConsecutiveRepeatOp::create(
72 builder, loc, inputSequence, minRepetitions, repetitionRange);
73 case SequenceRepetition::GoTo:
74 return ltl::GoToRepeatOp::create(builder, loc, inputSequence,
75 minRepetitions, repetitionRange);
76 }
77 llvm_unreachable("All enum values handled in switch");
78 }
79
80 Value visit(const slang::ast::SimpleAssertionExpr &expr) {
81 // Handle expression
82 auto value = context.convertRvalueExpression(expr.expr);
83 if (!value)
84 return {};
85 auto loc = context.convertLocation(expr.expr.sourceRange);
86 auto valueType = value.getType();
87 // For assertion instances the value is already the expected type, convert
88 // boolean value
89 if (!mlir::isa<ltl::SequenceType, ltl::PropertyType>(valueType)) {
90 value = context.convertToI1(value);
91 }
92 if (!value)
93 return {};
94
95 // Handle repetition
96 // The optional repetition is empty, return the converted expression
97 if (!expr.repetition.has_value()) {
98 return value;
99 }
100
101 // There is a repetition, embed the expression into the kind of given
102 // repetition
103 return createRepetition(loc, expr.repetition.value(), value);
104 }
105
106 Value visit(const slang::ast::SequenceConcatExpr &expr) {
107 // Create a sequence of delayed operations, combined with a concat operation
108 assert(!expr.elements.empty());
109
110 SmallVector<Value> sequenceElements;
111
112 for (const auto &concatElement : expr.elements) {
113 Value sequenceValue =
114 context.convertAssertionExpression(*concatElement.sequence, loc);
115 if (!sequenceValue)
116 return {};
117
118 Type valueType = sequenceValue.getType();
119 assert(valueType.isInteger(1) || mlir::isa<ltl::SequenceType>(valueType));
120
121 auto [delayMin, delayRange] =
122 convertRangeToAttrs(concatElement.delay.min, concatElement.delay.max);
123 auto delayedSequence = ltl::DelayOp::create(builder, loc, sequenceValue,
124 delayMin, delayRange);
125 sequenceElements.push_back(delayedSequence);
126 }
127
128 return builder.createOrFold<ltl::ConcatOp>(loc, sequenceElements);
129 }
130
131 Value visit(const slang::ast::UnaryAssertionExpr &expr) {
132 auto value = context.convertAssertionExpression(expr.expr, loc);
133 if (!value)
134 return {};
135 using slang::ast::UnaryAssertionOperator;
136 switch (expr.op) {
137 case UnaryAssertionOperator::Not:
138 return ltl::NotOp::create(builder, loc, value);
139 case UnaryAssertionOperator::SEventually:
140 if (expr.range.has_value()) {
141 mlir::emitError(loc, "Strong eventually with range not supported");
142 return {};
143 } else {
144 return ltl::EventuallyOp::create(builder, loc, value);
145 }
146 case UnaryAssertionOperator::Always: {
147 std::pair<mlir::IntegerAttr, mlir::IntegerAttr> attr = {
148 builder.getI64IntegerAttr(0), mlir::IntegerAttr{}};
149 if (expr.range.has_value()) {
150 attr =
151 convertRangeToAttrs(expr.range.value().min, expr.range.value().max);
152 }
153 return ltl::RepeatOp::create(builder, loc, value, attr.first,
154 attr.second);
155 }
156 case UnaryAssertionOperator::NextTime: {
157 auto minRepetitions = builder.getI64IntegerAttr(1);
158 if (expr.range.has_value()) {
159 minRepetitions = builder.getI64IntegerAttr(expr.range.value().min);
160 }
161 return ltl::DelayOp::create(builder, loc, value, minRepetitions,
162 builder.getI64IntegerAttr(0));
163 }
164 case UnaryAssertionOperator::Eventually:
165 case UnaryAssertionOperator::SNextTime:
166 case UnaryAssertionOperator::SAlways:
167 mlir::emitError(loc, "unsupported unary operator: ")
168 << slang::ast::toString(expr.op);
169 return {};
170 }
171 llvm_unreachable("All enum values handled in switch");
172 }
173
174 Value visit(const slang::ast::BinaryAssertionExpr &expr) {
175 auto lhs = context.convertAssertionExpression(expr.left, loc);
176 auto rhs = context.convertAssertionExpression(expr.right, loc);
177 if (!lhs || !rhs)
178 return {};
179 SmallVector<Value, 2> operands = {lhs, rhs};
180 using slang::ast::BinaryAssertionOperator;
181 switch (expr.op) {
182 case BinaryAssertionOperator::And:
183 return ltl::AndOp::create(builder, loc, operands);
184 case BinaryAssertionOperator::Or:
185 return ltl::OrOp::create(builder, loc, operands);
186 case BinaryAssertionOperator::Intersect:
187 return ltl::IntersectOp::create(builder, loc, operands);
188 case BinaryAssertionOperator::Throughout: {
189 auto lhsRepeat = ltl::RepeatOp::create(
190 builder, loc, lhs, builder.getI64IntegerAttr(0), mlir::IntegerAttr{});
191 return ltl::IntersectOp::create(builder, loc,
192 SmallVector<Value, 2>{lhsRepeat, rhs});
193 }
194 case BinaryAssertionOperator::Within: {
195 auto constOne =
196 hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1);
197 auto oneRepeat = ltl::RepeatOp::create(builder, loc, constOne,
198 builder.getI64IntegerAttr(0),
199 mlir::IntegerAttr{});
200 auto repeatDelay = ltl::DelayOp::create(builder, loc, oneRepeat,
201 builder.getI64IntegerAttr(1),
202 builder.getI64IntegerAttr(0));
203 auto lhsDelay =
204 ltl::DelayOp::create(builder, loc, lhs, builder.getI64IntegerAttr(1),
205 builder.getI64IntegerAttr(0));
206 auto combined = ltl::ConcatOp::create(
207 builder, loc, SmallVector<Value, 3>{repeatDelay, lhsDelay, constOne});
208 return ltl::IntersectOp::create(builder, loc,
209 SmallVector<Value, 2>{combined, rhs});
210 }
211 case BinaryAssertionOperator::Iff: {
212 auto ored = ltl::OrOp::create(builder, loc, operands);
213 auto notOred = ltl::NotOp::create(builder, loc, ored);
214 auto anded = ltl::AndOp::create(builder, loc, operands);
215 return ltl::OrOp::create(builder, loc,
216 SmallVector<Value, 2>{notOred, anded});
217 }
218 case BinaryAssertionOperator::Until:
219 return ltl::UntilOp::create(builder, loc, operands);
220 case BinaryAssertionOperator::UntilWith: {
221 auto untilOp = ltl::UntilOp::create(builder, loc, operands);
222 auto andOp = ltl::AndOp::create(builder, loc, operands);
223 auto notUntil = ltl::NotOp::create(builder, loc, untilOp);
224 return ltl::OrOp::create(builder, loc,
225 SmallVector<Value, 2>{notUntil, andOp});
226 }
227 case BinaryAssertionOperator::Implies: {
228 auto notLhs = ltl::NotOp::create(builder, loc, lhs);
229 return ltl::OrOp::create(builder, loc,
230 SmallVector<Value, 2>{notLhs, rhs});
231 }
232 case BinaryAssertionOperator::OverlappedImplication:
233 return ltl::ImplicationOp::create(builder, loc, operands);
234 case BinaryAssertionOperator::NonOverlappedImplication: {
235 auto constOne =
236 hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1);
237 auto lhsDelay =
238 ltl::DelayOp::create(builder, loc, lhs, builder.getI64IntegerAttr(1),
239 builder.getI64IntegerAttr(0));
240 auto antecedent = ltl::ConcatOp::create(
241 builder, loc, SmallVector<Value, 2>{lhsDelay, constOne});
242 return ltl::ImplicationOp::create(builder, loc,
243 SmallVector<Value, 2>{antecedent, rhs});
244 }
245 case BinaryAssertionOperator::OverlappedFollowedBy: {
246 auto notRhs = ltl::NotOp::create(builder, loc, rhs);
247 auto implication = ltl::ImplicationOp::create(
248 builder, loc, SmallVector<Value, 2>{lhs, notRhs});
249 return ltl::NotOp::create(builder, loc, implication);
250 }
251 case BinaryAssertionOperator::NonOverlappedFollowedBy: {
252 auto constOne =
253 hw::ConstantOp::create(builder, loc, builder.getI1Type(), 1);
254 auto notRhs = ltl::NotOp::create(builder, loc, rhs);
255 auto lhsDelay =
256 ltl::DelayOp::create(builder, loc, lhs, builder.getI64IntegerAttr(1),
257 builder.getI64IntegerAttr(0));
258 auto antecedent = ltl::ConcatOp::create(
259 builder, loc, SmallVector<Value, 2>{lhsDelay, constOne});
260 auto implication = ltl::ImplicationOp::create(
261 builder, loc, SmallVector<Value, 2>{antecedent, notRhs});
262 return ltl::NotOp::create(builder, loc, implication);
263 }
264 case BinaryAssertionOperator::SUntil:
265 case BinaryAssertionOperator::SUntilWith:
266 mlir::emitError(loc, "unsupported binary operator: ")
267 << slang::ast::toString(expr.op);
268 return {};
269 }
270 llvm_unreachable("All enum values handled in switch");
271 }
272
273 Value visit(const slang::ast::ClockingAssertionExpr &expr) {
274 auto assertionExpr = context.convertAssertionExpression(expr.expr, loc);
275 if (!assertionExpr)
276 return {};
277 return context.convertLTLTimingControl(expr.clocking, assertionExpr);
278 }
279
280 /// Emit an error for all other expressions.
281 template <typename T>
282 Value visit(T &&node) {
283 mlir::emitError(loc, "unsupported expression: ")
284 << slang::ast::toString(node.kind);
285 return {};
286 }
287
288 Value visitInvalid(const slang::ast::AssertionExpr &expr) {
289 mlir::emitError(loc, "invalid expression");
290 return {};
291 }
292};
293} // namespace
294
295Value Context::convertAssertionExpression(const slang::ast::AssertionExpr &expr,
296 Location loc) {
297 AssertionExprVisitor visitor{*this, loc};
298 return expr.visit(visitor);
299}
300// NOLINTEND(misc-no-recursion)
301
302/// Helper function to convert a value to an i1 value.
303Value Context::convertToI1(Value value) {
304 if (!value)
305 return {};
306 auto type = dyn_cast<moore::IntType>(value.getType());
307 if (!type || type.getBitSize() != 1) {
308 mlir::emitError(value.getLoc(), "expected a 1-bit integer");
309 return {};
310 }
311
312 return moore::ConversionOp::create(builder, value.getLoc(),
313 builder.getI1Type(), value);
314}
assert(baseType &&"element must be base type")
create(data_type, value)
Definition hw.py:433
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
A helper class to facilitate the conversion from a Slang AST to MLIR operations.
Value convertToI1(Value value)
Helper function to convert a value to a MLIR I1 value.
Value convertLTLTimingControl(const slang::ast::TimingControl &ctrl, const Value &seqOrPro)
OpBuilder builder
The builder used to create IR operations.
Value convertRvalueExpression(const slang::ast::Expression &expr, Type requiredType={})
Value convertAssertionExpression(const slang::ast::AssertionExpr &expr, Location loc)
Location convertLocation(slang::SourceLocation loc)
Convert a slang SourceLocation into an MLIR Location.