summaryrefslogtreecommitdiff
path: root/src/test/scala/chiselTests/VerificationSpec.scala
diff options
context:
space:
mode:
authorAditya Naik2023-11-23 03:11:56 -0800
committerAditya Naik2023-11-23 03:11:56 -0800
commitaf415532cf160e63e971ceb301833b8433c18a50 (patch)
tree1fef70139846f57298c8e24a590490a74249f7dd /src/test/scala/chiselTests/VerificationSpec.scala
parent8200c0cdf1d471453946d5ae24bc99757b2ef02d (diff)
cleanup
Diffstat (limited to 'src/test/scala/chiselTests/VerificationSpec.scala')
-rw-r--r--src/test/scala/chiselTests/VerificationSpec.scala156
1 files changed, 0 insertions, 156 deletions
diff --git a/src/test/scala/chiselTests/VerificationSpec.scala b/src/test/scala/chiselTests/VerificationSpec.scala
deleted file mode 100644
index 32cee9e3..00000000
--- a/src/test/scala/chiselTests/VerificationSpec.scala
+++ /dev/null
@@ -1,156 +0,0 @@
-// SPDX-License-Identifier: Apache-2.0
-
-package chiselTests
-
-import chisel3._
-import chisel3.experimental.{ChiselAnnotation, verification => formal}
-import chisel3.stage.ChiselStage
-import firrtl.annotations.{ReferenceTarget, SingleTargetAnnotation}
-import org.scalatest.matchers.should.Matchers
-
-import java.io.File
-
-class SimpleTest extends Module {
- val io = IO(new Bundle {
- val in = Input(UInt(8.W))
- val out = Output(UInt(8.W))
- })
- io.out := io.in
- cover(io.in === 3.U)
- when(io.in === 3.U) {
- assume(io.in =/= 2.U)
- assert(io.out === io.in)
- }
-}
-
-/** Dummy verification annotation.
- * @param target target of component to be annotated
- */
-case class VerifAnnotation(target: ReferenceTarget) extends SingleTargetAnnotation[ReferenceTarget] {
- def duplicate(n: ReferenceTarget): VerifAnnotation = this.copy(target = n)
-}
-
-object VerifAnnotation {
-
- /** Create annotation for a given verification component.
- * @param c component to be annotated
- */
- def annotate(c: VerificationStatement): Unit = {
- chisel3.experimental.annotate(new ChiselAnnotation {
- def toFirrtl: VerifAnnotation = VerifAnnotation(c.toTarget)
- })
- }
-}
-
-class VerificationSpec extends ChiselPropSpec with Matchers {
-
- def assertContains(s: Seq[String], x: String): Unit = {
- val containsLine = s.map(_.contains(x)).reduce(_ || _)
- assert(containsLine, s"\n $x\nwas not found in`\n ${s.mkString("\n ")}``")
- }
-
- property("basic equality check should work") {
- val fir = ChiselStage.emitChirrtl(new SimpleTest)
- val lines = fir.split("\n").map(_.trim)
-
- // reset guard around the verification statement
- assertContains(lines, "when _T_2 : @[VerificationSpec.scala")
- assertContains(lines, "cover(clock, _T, UInt<1>(\"h1\"), \"\")")
-
- assertContains(lines, "when _T_6 : @[VerificationSpec.scala")
- assertContains(lines, "assume(clock, _T_4, 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") {
-
- /** Circuit that contains and annotates verification nodes. */
- class AnnotationTest extends Module {
- val io = IO(new Bundle {
- val in = Input(UInt(8.W))
- val out = Output(UInt(8.W))
- })
- 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)
- }
-
- // compile circuit
- val testDir = new File("test_run_dir", "VerificationAnnotationTests")
- (new ChiselStage).emitSystemVerilog(
- gen = new AnnotationTest,
- args = Array("-td", testDir.getPath)
- )
-
- // read in annotation file
- val annoFile = new File(testDir, "AnnotationTest.anno.json")
- annoFile should exist
- val annoLines = scala.io.Source.fromFile(annoFile).getLines.toList
-
- // check for expected verification annotations
- 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")
-
- // read in FIRRTL file
- val firFile = new File(testDir, "AnnotationTest.fir")
- firFile should exist
- val firLines = scala.io.Source.fromFile(firFile).getLines.toList
-
- // check that verification components have expected names
- (exactly(1, firLines) should include).regex("^\\s*cover\\(.*\\) : cov")
- (exactly(1, firLines) should include).regex("^\\s*assume\\(.*\\) : assm")
- (exactly(1, firLines) should include).regex("^\\s*assert\\(.*\\) : asst")
- }
-
- property("annotation of verification constructs with suggested name should work") {
-
- /** Circuit that annotates a renamed verification nodes. */
- class AnnotationRenameTest extends Module {
- val io = IO(new Bundle {
- val in = Input(UInt(8.W))
- val out = Output(UInt(8.W))
- })
- io.out := io.in
-
- val goodbye = chisel3.assert(io.in === 1.U)
- goodbye.suggestName("hello")
- VerifAnnotation.annotate(goodbye)
-
- VerifAnnotation.annotate(chisel3.assume(io.in =/= 2.U).suggestName("howdy"))
- }
-
- // compile circuit
- val testDir = new File("test_run_dir", "VerificationAnnotationRenameTests")
- (new ChiselStage).emitSystemVerilog(
- gen = new AnnotationRenameTest,
- args = Array("-td", testDir.getPath)
- )
-
- // read in annotation file
- val annoFile = new File(testDir, "AnnotationRenameTest.anno.json")
- annoFile should exist
- val annoLines = scala.io.Source.fromFile(annoFile).getLines.toList
-
- // check for expected verification annotations
- exactly(2, annoLines) should include("chiselTests.VerifAnnotation")
- exactly(1, annoLines) should include("~AnnotationRenameTest|AnnotationRenameTest>hello")
- exactly(1, annoLines) should include("~AnnotationRenameTest|AnnotationRenameTest>howdy")
-
- // read in FIRRTL file
- val firFile = new File(testDir, "AnnotationRenameTest.fir")
- firFile should exist
- val firLines = scala.io.Source.fromFile(firFile).getLines.toList
-
- // check that verification components have expected names
- (exactly(1, firLines) should include).regex("^\\s*assert\\(.*\\) : hello")
- (exactly(1, firLines) should include).regex("^\\s*assume\\(.*\\) : howdy")
- }
-}