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--- .../scala/chisel3/internal/firrtl/Emitter.scala | 4 +- .../verification/VerificationSpec.scala | 134 +++++++++++++++++++-- 2 files changed, 124 insertions(+), 14 deletions(-) (limited to 'src') diff --git a/src/main/scala/chisel3/internal/firrtl/Emitter.scala b/src/main/scala/chisel3/internal/firrtl/Emitter.scala index ad4df80a..53d5c6ce 100644 --- a/src/main/scala/chisel3/internal/firrtl/Emitter.scala +++ b/src/main/scala/chisel3/internal/firrtl/Emitter.scala @@ -80,8 +80,8 @@ private class Emitter(circuit: Circuit) { val printfArgs = Seq(e.clock.fullName(ctx), "UInt<1>(1)", "\"" + printf.format(fmt) + "\"") ++ args printfArgs mkString ("printf(", ", ", ")") - case e: Verification => s"${e.op}(${e.clock.fullName(ctx)}, ${e.predicate.fullName(ctx)}, " + - s"UInt<1>(1), " + "\"" + s"${printf.format(e.message)}" + "\")" + case e: Verification[_] => + s"""${e.op}(${e.clock.fullName(ctx)}, ${e.predicate.fullName(ctx)}, UInt<1>(1), "${printf.format(e.message)}") : ${e.name}""" case e: DefInvalid => s"${e.arg.fullName(ctx)} is invalid" case e: DefInstance => s"inst ${e.name} of ${e.id.name}" case w: WhenBegin => 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