[Verif] Add ContractOp to Visitor (#8155)

Add the `ContractOp` to the `verif::Visitor`. This requires a minor tweak to the HWToBTOR2 pass to handle unknown operations more generally.
llvm · Jan 30, 2025 · 0a111c7 · 0a111c7
1 parent 8d2f1ec
commit 0a111c7
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 9 deletions.
diff --git a/include/circt/Dialect/Verif/VerifVisitors.h b/include/circt/Dialect/Verif/VerifVisitors.h
@@ -22,7 +22,7 @@ class Visitor {
     auto *thisCast = static_cast<ConcreteType *>(this);
     return TypeSwitch<Operation *, ResultType>(op)
         .template Case<AssertOp, AssumeOp, CoverOp, ClockedAssertOp,
-                       ClockedAssumeOp, ClockedCoverOp>(
+                       ClockedAssumeOp, ClockedCoverOp, ContractOp>(
             [&](auto op) -> ResultType {
               return thisCast->visitVerif(op, args...);
             })
@@ -55,6 +55,7 @@ class Visitor {
   HANDLE(ClockedAssertOp, Unhandled);
   HANDLE(ClockedAssumeOp, Unhandled);
   HANDLE(ClockedCoverOp, Unhandled);
+  HANDLE(ContractOp, Unhandled);
 #undef HANDLE
 };
 

diff --git a/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp b/lib/Conversion/HWToBTOR2/HWToBTOR2.cpp
@@ -52,6 +52,8 @@ struct ConvertHWToBTOR2Pass
       public hw::TypeOpVisitor<ConvertHWToBTOR2Pass>,
       public verif::Visitor<ConvertHWToBTOR2Pass> {
 public:
+  using verif::Visitor<ConvertHWToBTOR2Pass>::visitVerif;
+
   ConvertHWToBTOR2Pass(raw_ostream &os) : os(os) {}
   // Executes the pass
   void runOnOperation() override;
@@ -843,14 +845,8 @@ struct ConvertHWToBTOR2Pass
   void visitVerif(verif::AssumeOp op) { visitAssumeLike(op); }
   void visitVerif(verif::ClockedAssumeOp op) { visitAssumeLike(op); }
 
-  // Cover is not supported in btor2
-  void visitVerif(verif::CoverOp op) {
-    op->emitError("Cover is not supported in btor2!");
-    return signalPassFailure();
-  }
-
-  void visitVerif(verif::ClockedCoverOp op) {
-    op->emitError("Cover is not supported in btor2!");
+  void visitUnhandledVerif(Operation *op) {
+    op->emitError("not supported in btor2!");
     return signalPassFailure();
   }