@@ -21,7 +21,7 @@ class SimpleTest extends Module {
21
21
}
22
22
}
23
23
24
- class VerificationSpec extends ChiselPropSpec with Matchers {
24
+ class VerificationSpec extends ChiselPropSpec with FileCheck with Matchers {
25
25
26
26
def assertContains (s : Seq [String ], x : String ): Unit = {
27
27
val containsLine = s.map(_.contains(x)).reduce(_ || _)
@@ -74,4 +74,32 @@ class VerificationSpec extends ChiselPropSpec with Matchers {
74
74
exactly(1 , svLines) should include(" assume(io_in != 8'h2)" )
75
75
exactly(1 , svLines) should include(" $error(\" Assumption failed" )
76
76
}
77
+
78
+ property(" verification statements should check that Disable toggles" ) {
79
+ class DisableChecksTest extends Module {
80
+ val io = IO (new Bundle {
81
+ val in = Input (UInt (8 .W ))
82
+ val out = Output (UInt (8 .W ))
83
+ })
84
+ io.out := io.in
85
+ val assert = chisel3.assert(io.out === io.in)
86
+ printf(cf " io: ${io.in}" )
87
+ }
88
+
89
+ val fir = ChiselStage .emitCHIRRTL(
90
+ new DisableChecksTest ,
91
+ args = Array (" --emit-verif-statement-disable-properties" )
92
+ )
93
+ fileCheckString(fir)(
94
+ """
95
+ CHECK: node assert_disable =
96
+ CHECK: node [[NOT_DISABLE:[a-zA-Z0-9_]+]] = eq(assert_disable, UInt<1>(0h0))
97
+ CHECK: node assert_ltl_eventually = intrinsic(circt_ltl_eventually : UInt<1>, [[NOT_DISABLE]])
98
+
99
+ CHECK: node disable =
100
+ CHECK: node [[NOT_DISABLE_1:[a-zA-Z0-9_]+]] = eq(disable, UInt<1>(0h0))
101
+ CHECK: node ltl_eventually = intrinsic(circt_ltl_eventually : UInt<1>, [[NOT_DISABLE_1]])
102
+ """
103
+ )
104
+ }
77
105
}
0 commit comments