[HWToBTOR2] Emit verif.symbolic_value as input

lib/Conversion/HWToBTOR2/HWToBTOR2.cpp

@@ -704,7 +704,7 @@ struct ConvertHWToBTOR2Pass
   // the final assertions
   void visit(hw::PortInfo &port) {
     // Separate the inputs from outputs and generate the first btor2 lines for
-    // input declaration We only consider ports with an explicit bit-width (so
+    // input declaration. We only consider ports with an explicit bit-width (so
     // ignore clocks and immutables)
     if (port.isInput() && !isa<seq::ClockType, seq::ImmutableType>(port.type)) {
       // Generate the associated btor declaration for the inputs
@@ -1002,6 +1002,25 @@ struct ConvertHWToBTOR2Pass
   void visitVerif(verif::AssumeOp op) { visitAssumeLike(op); }
   void visitVerif(verif::ClockedAssumeOp op) { visitAssumeLike(op); }
 
+  // Symbolic values get handled the same way as block arguments.
+  // The one difference if that we treat them as regular opertions rather than
+  // block arguments, i.e. we don't need to special case store these inputLIDs
+  // and can simply store them in opLIDs like the other operations.
+  void visitVerif(verif::SymbolicValueOp op) {
+    // Retrieve name, make sure it's unique
+    auto name = symbolNamespace.newName(op.getName().value_or(""));
+
+    // Guarantees that a sort will exist for the generation of this symbolic
+    // value's translation into btor2
+    int64_t w = requireSort(op.getType());
+
+    // Store and generate a new lid
+    size_t inlid = setOpLID(op.getOperation());
+
+    // Generate the input in btor2
+    genInput(inlid, w, name);
+  }
+
   // Error out on most unhandled verif ops
   void visitUnhandledVerif(Operation *op) {
     op->emitError("not supported in btor2!");
@@ -1163,14 +1182,9 @@ struct ConvertHWToBTOR2Pass
           return signalPassFailure();
         });
   }
-};
-} // end anonymous namespace
 
