create and extend annotatable BaseSim class for verification nodes (c…

…hipsalliance#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

core/src/main/scala/chisel3/RawModule.scala

@@ -5,8 +5,7 @@ package chisel3
 import scala.collection.mutable.{ArrayBuffer, HashMap}
 import scala.util.Try
 import scala.language.experimental.macros
-
-import chisel3.experimental.BaseModule
+import chisel3.experimental.{BaseModule, BaseSim}
 import chisel3.internal._
 import chisel3.internal.Builder._
 import chisel3.internal.firrtl._
@@ -77,6 +76,7 @@ abstract class RawModule(implicit moduleCompileOptions: CompileOptions)
       id match {
         case id: BaseModule => id.forceName(None, default=id.desiredName, _namespace)
         case id: MemBase[_] => id.forceName(None, default="MEM", _namespace)
+        case id: BaseSim => id.forceName(None, default="SIM", _namespace)
         case id: Data  =>
           if (id.isSynthesizable) {
             id.topBinding match {

core/src/main/scala/chisel3/experimental/package.scala

@@ -2,6 +2,7 @@
 
 package chisel3
 
+import chisel3.internal.NamedComponent
 import chisel3.internal.sourceinfo.SourceInfo
 
 /** Package for experimental features, which may have their API changed, be removed, etc.
@@ -165,4 +166,9 @@ package object experimental {
   val prefix = chisel3.internal.prefix
   // Use to remove prefixes not in provided scope
   val noPrefix = chisel3.internal.noPrefix
+
+  /** Base simulation-only component. */
+  abstract class BaseSim extends NamedComponent {
+    _parent.foreach(_.addId(this))
+  }
 }

core/src/main/scala/chisel3/experimental/verification/package.scala

@@ -8,36 +8,52 @@ import chisel3.internal.firrtl.{Formal, Verification}
 import chisel3.internal.sourceinfo.SourceInfo
 
 package object verification {
+
+  /** Named class for assertions. */
+  final class Assert(val predicate: Bool) extends BaseSim
+
+  /** Named class for assumes. */
+  final class Assume(val predicate: Bool) extends BaseSim
+
+  /** Named class for covers. */
+  final class Cover(val predicate: Bool) extends BaseSim
+
   object assert {
     def apply(predicate: Bool, msg: String = "")(
       implicit sourceInfo: SourceInfo,
-      compileOptions: CompileOptions): Unit = {
+      compileOptions: CompileOptions): Assert = {
+      val a = new Assert(predicate)
       when (!Module.reset.asBool) {
         val clock = Module.clock
-        Builder.pushCommand(Verification(Formal.Assert, sourceInfo, clock.ref, predicate.ref, msg))
+        Builder.pushCommand(Verification(a, Formal.Assert, sourceInfo, clock.ref, predicate.ref, msg))
       }
+      a
     }
   }
 
   object assume {
     def apply(predicate: Bool, msg: String = "")(
       implicit sourceInfo: SourceInfo,
-      compileOptions: CompileOptions): Unit = {
+      compileOptions: CompileOptions): Assume = {
+      val a = new Assume(predicate)
       when (!Module.reset.asBool) {
         val clock = Module.clock
-        Builder.pushCommand(Verification(Formal.Assume, sourceInfo, clock.ref, predicate.ref, msg))
+        Builder.pushCommand(Verification(a, Formal.Assume, sourceInfo, clock.ref, predicate.ref, msg))
       }
+      a
     }
   }
 
   object cover {
     def apply(predicate: Bool, msg: String = "")(
       implicit sourceInfo: SourceInfo,
-      compileOptions: CompileOptions): Unit = {
+      compileOptions: CompileOptions): Cover = {
       val clock = Module.clock
+      val c = new Cover(predicate)
       when (!Module.reset.asBool) {
-        Builder.pushCommand(Verification(Formal.Cover, sourceInfo, clock.ref, predicate.ref, msg))
+        Builder.pushCommand(Verification(c, Formal.Cover, sourceInfo, clock.ref, predicate.ref, msg))
       }
+      c
     }
   }
 }

core/src/main/scala/chisel3/internal/firrtl/Converter.scala

@@ -136,14 +136,14 @@ private[chisel3] object Converter {
       val (fmt, args) = unpack(pable, ctx)
       Some(fir.Print(convert(info), fir.StringLit(fmt),
                      args.map(a => convert(a, ctx, info)), convert(clock, ctx, info), firrtl.Utils.one))
-    case Verification(op, info, clk, pred, msg) =>
+    case e @ Verification(_, op, info, clk, pred, msg) =>
       val firOp = op match {
         case Formal.Assert => fir.Formal.Assert
         case Formal.Assume => fir.Formal.Assume
         case Formal.Cover => fir.Formal.Cover
       }
       Some(fir.Verification(firOp, convert(info), convert(clk, ctx, info),
-        convert(pred, ctx, info), firrtl.Utils.one, fir.StringLit(msg)))
+        convert(pred, ctx, info), firrtl.Utils.one, fir.StringLit(msg), e.name))
     case _ => None
   }
 

core/src/main/scala/chisel3/internal/firrtl/IR.scala

@@ -3,7 +3,6 @@
 package chisel3.internal.firrtl
 
 import firrtl.{ir => fir}
-
 import chisel3._
 import chisel3.internal._
 import chisel3.internal.sourceinfo.SourceInfo
@@ -765,8 +764,8 @@ object Formal extends Enumeration {
   val Assume = Value("assume")
   val Cover = Value("cover")
 }
-case class Verification(op: Formal.Value, sourceInfo: SourceInfo, clock: Arg,
-                        predicate: Arg, message: String) extends Command
+case class Verification[T <: BaseSim](id: T, op: Formal.Value, sourceInfo: SourceInfo, clock: Arg,
+                        predicate: Arg, message: String) extends Definition
 abstract class Component extends Arg {
   def id: BaseModule
   def name: String

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 =>

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")
   }
 }