From 492a71d6d4d3acef39f29345835637bca028a089 Mon Sep 17 00:00:00 2001 From: Schuyler Eldridge Date: Wed, 17 Mar 2021 14:00:27 -0400 Subject: Fix incorrect usage of emitFirrtl in test (#1817) Change a test to use emitChirrtl instead of emitFirrtl. This test isn't supposed to be running the Scala FIRRTL Compiler, but the latter method causes this to happen. Signed-off-by: Schuyler Eldridge --- .../scala/chiselTests/experimental/verification/VerificationSpec.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/test/scala/chiselTests/experimental/verification') diff --git a/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala b/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala index 52293abb..fe642156 100644 --- a/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala +++ b/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala @@ -28,7 +28,7 @@ class VerificationSpec extends ChiselPropSpec { } property("basic equality check should work") { - val fir = ChiselStage.emitFirrtl(new VerificationModule) + val fir = ChiselStage.emitChirrtl(new VerificationModule) val lines = fir.split("\n").map(_.trim) assertContains(lines, "cover(clock, _T, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 16:15]") assertContains(lines, "assume(clock, _T_2, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 18:18]") -- cgit v1.2.3 From 4d8fed00225d15221cf32177ea9147b20d0b91f7 Mon Sep 17 00:00:00 2001 From: Kevin Laeufer Date: Thu, 29 Apr 2021 11:52:20 -0700 Subject: verification: guard statements with module reset (#1891) --- .../experimental/verification/VerificationSpec.scala | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'src/test/scala/chiselTests/experimental/verification') diff --git a/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala b/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala index fe642156..86d6418c 100644 --- a/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala +++ b/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala @@ -30,8 +30,15 @@ class VerificationSpec extends ChiselPropSpec { property("basic equality check should work") { val fir = ChiselStage.emitChirrtl(new VerificationModule) val lines = fir.split("\n").map(_.trim) + + // reset guard around the verification statement + assertContains(lines, "when _T_2 : @[VerificationSpec.scala 16:15]") assertContains(lines, "cover(clock, _T, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 16:15]") - assertContains(lines, "assume(clock, _T_2, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 18:18]") - assertContains(lines, "assert(clock, _T_3, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 19:18]") + + assertContains(lines, "when _T_6 : @[VerificationSpec.scala 18:18]") + assertContains(lines, "assume(clock, _T_4, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 18:18]") + + assertContains(lines, "when _T_9 : @[VerificationSpec.scala 19:18]") + assertContains(lines, "assert(clock, _T_7, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 19:18]") } } -- cgit v1.2.3 From f8053db3d20b733e0119b77595f0cdfcdab71057 Mon Sep 17 00:00:00 2001 From: Deborah Soung Date: Thu, 24 Jun 2021 14:03:28 -0700 Subject: create and extend annotatable BaseSim class for verification nodes (#1968) * prototype annotating verif constructs * switch to final class * name emissions * moving BaseSim to experimental * adding name tests * fixing quotation escapes * emitting names, but everything has a default name * only name things with provided/suggested names * name every BaseSim node * removing msg, unused imports * fixing file exist calls--- .../verification/VerificationSpec.scala | 134 +++++++++++++++++++-- 1 file changed, 122 insertions(+), 12 deletions(-) (limited to 'src/test/scala/chiselTests/experimental/verification') diff --git a/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala b/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala index 86d6418c..a1fc2a1d 100644 --- a/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala +++ b/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala @@ -3,11 +3,15 @@ package chiselTests.experimental.verification import chisel3._ -import chisel3.experimental.{verification => formal} +import chisel3.experimental.{ChiselAnnotation, verification => formal} import chisel3.stage.ChiselStage import chiselTests.ChiselPropSpec +import firrtl.annotations.{ReferenceTarget, SingleTargetAnnotation} -class VerificationModule extends Module { +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)) @@ -20,25 +24,131 @@ class VerificationModule extends Module { } } -class VerificationSpec extends ChiselPropSpec { +/** 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[T](s: Seq[T], x: T): Unit = { - val containsLine = s.map(_ == x).reduce(_ || _) + 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 VerificationModule) + 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 16:15]") - assertContains(lines, "cover(clock, _T, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 16:15]") + 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>(1), \"\") : cov") + exactly(1, firLines) should include ("assume(clock, _T_3, UInt<1>(1), \"\") : assm") + exactly(1, firLines) should include ("assert(clock, _T_6, UInt<1>(1), \"\") : 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") - assertContains(lines, "when _T_6 : @[VerificationSpec.scala 18:18]") - assertContains(lines, "assume(clock, _T_4, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 18:18]") + // read in FIRRTL file + val firFile = new File(testDir, "AnnotationRenameTest.fir") + firFile should exist + val firLines = scala.io.Source.fromFile(firFile).getLines.toList - assertContains(lines, "when _T_9 : @[VerificationSpec.scala 19:18]") - assertContains(lines, "assert(clock, _T_7, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 19:18]") + // check that verification components have expected names + exactly(1, firLines) should include ("assert(clock, _T, UInt<1>(1), \"\") : hello") + exactly(1, firLines) should include ("assume(clock, _T_3, UInt<1>(1), \"\") : howdy") } } -- cgit v1.2.3 From 73bd4ee6b9b510725b692c33e075362a19512d2c Mon Sep 17 00:00:00 2001 From: Jack Koenig Date: Fri, 20 Aug 2021 11:30:27 -0700 Subject: Remove chisel3's own firrtl Emitter, use firrtl Serializer This will be slightly slower as it involves converting from Chisel modules to FIRRTL modules before turning them into Strings. This cost is somewhat mitigated by doing that conversion lazily such that we never materialize the entire firrtl Circuit in memory, only 1 module at a time. --- .../experimental/verification/VerificationSpec.scala | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src/test/scala/chiselTests/experimental/verification') diff --git a/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala b/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala index a1fc2a1d..1e080739 100644 --- a/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala +++ b/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala @@ -104,9 +104,9 @@ class VerificationSpec extends ChiselPropSpec with Matchers { 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>(1), \"\") : cov") - exactly(1, firLines) should include ("assume(clock, _T_3, UInt<1>(1), \"\") : assm") - exactly(1, firLines) should include ("assert(clock, _T_6, UInt<1>(1), \"\") : asst") + 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") { @@ -148,7 +148,7 @@ class VerificationSpec extends ChiselPropSpec with Matchers { 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>(1), \"\") : hello") - exactly(1, firLines) should include ("assume(clock, _T_3, UInt<1>(1), \"\") : howdy") + 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