From d1d38bd096fce8b92468720fbedc835ecda40e6b Mon Sep 17 00:00:00 2001 From: Kevin Laeufer Date: Thu, 23 Sep 2021 11:12:26 -0700 Subject: make all verification statements publically available (#2089) --- src/test/scala/chiselTests/PrintableSpec.scala | 8 +- src/test/scala/chiselTests/VerificationSpec.scala | 153 ++++++++++++++++++++ src/test/scala/chiselTests/aop/SelectSpec.scala | 7 +- .../verification/VerificationSpec.scala | 154 --------------------- 4 files changed, 160 insertions(+), 162 deletions(-) create mode 100644 src/test/scala/chiselTests/VerificationSpec.scala delete mode 100644 src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala (limited to 'src/test') 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/VerificationSpec.scala b/src/test/scala/chiselTests/VerificationSpec.scala new file mode 100644 index 00000000..2d7144df --- /dev/null +++ b/src/test/scala/chiselTests/VerificationSpec.scala @@ -0,0 +1,153 @@ +// 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 ("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_7, UInt<1>(\"h1\"), \"\") : 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 ("assert(clock, _T, UInt<1>(\"h1\"), \"\") : hello") + 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 )) } diff --git a/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala b/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala deleted file mode 100644 index 1e080739..00000000 --- a/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala +++ /dev/null @@ -1,154 +0,0 @@ -// SPDX-License-Identifier: Apache-2.0 - -package chiselTests.experimental.verification - -import chisel3._ -import chisel3.experimental.{ChiselAnnotation, verification => formal} -import chisel3.stage.ChiselStage -import chiselTests.ChiselPropSpec -import firrtl.annotations.{ReferenceTarget, SingleTargetAnnotation} - -import java.io.File -import org.scalatest.matchers.should.Matchers - -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 - formal.cover(io.in === 3.U) - when (io.in === 3.U) { - formal.assume(io.in =/= 2.U) - formal.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: experimental.BaseSim): 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_9 : @[VerificationSpec.scala") - assertContains(lines, "assert(clock, _T_7, 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 = formal.cover(io.in === 3.U) - val assm = formal.assume(io.in =/= 2.U) - val asst = formal.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.experimental.verification.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 ("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") - } - - 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 = formal.assert(io.in === 1.U) - goodbye.suggestName("hello") - VerifAnnotation.annotate(goodbye) - - VerifAnnotation.annotate(formal.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.experimental.verification.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 ("assert(clock, _T, UInt<1>(\"h1\"), \"\") : hello") - exactly(1, firLines) should include ("assume(clock, _T_3, UInt<1>(\"h1\"), \"\") : howdy") - } -} -- cgit v1.2.3