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