9#include "slang/ast/expressions/AssertionExpr.h"
14#include "mlir/IR/BuiltinAttributes.h"
15#include "mlir/Support/LLVM.h"
21using namespace ImportVerilog;
25struct AssertionExprVisitor {
30 AssertionExprVisitor(
Context &context, Location loc)
31 : context(context), loc(loc), builder(context.builder) {}
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);
42 return {minAttr, rangeAttr};
46 Value createRepetition(Location loc,
47 const slang::ast::SequenceRepetition &repetition,
48 Value &inputSequence) {
50 auto [minRepetitions, repetitionRange] =
51 convertRangeToAttrs(repetition.range.min, repetition.range.max);
53 using slang::ast::SequenceRepetition;
56 if ((repetition.kind == SequenceRepetition::Nonconsecutive ||
57 repetition.kind == SequenceRepetition::GoTo) &&
60 repetition.kind == SequenceRepetition::Nonconsecutive
61 ?
"Nonconsecutive repetition requires a maximum value"
62 :
"GoTo repetition requires a maximum value");
66 switch (repetition.kind) {
67 case SequenceRepetition::Consecutive:
68 return ltl::RepeatOp::create(builder, loc, inputSequence, minRepetitions,
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);
77 llvm_unreachable(
"All enum values handled in switch");
80 Value visit(
const slang::ast::SimpleAssertionExpr &expr) {
86 auto valueType = value.getType();
89 if (!mlir::isa<ltl::SequenceType, ltl::PropertyType>(valueType)) {
97 if (!expr.repetition.has_value()) {
103 return createRepetition(loc, expr.repetition.value(), value);
106 Value visit(
const slang::ast::SequenceConcatExpr &expr) {
108 assert(!expr.elements.empty());
110 SmallVector<Value> sequenceElements;
112 for (
const auto &concatElement : expr.elements) {
113 Value sequenceValue =
118 Type valueType = sequenceValue.getType();
119 assert(valueType.isInteger(1) || mlir::isa<ltl::SequenceType>(valueType));
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);
128 return builder.createOrFold<ltl::ConcatOp>(loc, sequenceElements);
131 Value visit(
const slang::ast::UnaryAssertionExpr &expr) {
135 using slang::ast::UnaryAssertionOperator;
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");
144 return ltl::EventuallyOp::create(builder, loc, value);
146 case UnaryAssertionOperator::Always: {
147 std::pair<mlir::IntegerAttr, mlir::IntegerAttr> attr = {
148 builder.getI64IntegerAttr(0), mlir::IntegerAttr{}};
149 if (expr.range.has_value()) {
151 convertRangeToAttrs(expr.range.value().min, expr.range.value().max);
153 return ltl::RepeatOp::create(builder, loc, value, attr.first,
156 case UnaryAssertionOperator::NextTime: {
157 auto minRepetitions = builder.getI64IntegerAttr(1);
158 if (expr.range.has_value()) {
159 minRepetitions = builder.getI64IntegerAttr(expr.range.value().min);
161 return ltl::DelayOp::create(builder, loc, value, minRepetitions,
162 builder.getI64IntegerAttr(0));
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);
171 llvm_unreachable(
"All enum values handled in switch");
174 Value visit(
const slang::ast::BinaryAssertionExpr &expr) {
179 SmallVector<Value, 2> operands = {lhs, rhs};
180 using slang::ast::BinaryAssertionOperator;
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});
194 case BinaryAssertionOperator::Within: {
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));
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});
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});
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});
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});
232 case BinaryAssertionOperator::OverlappedImplication:
233 return ltl::ImplicationOp::create(builder, loc, operands);
234 case BinaryAssertionOperator::NonOverlappedImplication: {
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});
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);
251 case BinaryAssertionOperator::NonOverlappedFollowedBy: {
254 auto notRhs = ltl::NotOp::create(builder, loc, rhs);
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);
264 case BinaryAssertionOperator::SUntil:
265 case BinaryAssertionOperator::SUntilWith:
266 mlir::emitError(loc,
"unsupported binary operator: ")
267 << slang::ast::toString(expr.op);
270 llvm_unreachable(
"All enum values handled in switch");
273 Value visit(
const slang::ast::ClockingAssertionExpr &expr) {
281 template <
typename T>
282 Value visit(T &&node) {
283 mlir::emitError(loc,
"unsupported expression: ")
284 << slang::ast::toString(node.kind);
288 Value visitInvalid(
const slang::ast::AssertionExpr &expr) {
289 mlir::emitError(loc,
"invalid expression");
295Value Context::convertAssertionExpression(
const slang::ast::AssertionExpr &expr,
297 AssertionExprVisitor visitor{*
this, loc};
298 return expr.visit(visitor);
295Value Context::convertAssertionExpression(
const slang::ast::AssertionExpr &expr, {
…}
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");
312 return moore::ConversionOp::create(
builder, value.getLoc(),
assert(baseType &&"element must be base type")
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.