-void ConvertHWToBTOR2Pass::runOnOperation() {
-  // Btor2 does not have the concept of modules or module
-  // hierarchies, so we assume that no nested modules exist at this point.
-  // This greatly simplifies translation.
-  getOperation().walk([&](hw::HWModuleOp module) {
+  /// Prepares and visits all of the ports in a module
+  LogicalResult visitPorts(hw::HWModuleOp module) {
     // Start by extracting the inputs and generating appropriate instructions
     for (auto &port : module.getPortList()) {
       // Check whether the port is used as a clock
@@ -1186,16 +1200,35 @@ void ConvertHWToBTOR2Pass::runOnOperation() {
           if (portVal.getNumUses() > 1) {
             module.emitError(
                 "Inputs converted to clocks may only have one user.");
-            return signalPassFailure();
+            return failure();
           }
           // Ports used as clocks should be implicit so don't visit them
           continue;
         }
       }
+      // Once ready, run actual port visitor
       visit(port);
     }
+    return success();
+  }
+
+  /// Checks if a given operation is a supported modulelike
+  template <typename T>
+  bool isSuportedModule(T module) {
+    bool supported = isa<hw::HWModuleOp, verif::FormalOp>(module);
+    if (!supported)
+      module.emitError("Unsupported module type!");
+    return supported;
+  }
+
+  /// Previsits all registers in a given module (avoids dependency cycles)
+  template <typename T>
+  LogicalResult preVisitRegs(T module) {
+    // Sanity check
+    if (!isSuportedModule(module))
+      return failure();
 
-    // Previsit all registers in the module in order to avoid dependency cycles
+    // Find all supported registers and visit them
     module.walk([&](Operation *op) {
       TypeSwitch<Operation *, void>(op)
           .Case<seq::FirRegOp, seq::CompRegOp>([&](auto reg) {
@@ -1205,12 +1238,22 @@ void ConvertHWToBTOR2Pass::runOnOperation() {
           .Default([&](auto expr) {});
     });
 
+    return success();
+  }
+
+  /// Visits all of the regular operations in our module
+  template <typename T>
+  LogicalResult visitBodyOps(T module) {
+    // Sanity check
+    if (!isSuportedModule(module))
+      return failure();
+
     // Visit all of the operations in our module
     module.walk([&](Operation *op) {
       // Check: instances are not (yet) supported
       if (isa<hw::InstanceOp>(op)) {
         op->emitOpError("not supported in BTOR2 conversion");
-        return;
+        return signalPassFailure();
       }
 
       // Don't process ops that have already been emitted
@@ -1224,7 +1267,8 @@ void ConvertHWToBTOR2Pass::runOnOperation() {
       while (!worklist.empty()) {
         auto &[op, operandIt] = worklist.back();
         if (operandIt == op->operand_end()) {
-          // All of the operands have been emitted, it is safe to emit our op
+          // All of the operands have been emitted, it is safe to emit our
+          // op
           dispatchTypeOpVisitor(op);
 
           // Record that our op has been emitted
@@ -1233,8 +1277,8 @@ void ConvertHWToBTOR2Pass::runOnOperation() {
           continue;
         }
 
-        // Send the operands of our op to the worklist in case they are still
-        // un-emitted
+        // Send the operands of our op to the worklist in case they are
+        // still un-emitted
         Value operand = *(operandIt++);
         auto *defOp = operand.getDefiningOp();
 
@@ -1246,16 +1290,51 @@ void ConvertHWToBTOR2Pass::runOnOperation() {
         // wasn't handled
         if (!worklist.insert({defOp, defOp->operand_begin()}).second) {
           defOp->emitError("dependency cycle");
-          return;
+          return signalPassFailure();
         }
       }
     });
 
+    return success();
+  }
+
+  /// Handles the core logic of the pass, in a generic manner
+  template <typename T>
+  LogicalResult handleTopLevel(T module) {
+    if (isa<hw::HWModuleOp>(module)) {
+      // Start by extracting the inputs and generating appropriate instructions
+      if (failed(visitPorts(module)))
+        return failure();
+    }
+    // Previsit all registers in the module in order to avoid dependency
+    // cycles
+    if (failed(preVisitRegs(module)))
+      return failure();
+
+    // Visit all of the operations in our module
+    if (failed(visitBodyOps(module)))
+      return failure();
+
     // Iterate through the registers and generate the `next` instructions
-    for (size_t i = 0; i < regOps.size(); ++i) {
+    for (size_t i = 0; i < regOps.size(); ++i)
       finalizeRegVisit(regOps[i]);
-    }
+
+    return success();
+  }
+};
+} // end anonymous namespace
+
+void ConvertHWToBTOR2Pass::runOnOperation() {
+  // Btor2 does not have the concept of modules or module
+  // hierarchies, so we assume that no nested modules exist at this point.
+  // This greatly simplifies translation.
+  // We also consider hw::HWModuleOp and verif::FormalOp as the same
+  auto top = getOperation();
+  top.walk([&](hw::HWModuleOp module) {
+    if (failed(handleTopLevel(module)))
+      return signalPassFailure();
   });
+
   // Clear data structures to allow for pass reuse
   sortToLIDMap.clear();
   constToLIDMap.clear();

test/Conversion/HWToBTOR2/symbolic.mlir

@@ -0,0 +1,21 @@
+// RUN: circt-opt %s --convert-hw-to-btor2 -o %t | FileCheck %s  
+
+// CHECK: [[I32:[0-9]+]] sort bitvec 32
+// CHECK: [[A:[0-9]+]] input [[I32]] a
+// CHECK: [[B:[0-9]+]] input [[I32]] b
+// CHECK: [[C:[0-9]+]] input [[I32]] c
+// CHECK: [[ADD:[0-9]+]] add [[I32]] [[A]] [[B]]
+// CHECK: [[I1:[0-9]+]] sort bitvec 1
+// CHECK: [[RES:[0-9]+]] eq [[I1]] [[ADD]] [[C]]
+// CHECK: [[NOT:[0-9]+]] not [[I1]] [[RES]]
+// CHECK: [[BAD:[0-9]+]] bad [[NOT]]
+
+module {
+  hw.module @foo(in %a : i32) {
+    %b = verif.symbolic_value : i32
+    %c = verif.symbolic_value : i32
+    %res = comb.add %a, %b : i32 
+    %cond = comb.icmp eq %res, %c : i32
+    verif.assert %cond : i1
+  }
+}