[SV][Verif] Extract verif ops in SVExtractTestCode (#6865)

Fix a bug where SVExtractTestCode was not extracting asserts, assumes, and covers from the verif dialect. This resulted in unexpected end-to-end "failures" from Chisel where Chisel asserts, assumes, and covers were not extracted and left in the design. Fixes #6864. Signed-off-by: Schuyler Eldridge <[email protected]>
llvm · Mar 24, 2024 · 08fb99b · 08fb99b
1 parent f8c7fae
commit 08fb99b
Show file tree

Hide file tree

Showing 7 changed files with 53 additions and 14 deletions.
diff --git a/include/circt/Dialect/SV/SVPasses.td b/include/circt/Dialect/SV/SVPasses.td
@@ -97,7 +97,10 @@ def SVExtractTestCode : Pass<"sv-extract-test-code", "ModuleOp"> {
   }];
 
   let constructor = "circt::sv::createSVExtractTestCodePass()";
-  let dependentDialects = ["circt::sv::SVDialect"];
+  let dependentDialects = [
+    "circt::sv::SVDialect",
+    "circt::verif::VerifDialect"
+  ];
   let options = [
     Option<"disableInstanceExtraction", "disable-instance-extraction", "bool",
            "false", "Disable extracting instances only that feed test code">,

diff --git a/lib/Dialect/SV/CMakeLists.txt b/lib/Dialect/SV/CMakeLists.txt
@@ -17,6 +17,7 @@ add_circt_dialect_library(CIRCTSV
   CIRCTComb
   CIRCTHW
   CIRCTSupport
+  CIRCTVerif
   MLIRIR
 )
 

diff --git a/lib/Dialect/SV/Transforms/CMakeLists.txt b/lib/Dialect/SV/Transforms/CMakeLists.txt
@@ -19,6 +19,7 @@ add_circt_dialect_library(CIRCTSVTransforms
   CIRCTSeq
   CIRCTSupport
   CIRCTSV
+  CIRCTVerif
   MLIRIR
   MLIRPass
   MLIRTransformUtils

diff --git a/lib/Dialect/SV/Transforms/PassDetail.h b/lib/Dialect/SV/Transforms/PassDetail.h
@@ -30,6 +30,10 @@ class HWDialect;
 class HWModuleOp;
 } // namespace hw
 
+namespace verif {
+class VerifDialect;
+} // namespace verif
+
 namespace sv {
 
 #define GEN_PASS_CLASSES

diff --git a/lib/Dialect/SV/Transforms/SVExtractTestCode.cpp b/lib/Dialect/SV/Transforms/SVExtractTestCode.cpp
@@ -23,6 +23,7 @@
 #include "circt/Dialect/SV/SVPasses.h"
 #include "circt/Dialect/Seq/SeqDialect.h"
 #include "circt/Dialect/Seq/SeqOps.h"
+#include "circt/Dialect/Verif/VerifOps.h"
 #include "circt/Support/Namespace.h"
 #include "mlir/IR/Builders.h"
 #include "mlir/IR/IRMapping.h"
@@ -552,7 +553,8 @@ static bool isAssertOp(hw::HWSymbolCache &symCache, Operation *op) {
     return false;
   }
 
-  return isa<AssertOp, FinishOp, FWriteOp, AssertConcurrentOp, FatalOp>(op);
+  return isa<AssertOp, FinishOp, FWriteOp, AssertConcurrentOp, FatalOp,
+             verif::AssertOp>(op);
 }
 
 static bool isCoverOp(hw::HWSymbolCache &symCache, Operation *op) {
@@ -562,7 +564,7 @@ static bool isCoverOp(hw::HWSymbolCache &symCache, Operation *op) {
     if (auto *mod = symCache.getDefinition(inst.getModuleNameAttr()))
       if (mod->getAttr("firrtl.extract.cover.extra"))
         return true;
-  return isa<CoverOp, CoverConcurrentOp>(op);
+  return isa<CoverOp, CoverConcurrentOp, verif::CoverOp>(op);
 }
 
 static bool isAssumeOp(hw::HWSymbolCache &symCache, Operation *op) {
@@ -573,7 +575,7 @@ static bool isAssumeOp(hw::HWSymbolCache &symCache, Operation *op) {
       if (mod->getAttr("firrtl.extract.assume.extra"))
         return true;
 
-  return isa<AssumeOp, AssumeConcurrentOp>(op);
+  return isa<AssumeOp, AssumeConcurrentOp, verif::AssumeOp>(op);
 }
 
 /// Return true if the operation belongs to the design.

diff --git a/test/Dialect/SV/hw-extract-test-code.mlir b/test/Dialect/SV/hw-extract-test-code.mlir
@@ -589,3 +589,18 @@ module {
     hw.output %2 : i1
   }
 }
+
+// -----
+
+// Check that verif ops are also extracted.
+
+// CHECK: hw.module private @VerifOps_assert
+// CHECK: hw.module private @VerifOps_assume
+// CHECK: hw.module private @VerifOps_cover
+hw.module @VerifOps(in %a : i1, in %b : i1) {
+  %true = hw.constant true
+  verif.assert %true : i1
+  verif.assume %true : i1
+  verif.cover %true : i1
+  hw.output
+}
diff --git a/test/firtool/extract-test-code.fir b/test/firtool/extract-test-code.fir
@@ -2,11 +2,12 @@
 ; RUN: firtool %s -extract-test-code -etc-disable-instance-extraction | FileCheck %s --check-prefix=DISABLEINSTANCE
 ; RUN: firtool %s -extract-test-code -etc-disable-module-inlining | FileCheck %s --check-prefix=DISABLEMODULE
 
+FIRRTL version 4.0.0
 circuit Top:
   module Foo:
     input a : UInt<1>
     output b : UInt<1>
-    b <= a
+    connect b, a
 
   ; Ensure foo is extracted by default.
   ; CHECK-LABEL: module InstanceExtracted_assert(
@@ -23,12 +24,12 @@ circuit Top:
 
     wire b : UInt<1>
     inst foo of Foo
-    foo.a <= cond
-    b <= foo.b
+    connect foo.a, cond
+    connect b, foo.b
 
     assert(clock, cond, b, "Some assertion")
 
-    out <= cond
+    connect out, cond
 
   ; Ensure InputOnly is inlined by default.
   ; CHECK-NOT: module InputOnly(
@@ -41,17 +42,29 @@ circuit Top:
     input cond : UInt<1>
     assert(clock, cond, cond, "Some assertion")
 
-  module Top:
+  intmodule VerifAssertIntrinsic_foo :
+    input property : UInt<1>
+    intrinsic = circt_verif_assert
+    parameter label = "foo"
+
+  ; CHECK: module Top_assert(
+  ; CHECK-NOT: endmodule
+  ; CHECK:   foo: assert property (cond);
+  ; CHECK: endmodule
+
+  public module Top:
     input clock : Clock
     input cond : UInt<1>
     output out : UInt<1>
 
     inst instance_extracted of InstanceExtracted
-    instance_extracted.clock <= clock
-    instance_extracted.cond <= cond
-    out <= instance_extracted.out
+    connect instance_extracted.clock, clock
+    connect instance_extracted.cond, cond
+    connect out, instance_extracted.out
 
     inst input_only of InputOnly
-    input_only.clock <= clock
-    input_only.cond <= cond
+    connect input_only.clock, clock
+    connect input_only.cond, cond
 
+    inst verif of VerifAssertIntrinsic_foo
+    connect verif.property, cond
-Original file line number
+Diff line change
@@ Expand Up / @@ -17,6 +17,7 @@ add_circt_dialect_library(CIRCTSV @@
       CIRCTComb
       CIRCTHW
       CIRCTSupport
+      CIRCTVerif
       MLIRIR
     )
@@ Expand Down @@