Loading [MathJax]/extensions/tex2jax.js
CIRCT 21.0.0git
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
HWToBTOR2.cpp
Go to the documentation of this file.
1//===- HWToBTOR2.cpp - HW to BTOR2 translation ------------------*- 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// Converts a hw module to a btor2 format and prints it out
9//
10//===----------------------------------------------------------------------===//
11
31#include "mlir/Pass/Pass.h"
32#include "llvm/ADT/MapVector.h"
33#include "llvm/ADT/TypeSwitch.h"
34#include "llvm/Support/raw_ostream.h"
35
36namespace circt {
37#define GEN_PASS_DEF_CONVERTHWTOBTOR2
38#include "circt/Conversion/Passes.h.inc"
39} // namespace circt
40
41using namespace circt;
42using namespace hw;
43
44namespace {
45// The goal here is to traverse the operations in order and convert them one by
46// one into btor2
47struct ConvertHWToBTOR2Pass
48 : public circt::impl::ConvertHWToBTOR2Base<ConvertHWToBTOR2Pass>,
49 public comb::CombinationalVisitor<ConvertHWToBTOR2Pass>,
50 public sv::Visitor<ConvertHWToBTOR2Pass>,
51 public hw::TypeOpVisitor<ConvertHWToBTOR2Pass>,
52 public verif::Visitor<ConvertHWToBTOR2Pass> {
53public:
54 using verif::Visitor<ConvertHWToBTOR2Pass>::visitVerif;
55
56 ConvertHWToBTOR2Pass(raw_ostream &os) : os(os) {}
57 // Executes the pass
58 void runOnOperation() override;
59
60private:
61 // Output stream in which the btor2 will be emitted
62 raw_ostream &os;
63
64 // Create a counter that attributes a unique id to each generated btor2 line
65 size_t lid = 1; // btor2 line identifiers usually start at 1
66 size_t nclocks = 0;
67
68 // Create maps to keep track of lid associations
69 // We need these in order to reference results as operands in btor2
70
71 // Keeps track of the ids associated to each declared sort
72 // This is used in order to guarantee that sorts are unique and to allow for
73 // instructions to reference the given sorts (key: width, value: LID)
74 DenseMap<size_t, size_t> sortToLIDMap;
75 // Keeps track of {constant, width} -> LID mappings
76 // This is used in order to avoid duplicating constant declarations
77 // in the output btor2. It is also useful when tracking
78 // constants declarations that aren't tied to MLIR ops.
79 DenseMap<APInt, size_t> constToLIDMap;
80 // Keeps track of the most recent update line for each operation
81 // This allows for operations to be used throughout the btor file
82 // with their most recent expression. Btor uses unique identifiers for each
83 // instruction, so we need to have an association between those and MLIR Ops.
84 DenseMap<Operation *, size_t> opLIDMap;
85 // Stores the LID of the associated input.
86 // This holds a similar function as the opLIDMap but keeps
87 // track of block argument index -> LID mappings
88 DenseMap<size_t, size_t> inputLIDs;
89 // Stores all of the register declaration ops.
90 // This allows for the emission of transition arcs for the regs
91 // to be deferred to the end of the pass.
92 // This is necessary, as we need to wait for the `next` operation to
93 // have been converted to btor2 before we can emit the transition.
94 SmallVector<Operation *> regOps;
95
96 // Used to perform a DFS search through the module to declare all operands
97 // before they are used
98 llvm::SmallMapVector<Operation *, OperandRange::iterator, 16> worklist;
99
100 // Keeps track of operations that have been declared
101 DenseSet<Operation *> handledOps;
102
103 // Constants used during the conversion
104 static constexpr size_t noLID = -1UL;
105 [[maybe_unused]] static constexpr int64_t noWidth = -1L;
106
107 /// Field helper functions
108public:
109 // Checks if an operation was declared
110 // If so, its lid will be returned
111 // Otherwise a new lid will be assigned to the op
112 size_t getOpLID(Operation *op) {
113 // Look for the original operation declaration
114 // Make sure that wires are considered when looking for an lid
115 Operation *defOp = op;
116 auto &f = opLIDMap[defOp];
117
118 // If the op isn't associated to an lid, assign it a new one
119 if (!f)
120 f = lid++;
121 return f;
122 }
123
124 // Associates the current lid to an operation
125 // The LID is then incremented to maintain uniqueness
126 size_t setOpLID(Operation *op) {
127 size_t oplid = lid++;
128 opLIDMap[op] = oplid;
129 return oplid;
130 }
131
132 // Checks if an operation was declared
133 // If so, its lid will be returned
134 // Otherwise -1 will be returned
135 size_t getOpLID(Value value) {
136 Operation *defOp = value.getDefiningOp();
137
138 if (auto it = opLIDMap.find(defOp); it != opLIDMap.end())
139 return it->second;
140
141 // Check for special case where op is actually a port
142 // To do so, we start by checking if our operation is a block argument
143 if (BlockArgument barg = dyn_cast<BlockArgument>(value)) {
144 // Extract the block argument index and use that to get the line number
145 size_t argIdx = barg.getArgNumber();
146
147 // Check that the extracted argument is in range before using it
148 if (auto it = inputLIDs.find(argIdx); it != inputLIDs.end())
149 return it->second;
150 }
151
152 // Return -1 if no LID was found
153 return noLID;
154 }
155
156private:
157 // Checks if a sort was declared with the given width
158 // If so, its lid will be returned
159 // Otherwise -1 will be returned
160 size_t getSortLID(size_t w) {
161 if (auto it = sortToLIDMap.find(w); it != sortToLIDMap.end())
162 return it->second;
163
164 // If no lid was found return -1
165 return noLID;
166 }
167
168 // Associate the sort with a new lid
169 size_t setSortLID(size_t w) {
170 size_t sortlid = lid;
171 // Add the width to the declared sorts along with the associated line id
172 sortToLIDMap[w] = lid++;
173 return sortlid;
174 }
175
176 // Checks if a constant of a given size has been declared.
177 // If so, its lid will be returned.
178 // Otherwise -1 will be returned.
179 size_t getConstLID(int64_t val, size_t w) {
180 if (auto it = constToLIDMap.find(APInt(w, val)); it != constToLIDMap.end())
181 return it->second;
182
183 // if no lid was found return -1
184 return noLID;
185 }
186
187 // Associates a constant declaration to a new lid
188 size_t setConstLID(int64_t val, size_t w) {
189 size_t constlid = lid;
190 // Keep track of this value in a constant declaration tracker
191 constToLIDMap[APInt(w, val)] = lid++;
192 return constlid;
193 }
194
195 /// String generation helper functions
196
197 // Generates a sort declaration instruction given a type ("bitvec" or array)
198 // and a width.
199 void genSort(StringRef type, size_t width) {
200 // Check that the sort wasn't already declared
201 if (getSortLID(width) != noLID) {
202 return; // If it has already been declared then return an empty string
203 }
204
205 size_t sortlid = setSortLID(width);
206
207 // Build and return a sort declaration
208 os << sortlid << " "
209 << "sort"
210 << " " << type << " " << width << "\n";
211 }
212
213 // Generates an input declaration given a sort lid and a name.
214 void genInput(size_t inlid, size_t width, StringRef name) {
215 // Retrieve the lid associated with the sort (sid)
216 size_t sid = sortToLIDMap.at(width);
217
218 // Generate input declaration
219 os << inlid << " "
220 << "input"
221 << " " << sid << " " << name << "\n";
222 }
223
224 // Generates a constant declaration given a value, a width and a name.
225 void genConst(APInt value, size_t width, Operation *op) {
226 // For now we're going to assume that the name isn't taken, given that hw
227 // is already in SSA form
228 size_t opLID = getOpLID(op);
229
230 // Retrieve the lid associated with the sort (sid)
231 size_t sid = sortToLIDMap.at(width);
232
233 os << opLID << " "
234 << "constd"
235 << " " << sid << " " << value << "\n";
236 }
237
238 // Generates a zero constant expression
239 size_t genZero(size_t width) {
240 // Check if the constant has been created yet
241 size_t zlid = getConstLID(0, width);
242 if (zlid != noLID)
243 return zlid;
244
245 // Retrieve the lid associated with the sort (sid)
246 size_t sid = sortToLIDMap.at(width);
247
248 // Associate an lid to the new constant
249 size_t constlid = setConstLID(0, width);
250
251 // Build and return the zero btor instruction
252 os << constlid << " "
253 << "zero"
254 << " " << sid << "\n";
255 return constlid;
256 }
257
258 // Generates an init statement, which allows for the use of initial values
259 // operands in compreg registers
260 void genInit(Operation *reg, Value initVal, int64_t width) {
261 // Retrieve the various identifiers we require for this
262 size_t regLID = getOpLID(reg);
263 size_t sid = sortToLIDMap.at(width);
264 size_t initValLID = getOpLID(initVal);
265
266 // Build and emit the string (the lid here doesn't need to be associated
267 // to an op as it won't be used)
268 os << lid++ << " "
269 << "init"
270 << " " << sid << " " << regLID << " " << initValLID << "\n";
271 }
272
273 // Generates a binary operation instruction given an op name, two operands
274 // and a result width.
275 void genBinOp(StringRef inst, Operation *binop, Value op1, Value op2,
276 size_t width) {
277 // TODO: adding support for most variadic ops shouldn't be too hard
278 if (binop->getNumOperands() != 2) {
279 binop->emitError("variadic operations not are not currently supported");
280 return;
281 }
282
283 // Set the LID for this operation
284 size_t opLID = getOpLID(binop);
285
286 // Find the sort's lid
287 size_t sid = sortToLIDMap.at(width);
288
289 // Assuming that the operands were already emitted
290 // Find the LIDs associated to the operands
291 size_t op1LID = getOpLID(op1);
292 size_t op2LID = getOpLID(op2);
293
294 // Build and return the string
295 os << opLID << " " << inst << " " << sid << " " << op1LID << " " << op2LID
296 << "\n";
297 }
298
299 // Generates a slice instruction given an operand, the lowbit, and the width
300 void genSlice(Operation *srcop, Value op0, size_t lowbit, int64_t width) {
301 // Assign a LID to this operation
302 size_t opLID = getOpLID(srcop);
303
304 // Find the sort's associated lid in order to use it in the instruction
305 size_t sid = sortToLIDMap.at(width);
306
307 // Assuming that the operand has already been emitted
308 // Find the LID associated to the operand
309 size_t op0LID = getOpLID(op0);
310
311 // Build and return the slice instruction
312 os << opLID << " "
313 << "slice"
314 << " " << sid << " " << op0LID << " " << (lowbit + width - 1) << " "
315 << lowbit << "\n";
316 }
317
318 // Generates a constant declaration given a value, a width and a name
319 void genUnaryOp(Operation *srcop, Operation *op0, StringRef inst,
320 size_t width) {
321 // Register the source operation with the current line id
322 size_t opLID = getOpLID(srcop);
323
324 // Retrieve the lid associated with the sort (sid)
325 size_t sid = sortToLIDMap.at(width);
326
327 // Assuming that the operand has already been emitted
328 // Find the LID associated to the operand
329 size_t op0LID = getOpLID(op0);
330
331 os << opLID << " " << inst << " " << sid << " " << op0LID << "\n";
332 }
333
334 // Generates a constant declaration given a value, a width and a name and
335 // returns the LID associated to it
336 void genUnaryOp(Operation *srcop, Value op0, StringRef inst, size_t width) {
337 genUnaryOp(srcop, op0.getDefiningOp(), inst, width);
338 }
339
340 // Generates a constant declaration given a operand lid, a width and a name
341 size_t genUnaryOp(size_t op0LID, StringRef inst, size_t width) {
342 // Register the source operation with the current line id
343 size_t curLid = lid++;
344
345 // Retrieve the lid associated with the sort (sid)
346 size_t sid = sortToLIDMap.at(width);
347
348 os << curLid << " " << inst << " " << sid << " " << op0LID << "\n";
349 return curLid;
350 }
351
352 // Generates a constant declaration given a value, a width and a name
353 size_t genUnaryOp(Operation *op0, StringRef inst, size_t width) {
354 return genUnaryOp(getOpLID(op0), inst, width);
355 }
356
357 // Generates a constant declaration given a value, a width and a name and
358 // returns the LID associated to it
359 size_t genUnaryOp(Value op0, StringRef inst, size_t width) {
360 return genUnaryOp(getOpLID(op0), inst, width);
361 }
362
363 // Generate a btor2 assertion given an assertion operation
364 // Note that a predicate inversion must have already been generated at this
365 // point
366 void genBad(Operation *assertop) {
367 // Start by finding the expression lid
368 size_t assertLID = getOpLID(assertop);
369 genBad(assertLID);
370 }
371
372 // Generate a btor2 assertion given an assertion operation's LID
373 // Note that a predicate inversion must have already been generated at this
374 // point
375 void genBad(size_t assertLID) {
376 // Build and return the btor2 string
377 // Also update the lid as this instruction is not associated to an mlir op
378 os << lid++ << " "
379 << "bad"
380 << " " << assertLID << "\n";
381 }
382
383 // Generate a btor2 constraint given an expression from an assumption
384 // operation
385 void genConstraint(Value expr) {
386 // Start by finding the expression lid
387 size_t exprLID = getOpLID(expr);
388
389 genConstraint(exprLID);
390 }
391
392 // Generate a btor2 constraint given an expression from an assumption
393 // operation
394 void genConstraint(size_t exprLID) {
395 // Build and return the btor2 string
396 // Also update the lid as this instruction is not associated to an mlir op
397 os << lid++ << " "
398 << "constraint"
399 << " " << exprLID << "\n";
400 }
401
402 // Generate an ite instruction (if then else) given a predicate, two values
403 // and a res width
404 void genIte(Operation *srcop, Value cond, Value t, Value f, int64_t width) {
405 // Retrieve the operand lids, assuming they were emitted
406 size_t condLID = getOpLID(cond);
407 size_t tLID = getOpLID(t);
408 size_t fLID = getOpLID(f);
409
410 genIte(srcop, condLID, tLID, fLID, width);
411 }
412
413 // Generate an ite instruction (if then else) given a predicate, two values
414 // and a res width
415 void genIte(Operation *srcop, size_t condLID, size_t tLID, size_t fLID,
416 int64_t width) {
417 // Register the source operation with the current line id
418 size_t opLID = getOpLID(srcop);
419
420 // Retrieve the lid associated with the sort (sid)
421 size_t sid = sortToLIDMap.at(width);
422
423 // Build and return the ite instruction
424 os << opLID << " "
425 << "ite"
426 << " " << sid << " " << condLID << " " << tLID << " " << fLID << "\n";
427 }
428
429 // Generate a logical implication given a lhs and a rhs
430 size_t genImplies(Operation *srcop, Value lhs, Value rhs) {
431 // Retrieve LIDs for the lhs and rhs
432 size_t lhsLID = getOpLID(lhs);
433 size_t rhsLID = getOpLID(rhs);
434
435 return genImplies(srcop, lhsLID, rhsLID);
436 }
437
438 // Generate a logical implication given a lhs and a rhs
439 size_t genImplies(Operation *srcop, size_t lhsLID, size_t rhsLID) {
440 // Register the source operation with the current line id
441 size_t opLID = getOpLID(srcop);
442 return genImplies(opLID, lhsLID, rhsLID);
443 }
444
445 size_t genImplies(size_t opLID, size_t lhsLID, size_t rhsLID) {
446 // Retrieve the lid associated with the sort (sid)
447 size_t sid = sortToLIDMap.at(1);
448 // Build and emit the implies operation
449 os << opLID << " "
450 << "implies"
451 << " " << sid << " " << lhsLID << " " << rhsLID << "\n";
452 return opLID;
453 }
454
455 // Generates a state instruction given a width and a name
456 void genState(Operation *srcop, int64_t width, StringRef name) {
457 // Register the source operation with the current line id
458 size_t opLID = getOpLID(srcop);
459
460 // Retrieve the lid associated with the sort (sid)
461 size_t sid = sortToLIDMap.at(width);
462
463 // Build and return the state instruction
464 os << opLID << " "
465 << "state"
466 << " " << sid << " " << name << "\n";
467 }
468
469 // Generates a next instruction, given a width, a state LID, and a next
470 // value LID
471 void genNext(Value next, Operation *reg, int64_t width) {
472 // Retrieve the lid associated with the sort (sid)
473 size_t sid = sortToLIDMap.at(width);
474
475 // Retrieve the LIDs associated to reg and next
476 size_t regLID = getOpLID(reg);
477 size_t nextLID = getOpLID(next);
478
479 // Build and return the next instruction
480 // Also update the lid as this instruction is not associated to an mlir op
481 os << lid++ << " "
482 << "next"
483 << " " << sid << " " << regLID << " " << nextLID << "\n";
484 }
485
486 // Verifies that the sort required for the given operation's btor2 emission
487 // has been generated
488 int64_t requireSort(mlir::Type type) {
489 // Start by figuring out what sort needs to be generated
490 int64_t width = hw::getBitWidth(type);
491
492 // Sanity check: getBitWidth can technically return -1 it is a type with
493 // no width (like a clock). This shouldn't be allowed as width is required
494 // to generate a sort
495 assert(width != noWidth);
496
497 // Generate the sort regardles of resulting width (nothing will be added
498 // if the sort already exists)
499 genSort("bitvec", width);
500 return width;
501 }
502
503 // Generates the transitions required to finalize the register to state
504 // transition system conversion
505 void finalizeRegVisit(Operation *op) {
506 int64_t width;
507 Value next, reset, resetVal;
508
509 // Extract the operands depending on the register type
510 if (auto reg = dyn_cast<seq::CompRegOp>(op)) {
511 width = hw::getBitWidth(reg.getType());
512 next = reg.getInput();
513 reset = reg.getReset();
514 resetVal = reg.getResetValue();
515 } else if (auto reg = dyn_cast<seq::FirRegOp>(op)) {
516 width = hw::getBitWidth(reg.getType());
517 next = reg.getNext();
518 reset = reg.getReset();
519 resetVal = reg.getResetValue();
520 } else {
521 op->emitError("Invalid register operation !");
522 return;
523 }
524
525 genSort("bitvec", width);
526
527 // Next should already be associated to an LID at this point
528 // As we are going to override it, we need to keep track of the original
529 // instruction
530 size_t nextLID = noLID;
531
532 // We need to check if the next value is a port to avoid nullptrs
533 // To do so, we start by checking if our operation is a block argument
534 if (BlockArgument barg = dyn_cast<BlockArgument>(next)) {
535 // Extract the block argument index and use that to get the line number
536 size_t argIdx = barg.getArgNumber();
537
538 // Check that the extracted argument is in range before using it
539 nextLID = inputLIDs[argIdx];
540
541 } else {
542 nextLID = getOpLID(next);
543 }
544
545 // Check if the register has a reset
546 if (reset) {
547 size_t resetValLID = noLID;
548
549 // Check if the reset signal is a port to avoid nullptrs (as done above
550 // with next)
551 size_t resetLID = noLID;
552 if (BlockArgument barg = dyn_cast<BlockArgument>(reset)) {
553 // Extract the block argument index and use that to get the line
554 // number
555 size_t argIdx = barg.getArgNumber();
556
557 // Check that the extracted argument is in range before using it
558 resetLID = inputLIDs[argIdx];
559
560 } else {
561 resetLID = getOpLID(reset);
562 }
563
564 // Check for a reset value, if none exists assume it's zero
565 if (resetVal)
566 resetValLID = getOpLID(resetVal.getDefiningOp());
567 else
568 resetValLID = genZero(width);
569
570 // Assign a new LID to next
571 setOpLID(next.getDefiningOp());
572
573 // Sanity check: at this point the next operation should have had it's
574 // btor2 counterpart emitted if not then something terrible must have
575 // happened.
576 assert(nextLID != noLID);
577
578 // Generate the ite for the register update reset condition
579 // i.e. reg <= reset ? 0 : next
580 genIte(next.getDefiningOp(), resetLID, resetValLID, nextLID, width);
581 } else {
582 // Sanity check: next should have been assigned
583 if (nextLID == noLID) {
584 next.getDefiningOp()->emitError(
585 "Register input does not point to a valid op!");
586 return;
587 }
588 }
589
590 // Finally generate the next statement
591 genNext(next, op, width);
592 }
593
594public:
595 /// Visitor Methods used later on for pattern matching
596
597 // Visitor for the inputs of the module.
598 // This will generate additional sorts and input declaration explicitly for
599 // btor2 Note that outputs are ignored in btor2 as they do not contribute to
600 // the final assertions
601 void visit(hw::PortInfo &port) {
602 // Separate the inputs from outputs and generate the first btor2 lines for
603 // input declaration We only consider ports with an explicit bit-width (so
604 // ignore clocks and immutables)
605 if (port.isInput() && !isa<seq::ClockType, seq::ImmutableType>(port.type)) {
606 // Generate the associated btor declaration for the inputs
607 StringRef iName = port.getName();
608
609 // Guarantees that a sort will exist for the generation of this port's
610 // translation into btor2
611 int64_t w = requireSort(port.type);
612
613 // Save lid for later
614 size_t inlid = lid;
615
616 // Record the defining operation's line ID (the module itself in the
617 // case of ports)
618 inputLIDs[port.argNum] = lid;
619
620 // Increment the lid to keep it unique
621 lid++;
622
623 genInput(inlid, w, iName);
624 }
625 }
626
627 // Emits the associated btor2 operation for a constant. Note that for
628 // simplicity, we will only emit `constd` in order to avoid bit-string
629 // conversions
630 void visitTypeOp(hw::ConstantOp op) {
631 // Make sure the constant hasn't already been created
632 if (handledOps.contains(op))
633 return;
634
635 // Make sure that a sort has been created for our operation
636 int64_t w = requireSort(op.getType());
637
638 // Prepare for for const generation by extracting the const value and
639 // generting the btor2 string
640 genConst(op.getValue(), w, op);
641 }
642
643 // Wires should have been removed in PrepareForFormal
644 void visit(hw::WireOp op) {
645 op->emitError("Wires are not supported in btor!");
646 return signalPassFailure();
647 }
648
649 void visitTypeOp(Operation *op) { visitInvalidTypeOp(op); }
650
651 // Handles non-hw operations
652 void visitInvalidTypeOp(Operation *op) {
653 // Try comb ops
654 dispatchCombinationalVisitor(op);
655 }
656
657 // Binary operations are all emitted the same way, so we can group them into
658 // a single method.
659 template <typename Op>
660 void visitBinOp(Op op, StringRef inst) {
661 // Generete the sort
662 int64_t w = requireSort(op.getType());
663
664 // Start by extracting the operands
665 Value op1 = op.getOperand(0);
666 Value op2 = op.getOperand(1);
667
668 // Generate the line
669 genBinOp(inst, op, op1, op2, w);
670 }
671
672 // Visitors for the binary ops
673 void visitComb(comb::AddOp op) { visitBinOp(op, "add"); }
674 void visitComb(comb::SubOp op) { visitBinOp(op, "sub"); }
675 void visitComb(comb::MulOp op) { visitBinOp(op, "mul"); }
676 void visitComb(comb::DivSOp op) { visitBinOp(op, "sdiv"); }
677 void visitComb(comb::DivUOp op) { visitBinOp(op, "udiv"); }
678 void visitComb(comb::ModSOp op) { visitBinOp(op, "smod"); }
679 void visitComb(comb::ShlOp op) { visitBinOp(op, "sll"); }
680 void visitComb(comb::ShrUOp op) { visitBinOp(op, "srl"); }
681 void visitComb(comb::ShrSOp op) { visitBinOp(op, "sra"); }
682 void visitComb(comb::AndOp op) { visitBinOp(op, "and"); }
683 void visitComb(comb::OrOp op) { visitBinOp(op, "or"); }
684 void visitComb(comb::XorOp op) { visitBinOp(op, "xor"); }
685 void visitComb(comb::ConcatOp op) { visitBinOp(op, "concat"); }
686
687 // Extract ops translate to a slice operation in btor2 in a one-to-one
688 // manner
689 void visitComb(comb::ExtractOp op) {
690 int64_t w = requireSort(op.getType());
691
692 // Start by extracting the necessary information for the emission (i.e.
693 // operand, low bit, ...)
694 Value op0 = op.getOperand();
695 size_t lb = op.getLowBit();
696
697 // Generate the slice instruction
698 genSlice(op, op0, lb, w);
699 }
700
701 // Btor2 uses similar syntax as hw for its comparisons
702 // So we simply need to emit the cmpop name and check for corner cases
703 // where the namings differ.
704 void visitComb(comb::ICmpOp op) {
705 Value lhs = op.getOperand(0);
706 Value rhs = op.getOperand(1);
707
708 // Extract the predicate name (assuming that its a valid btor2
709 // predicate)
710 StringRef pred = stringifyICmpPredicate(op.getPredicate());
711
712 // Check for special cases where hw doesn't align with btor syntax
713 if (pred == "ne")
714 pred = "neq";
715 else if (pred == "ule")
716 pred = "ulte";
717 else if (pred == "sle")
718 pred = "slte";
719 else if (pred == "uge")
720 pred = "ugte";
721 else if (pred == "sge")
722 pred = "sgte";
723
724 // Width of result is always 1 for comparison
725 genSort("bitvec", 1);
726
727 // With the special cases out of the way, the emission is the same as that
728 // of a binary op
729 genBinOp(pred, op, lhs, rhs, 1);
730 }
731
732 // Muxes generally convert to an ite statement
733 void visitComb(comb::MuxOp op) {
734 // Extract predicate, true and false values
735 Value pred = op.getCond();
736 Value tval = op.getTrueValue();
737 Value fval = op.getFalseValue();
738
739 // We assume that both tval and fval have the same width
740 // This width should be the same as the output width
741 int64_t w = requireSort(op.getType());
742
743 // Generate the ite instruction
744 genIte(op, pred, tval, fval, w);
745 }
746
747 void visitComb(Operation *op) { visitInvalidComb(op); }
748
749 // Try sv ops when comb is done
750 void visitInvalidComb(Operation *op) { dispatchSVVisitor(op); }
751
752 // Assertions are negated then converted to a btor2 bad instruction
753 void visitSV(sv::AssertOp op) {
754 // Expression is what we will try to invert for our assertion
755 Value expr = op.getExpression();
756
757 // This sort is for assertion inversion and potential implies
758 genSort("bitvec", 1);
759
760 // Check for an overaching enable
761 // In our case the sv.if operation will probably only be used when
762 // conditioning an sv.assert on an enable signal. This means that
763 // its condition is probably used to imply our assertion
764 if (auto ifop = dyn_cast<sv::IfOp>(((Operation *)op)->getParentOp())) {
765 Value en = ifop.getOperand();
766
767 // Generate the implication
768 genImplies(ifop, en, expr);
769
770 // Generate the implies inversion
771 genUnaryOp(op, ifop, "not", 1);
772 } else {
773 // Generate the expression inversion
774 genUnaryOp(op, expr, "not", 1);
775 }
776
777 // Generate the bad btor2 instruction
778 genBad(op);
779 }
780 // Assumptions are converted to a btor2 constraint instruction
781 void visitSV(sv::AssumeOp op) {
782 // Extract the expression that we want our constraint to be about
783 Value expr = op.getExpression();
784 genConstraint(expr);
785 }
786
787 void visitSV(Operation *op) { visitInvalidSV(op); }
788
789 // Once SV Ops are visited, we need to check for seq ops
790 void visitInvalidSV(Operation *op) { dispatchVerifVisitor(op); }
791
792 template <typename Op>
793 void visitAssertLike(Op op) {
794 // Expression is what we will try to invert for our assertion
795 Value prop = op.getProperty();
796 Value en = op.getEnable();
797
798 // This sort is for assertion inversion and potential implies
799 genSort("bitvec", 1);
800
801 size_t assertLID = noLID;
802 // Check for a related enable signal
803 if (en) {
804 // Generate the implication
805 genImplies(op, en, prop);
806
807 // Generate the implies inversion
808 assertLID = genUnaryOp(op, "not", 1);
809 } else {
810 // Generate the expression inversion
811 assertLID = genUnaryOp(prop.getDefiningOp(), "not", 1);
812 }
813
814 // Generate the bad btor2 instruction
815 genBad(assertLID);
816 }
817
818 template <typename Op>
819 void visitAssumeLike(Op op) {
820 // Expression is what we will try to invert for our assertion
821 Value prop = op.getProperty();
822 Value en = op.getEnable();
823
824 size_t assumeLID = getOpLID(prop);
825 // Check for a related enable signal
826 if (en) {
827 // This sort is for assertion inversion and potential implies
828 genSort("bitvec", 1);
829 // Generate the implication
830 assumeLID = genImplies(op, en, prop);
831 }
832
833 // Generate the bad btor2 instruction
834 genConstraint(assumeLID);
835 }
836
837 // Folds the enable signal into the property and converts the result into a
838 // bad instruction.
839 void visitVerif(verif::AssertOp op) { visitAssertLike(op); }
840 void visitVerif(verif::ClockedAssertOp op) { visitAssertLike(op); }
841
842 // Fold the enable into the property and convert the assumption into a
843 // constraint instruction.
844 void visitVerif(verif::AssumeOp op) { visitAssumeLike(op); }
845 void visitVerif(verif::ClockedAssumeOp op) { visitAssumeLike(op); }
846
847 void visitUnhandledVerif(Operation *op) {
848 op->emitError("not supported in btor2!");
849 return signalPassFailure();
850 }
851
852 void visitInvalidVerif(Operation *op) { visit(op); }
853
854 // Seq operation visitor, that dispatches to other seq ops
855 // Also handles all remaining operations that should be explicitly ignored
856 void visit(Operation *op) {
857 // Typeswitch is used here because other seq types will be supported
858 // like all operations relating to memories and CompRegs
859 TypeSwitch<Operation *, void>(op)
860 .Case<seq::FirRegOp, seq::CompRegOp>([&](auto expr) { visit(expr); })
861 .Default([&](auto expr) { visitUnsupportedOp(op); });
862 }
863
864 // Firrtl registers generate a state instruction
865 // The final update is also used to generate a set of next btor
866 // instructions
867 void visit(seq::FirRegOp reg) {
868 // Start by retrieving the register's name and width
869 StringRef regName = reg.getName();
870 int64_t w = requireSort(reg.getType());
871
872 // Generate state instruction (represents the register declaration)
873 genState(reg, w, regName);
874
875 // Record the operation for future `next` instruction generation
876 // This is required to model transitions between states (i.e. how a
877 // register's value evolves over time)
878 regOps.push_back(reg);
879 }
880
881 // Compregs behave in a similar way as firregs for btor2 emission
882 void visit(seq::CompRegOp reg) {
883 // Start by retrieving the register's name and width
884 StringRef regName = reg.getName().value();
885 int64_t w = requireSort(reg.getType());
886
887 // Check for initial values which must be emitted before the state in
888 // btor2
889 auto init = reg.getInitialValue();
890
891 // If there's an initial value, we need to generate a constant for the
892 // initial value, then declare the state, then generate the init statement
893 // (BTOR2 parsers are picky about it being in this order)
894 if (init) {
895 if (!init.getDefiningOp<seq::InitialOp>()) {
896 reg->emitError(
897 "Initial value must be emitted directly by a seq.initial op");
898 return;
899 }
900 // Check that the initial value is a non-null constant
901 auto initialConstant = circt::seq::unwrapImmutableValue(init)
902 .getDefiningOp<hw::ConstantOp>();
903 if (!initialConstant)
904 reg->emitError("initial value must be constant");
905
906 // Visit the initial Value to generate the constant
907 dispatchTypeOpVisitor(initialConstant);
908
909 // Add it to the list of visited operations
910 handledOps.insert(initialConstant);
911
912 // Now we can declare the state
913 genState(reg, w, regName);
914
915 // Finally generate the init statement
916 genInit(reg, initialConstant, w);
917 } else {
918 // Just generate state instruction (represents the register declaration)
919 genState(reg, w, regName);
920 }
921
922 // Record the operation for future `next` instruction generation
923 // This is required to model transitions between states (i.e. how a
924 // register's value evolves over time)
925 regOps.push_back(reg);
926 }
927
928 // Ignore all other explicitly mentionned operations
929 // ** Purposefully left empty **
930 void ignore(Operation *op) {}
931
932 // Tail method that handles all operations that weren't handled by previous
933 // visitors. Here we simply make the pass fail or ignore the op
934 void visitUnsupportedOp(Operation *op) {
935 // Check for explicitly ignored ops vs unsupported ops (which cause a
936 // failure)
937 TypeSwitch<Operation *, void>(op)
938 // All explicitly ignored operations are defined here
939 .Case<sv::MacroDefOp, sv::MacroDeclOp, sv::VerbatimOp,
940 sv::VerbatimExprOp, sv::VerbatimExprSEOp, sv::IfOp, sv::IfDefOp,
941 sv::IfDefProceduralOp, sv::AlwaysOp, sv::AlwaysCombOp,
942 seq::InitialOp, sv::AlwaysFFOp, seq::FromClockOp, seq::InitialOp,
943 seq::YieldOp, hw::OutputOp, hw::HWModuleOp>(
944 [&](auto expr) { ignore(op); })
945
946 // Make sure that the design only contains one clock
947 .Case<seq::FromClockOp>([&](auto expr) {
948 if (++nclocks > 1UL) {
949 op->emitOpError("Mutli-clock designs are not supported!");
950 return signalPassFailure();
951 }
952 })
953
954 // Anything else is considered unsupported and might cause a wrong
955 // behavior if ignored, so an error is thrown
956 .Default([&](auto expr) {
957 op->emitOpError("is an unsupported operation");
958 return signalPassFailure();
959 });
960 }
961};
962} // end anonymous namespace
963
964void ConvertHWToBTOR2Pass::runOnOperation() {
965 // Btor2 does not have the concept of modules or module
966 // hierarchies, so we assume that no nested modules exist at this point.
967 // This greatly simplifies translation.
968 getOperation().walk([&](hw::HWModuleOp module) {
969 // Start by extracting the inputs and generating appropriate instructions
970 for (auto &port : module.getPortList()) {
971 visit(port);
972 }
973
974 // Previsit all registers in the module in order to avoid dependency cycles
975 module.walk([&](Operation *op) {
976 TypeSwitch<Operation *, void>(op)
977 .Case<seq::FirRegOp, seq::CompRegOp>([&](auto reg) {
978 visit(reg);
979 handledOps.insert(op);
980 })
981 .Default([&](auto expr) {});
982 });
983
984 // Visit all of the operations in our module
985 module.walk([&](Operation *op) {
986 // Check: instances are not (yet) supported
987 if (isa<hw::InstanceOp>(op)) {
988 op->emitOpError("not supported in BTOR2 conversion");
989 return;
990 }
991
992 // Don't process ops that have already been emitted
993 if (handledOps.contains(op))
994 return;
995
996 // Fill in our worklist
997 worklist.insert({op, op->operand_begin()});
998
999 // Process the elements in our worklist
1000 while (!worklist.empty()) {
1001 auto &[op, operandIt] = worklist.back();
1002 if (operandIt == op->operand_end()) {
1003 // All of the operands have been emitted, it is safe to emit our op
1004 dispatchTypeOpVisitor(op);
1005
1006 // Record that our op has been emitted
1007 handledOps.insert(op);
1008 worklist.pop_back();
1009 continue;
1010 }
1011
1012 // Send the operands of our op to the worklist in case they are still
1013 // un-emitted
1014 Value operand = *(operandIt++);
1015 auto *defOp = operand.getDefiningOp();
1016
1017 // Make sure that we don't emit the same operand twice
1018 if (!defOp || handledOps.contains(defOp))
1019 continue;
1020
1021 // This is triggered if our operand is already in the worklist and
1022 // wasn't handled
1023 if (!worklist.insert({defOp, defOp->operand_begin()}).second) {
1024 defOp->emitError("dependency cycle");
1025 return;
1026 }
1027 }
1028 });
1029
1030 // Iterate through the registers and generate the `next` instructions
1031 for (size_t i = 0; i < regOps.size(); ++i) {
1032 finalizeRegVisit(regOps[i]);
1033 }
1034 });
1035 // Clear data structures to allow for pass reuse
1036 sortToLIDMap.clear();
1037 constToLIDMap.clear();
1038 opLIDMap.clear();
1039 inputLIDs.clear();
1040 regOps.clear();
1041 handledOps.clear();
1042 worklist.clear();
1043}
1044
1045// Constructor with a custom ostream
1046std::unique_ptr<mlir::Pass>
1048 return std::make_unique<ConvertHWToBTOR2Pass>(os);
1049}
1050
1051// Basic default constructor
1052std::unique_ptr<mlir::Pass> circt::createConvertHWToBTOR2Pass() {
1053 return std::make_unique<ConvertHWToBTOR2Pass>(llvm::outs());
1054}
assert(baseType &&"element must be base type")
static SmallVector< PortInfo > getPortList(ModuleTy &mod)
Definition HWOps.cpp:1427
This helps visit Combinational nodes.
This helps visit TypeOp nodes.
Definition HWVisitors.h:25
Value unwrapImmutableValue(mlir::TypedValue< seq::ImmutableType > immutableVal)
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
std::unique_ptr< mlir::Pass > createConvertHWToBTOR2Pass()
Definition hw.py:1
reg(value, clock, reset=None, reset_value=None, name=None, sym_name=None)
Definition seq.py:21
mlir::Type type
Definition HWTypes.h:31
This holds the name, type, direction of a module's ports.
StringRef getName() const
size_t argNum
This is the argument index or the result index depending on the direction.