make all verification statements publically available (#2089)

3 files changed, 24 insertions, 26 deletions

diff --git a/src/test/scala/chiselTests/PrintableSpec.scala b/src/test/scala/chiselTests/PrintableSpec.scala
index 25b54966..95103352 100644
--- a/src/test/scala/chiselTests/PrintableSpec.scala
+++ b/src/test/scala/chiselTests/PrintableSpec.scala
@@ -3,7 +3,7 @@
 package chiselTests
 
 import chisel3._
-import chisel3.experimental.{BaseSim, ChiselAnnotation}
+import chisel3.experimental.ChiselAnnotation
 import chisel3.stage.ChiselStage
 import chisel3.testers.BasicTester
 import firrtl.annotations.{ReferenceTarget, SingleTargetAnnotation}
@@ -23,7 +23,7 @@ object PrintfAnnotation {
   /** Create annotation for a given [[printf]].
     * @param c component to be annotated
     */
-  def annotate(c: BaseSim): Unit = {
+  def annotate(c: VerificationStatement): Unit = {
     chisel3.experimental.annotate(new ChiselAnnotation {
       def toFirrtl: PrintfAnnotation = PrintfAnnotation(c.toTarget)
     })
@@ -246,7 +246,7 @@ class PrintableSpec extends AnyFlatSpec with Matchers {
     // check for expected annotations
     exactly(3, annoLines) should include ("chiselTests.PrintfAnnotation")
     exactly(1, annoLines) should include ("~PrintfAnnotationTest|PrintfAnnotationTest>farewell")
-    exactly(1, annoLines) should include ("~PrintfAnnotationTest|PrintfAnnotationTest>SIM")
+    exactly(1, annoLines) should include ("~PrintfAnnotationTest|PrintfAnnotationTest>printf")
     exactly(1, annoLines) should include ("~PrintfAnnotationTest|PrintfAnnotationTest>howdy")
 
     // read in FIRRTL file
@@ -256,7 +256,7 @@ class PrintableSpec extends AnyFlatSpec with Matchers {
 
     // check that verification components have expected names
     exactly(1, firLines) should include ("""printf(clock, UInt<1>("h1"), "hello AnonymousBundle(foo -> %d, bar -> %d)", myBun.foo, myBun.bar) : howdy""")
-    exactly(1, firLines) should include ("""printf(clock, UInt<1>("h1"), "goodbye AnonymousBundle(foo -> %d, bar -> %d)", myBun.foo, myBun.bar) : SIM""")
+    exactly(1, firLines) should include ("""printf(clock, UInt<1>("h1"), "goodbye AnonymousBundle(foo -> %d, bar -> %d)", myBun.foo, myBun.bar) : printf""")
     exactly(1, firLines) should include ("""printf(clock, UInt<1>("h1"), "adieu AnonymousBundle(foo -> %d, bar -> %d)", myBun.foo, myBun.bar) : farewell""")
   }
 }
diff --git a/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala b/src/test/scala/chiselTests/VerificationSpec.scala
index 1e080739..2d7144df 100644
--- a/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala
+++ b/src/test/scala/chiselTests/VerificationSpec.scala
@@ -1,15 +1,14 @@
 // SPDX-License-Identifier: Apache-2.0
 
-package chiselTests.experimental.verification
+package chiselTests
 
 import chisel3._
 import chisel3.experimental.{ChiselAnnotation, verification => formal}
 import chisel3.stage.ChiselStage
-import chiselTests.ChiselPropSpec
 import firrtl.annotations.{ReferenceTarget, SingleTargetAnnotation}
+import org.scalatest.matchers.should.Matchers
 
 import java.io.File
-import org.scalatest.matchers.should.Matchers
 
 class SimpleTest extends Module {
   val io = IO(new Bundle{
@@ -17,10 +16,10 @@ class SimpleTest extends Module {
     val out = Output(UInt(8.W))
   })
   io.out := io.in
-  formal.cover(io.in === 3.U)
+  cover(io.in === 3.U)
   when (io.in === 3.U) {
-    formal.assume(io.in =/= 2.U)
-    formal.assert(io.out === io.in)
+    assume(io.in =/= 2.U)
+    assert(io.out === io.in)
   }
 }
 
@@ -35,7 +34,7 @@ object VerifAnnotation {
   /** Create annotation for a given verification component.
     * @param c component to be annotated
     */
-  def annotate(c: experimental.BaseSim): Unit = {
+  def annotate(c: VerificationStatement): Unit = {
     chisel3.experimental.annotate(new ChiselAnnotation {
       def toFirrtl: VerifAnnotation = VerifAnnotation(c.toTarget)
     })
@@ -60,8 +59,8 @@ class VerificationSpec extends ChiselPropSpec with Matchers {
     assertContains(lines, "when _T_6 : @[VerificationSpec.scala")
     assertContains(lines, "assume(clock, _T_4, UInt<1>(\"h1\"), \"\")")
 
-    assertContains(lines, "when _T_9 : @[VerificationSpec.scala")
-    assertContains(lines, "assert(clock, _T_7, UInt<1>(\"h1\"), \"\")")
+    assertContains(lines, "when _T_10 : @[VerificationSpec.scala")
+    assertContains(lines, "assert(clock, _T_8, UInt<1>(\"h1\"), \"\")")
   }
 
   property("annotation of verification constructs should work") {
@@ -72,9 +71,9 @@ class VerificationSpec extends ChiselPropSpec with Matchers {
         val out = Output(UInt(8.W))
       })
       io.out := io.in
-      val cov = formal.cover(io.in === 3.U)
-      val assm = formal.assume(io.in =/= 2.U)
-      val asst = formal.assert(io.out === io.in)
+      val cov = cover(io.in === 3.U)
+      val assm = chisel3.assume(io.in =/= 2.U)
+      val asst = chisel3.assert(io.out === io.in)
       VerifAnnotation.annotate(cov)
       VerifAnnotation.annotate(assm)
       VerifAnnotation.annotate(asst)
@@ -93,7 +92,7 @@ class VerificationSpec extends ChiselPropSpec with Matchers {
     val annoLines = scala.io.Source.fromFile(annoFile).getLines.toList
 
     // check for expected verification annotations
-    exactly(3, annoLines) should include ("chiselTests.experimental.verification.VerifAnnotation")
+    exactly(3, annoLines) should include ("chiselTests.VerifAnnotation")
     exactly(1, annoLines) should include ("~AnnotationTest|AnnotationTest>asst")
     exactly(1, annoLines) should include ("~AnnotationTest|AnnotationTest>assm")
     exactly(1, annoLines) should include ("~AnnotationTest|AnnotationTest>cov")
@@ -106,7 +105,7 @@ class VerificationSpec extends ChiselPropSpec with Matchers {
     // check that verification components have expected names
     exactly(1, firLines) should include ("cover(clock, _T, UInt<1>(\"h1\"), \"\") : cov")
     exactly(1, firLines) should include ("assume(clock, _T_3, UInt<1>(\"h1\"), \"\") : assm")
-    exactly(1, firLines) should include ("assert(clock, _T_6, UInt<1>(\"h1\"), \"\") : asst")
+    exactly(1, firLines) should include ("assert(clock, _T_7, UInt<1>(\"h1\"), \"\") : asst")
   }
 
   property("annotation of verification constructs with suggested name should work") {
@@ -118,11 +117,11 @@ class VerificationSpec extends ChiselPropSpec with Matchers {
       })
       io.out := io.in
 
-      val goodbye = formal.assert(io.in === 1.U)
+      val goodbye = chisel3.assert(io.in === 1.U)
       goodbye.suggestName("hello")
       VerifAnnotation.annotate(goodbye)
 
-      VerifAnnotation.annotate(formal.assume(io.in =/= 2.U).suggestName("howdy"))
+      VerifAnnotation.annotate(chisel3.assume(io.in =/= 2.U).suggestName("howdy"))
     }
 
     // compile circuit
@@ -138,7 +137,7 @@ class VerificationSpec extends ChiselPropSpec with Matchers {
     val annoLines = scala.io.Source.fromFile(annoFile).getLines.toList
 
     // check for expected verification annotations
-    exactly(2, annoLines) should include ("chiselTests.experimental.verification.VerifAnnotation")
+    exactly(2, annoLines) should include ("chiselTests.VerifAnnotation")
     exactly(1, annoLines) should include ("~AnnotationRenameTest|AnnotationRenameTest>hello")
     exactly(1, annoLines) should include ("~AnnotationRenameTest|AnnotationRenameTest>howdy")
 
@@ -149,6 +148,6 @@ class VerificationSpec extends ChiselPropSpec with Matchers {
 
     // check that verification components have expected names
     exactly(1, firLines) should include ("assert(clock, _T, UInt<1>(\"h1\"), \"\") : hello")
-    exactly(1, firLines) should include ("assume(clock, _T_3, UInt<1>(\"h1\"), \"\") : howdy")
+    exactly(1, firLines) should include ("assume(clock, _T_4, UInt<1>(\"h1\"), \"\") : howdy")
   }
 }
diff --git a/src/test/scala/chiselTests/aop/SelectSpec.scala b/src/test/scala/chiselTests/aop/SelectSpec.scala
index e09e78c8..2b47c6b8 100644
--- a/src/test/scala/chiselTests/aop/SelectSpec.scala
+++ b/src/test/scala/chiselTests/aop/SelectSpec.scala
@@ -133,11 +133,10 @@ class SelectSpec extends ChiselFlatSpec {
       { dut: SelectTester =>
         Seq(Select.Stop(
           Seq(
-            When(Select.ops("eq")(dut).dropRight(1).last.asInstanceOf[Bool]),
-            When(dut.nreset),
-            WhenNot(dut.overflow)
+            When(Select.ops("eq")(dut)(1).asInstanceOf[Bool]),
+            When(dut.overflow)
           ),
-          1,
+          0,
           dut.clock
         ))
       }