[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
@@ -1008,6 +1008,25 @@ struct ConvertHWToBTOR2Pass
     return signalPassFailure();
   }
 
+  // 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);
+  }
+
   // Dispatch next visitors
   void visitInvalidVerif(Operation *op) { visit(op); }
 

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
+  }
+}