summaryrefslogtreecommitdiff
path: root/core
diff options
context:
space:
mode:
Diffstat (limited to 'core')
-rw-r--r--core/src/main/scala/chisel3/Assert.scala92
-rw-r--r--core/src/main/scala/chisel3/Printf.scala3
-rw-r--r--core/src/main/scala/chisel3/RawModule.scala8
-rw-r--r--core/src/main/scala/chisel3/VerificationStatement.scala236
-rw-r--r--core/src/main/scala/chisel3/experimental/package.scala5
-rw-r--r--core/src/main/scala/chisel3/experimental/verification/package.scala60
-rw-r--r--core/src/main/scala/chisel3/internal/firrtl/Converter.scala4
-rw-r--r--core/src/main/scala/chisel3/internal/firrtl/IR.scala4
8 files changed, 247 insertions, 165 deletions
diff --git a/core/src/main/scala/chisel3/Assert.scala b/core/src/main/scala/chisel3/Assert.scala
deleted file mode 100644
index 9a497e1f..00000000
--- a/core/src/main/scala/chisel3/Assert.scala
+++ /dev/null
@@ -1,92 +0,0 @@
-// SPDX-License-Identifier: Apache-2.0
-
-package chisel3
-
-import scala.reflect.macros.blackbox.Context
-import scala.language.experimental.macros
-
-import chisel3.internal._
-import chisel3.internal.Builder.pushCommand
-import chisel3.internal.firrtl._
-import chisel3.internal.sourceinfo.SourceInfo
-
-object assert {
- /** Checks for a condition to be valid in the circuit at all times. If the
- * condition evaluates to false, the circuit simulation stops with an error.
- *
- * Does not fire when in reset (defined as the encapsulating Module's
- * reset). If your definition of reset is not the encapsulating Module's
- * reset, you will need to gate this externally.
- *
- * May be called outside of a Module (like defined in a function), so
- * functions using assert make the standard Module assumptions (single clock
- * and single reset).
- *
- * @param cond condition, assertion fires (simulation fails) when false
- * @param message optional format string to print when the assertion fires
- * @param data optional bits to print in the message formatting
- *
- * @note See [[printf.apply(fmt:String* printf]] for format string documentation
- * @note currently cannot be used in core Chisel / libraries because macro
- * defs need to be compiled first and the SBT project is not set up to do
- * that
- */
- // Macros currently can't take default arguments, so we need two functions to emulate defaults.
- def apply(cond: Bool, message: String, data: Bits*)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Unit = macro apply_impl_msg_data
- def apply(cond: Bool)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Unit = macro apply_impl
-
- def apply_impl_msg_data(c: Context)(cond: c.Tree, message: c.Tree, data: c.Tree*)(sourceInfo: c.Tree, compileOptions: c.Tree): c.Tree = {
- import c.universe._
- val p = c.enclosingPosition
- val condStr = s"${p.source.file.name}:${p.line} ${p.lineContent.trim}"
- val apply_impl_do = symbolOf[this.type].asClass.module.info.member(TermName("apply_impl_do"))
- q"$apply_impl_do($cond, $condStr, _root_.scala.Some($message), ..$data)($sourceInfo, $compileOptions)"
- }
-
- def apply_impl(c: Context)(cond: c.Tree)(sourceInfo: c.Tree, compileOptions: c.Tree): c.Tree = {
- import c.universe._
- val p = c.enclosingPosition
- val condStr = s"${p.source.file.name}:${p.line} ${p.lineContent.trim}"
- val apply_impl_do = symbolOf[this.type].asClass.module.info.member(TermName("apply_impl_do"))
- q"$apply_impl_do($cond, $condStr, _root_.scala.None)($sourceInfo, $compileOptions)"
- }
-
- def apply_impl_do(cond: Bool, line: String, message: Option[String], data: Bits*)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions) {
- val escLine = line.replaceAll("%", "%%")
- when (!(cond || Module.reset.asBool)) {
- val fmt = message match {
- case Some(msg) =>
- s"Assertion failed: $msg\n at $escLine\n"
- case None => s"Assertion failed\n at $escLine\n"
- }
- printf.printfWithoutReset(fmt, data:_*)
- pushCommand(Stop(sourceInfo, Builder.forcedClock.ref, 1))
- }
- }
-
- /** An elaboration-time assertion, otherwise the same as the above run-time
- * assertion. */
- def apply(cond: Boolean, message: => String) {
- Predef.assert(cond, message)
- }
-
- /** A workaround for default-value overloading problems in Scala, just
- * 'assert(cond, "")' */
- def apply(cond: Boolean) {
- Predef.assert(cond, "")
- }
-}
-
-object stop {
- /** Terminate execution with a failure code. */
- def apply(code: Int)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Unit = {
- when (!Module.reset.asBool) {
- pushCommand(Stop(sourceInfo, Builder.forcedClock.ref, code))
- }
- }
-
- /** Terminate execution, indicating success. */
- def apply()(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Unit = {
- stop(0)
- }
-}
diff --git a/core/src/main/scala/chisel3/Printf.scala b/core/src/main/scala/chisel3/Printf.scala
index cf7821b8..be0146bb 100644
--- a/core/src/main/scala/chisel3/Printf.scala
+++ b/core/src/main/scala/chisel3/Printf.scala
@@ -6,7 +6,6 @@ import scala.language.experimental.macros
import chisel3.internal._
import chisel3.internal.Builder.pushCommand
import chisel3.internal.sourceinfo.SourceInfo
-import chisel3.experimental.BaseSim
/** Prints a message in simulation
*
@@ -34,7 +33,7 @@ object printf {
}
/** Named class for [[printf]]s. */
- final class Printf(val pable: Printable) extends BaseSim
+ final class Printf private[chisel3](val pable: Printable) extends VerificationStatement
/** Prints a message in simulation
*
diff --git a/core/src/main/scala/chisel3/RawModule.scala b/core/src/main/scala/chisel3/RawModule.scala
index 27f16ad4..f1b4c1cf 100644
--- a/core/src/main/scala/chisel3/RawModule.scala
+++ b/core/src/main/scala/chisel3/RawModule.scala
@@ -5,7 +5,7 @@ package chisel3
import scala.collection.mutable.{ArrayBuffer, HashMap}
import scala.util.Try
import scala.language.experimental.macros
-import chisel3.experimental.{BaseModule, BaseSim}
+import chisel3.experimental.BaseModule
import chisel3.internal._
import chisel3.internal.BaseModule.{ModuleClone, InstanceClone}
import chisel3.internal.Builder._
@@ -81,7 +81,11 @@ abstract class RawModule(implicit moduleCompileOptions: CompileOptions)
case id: InstanceClone[_] => id.setAsInstanceRef()
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: stop.Stop => id.forceName(None, default="stop", _namespace)
+ case id: assert.Assert => id.forceName(None, default="assert", _namespace)
+ case id: assume.Assume => id.forceName(None, default="assume", _namespace)
+ case id: cover.Cover => id.forceName(None, default="cover", _namespace)
+ case id: printf.Printf => id.forceName(None, default="printf", _namespace)
case id: Data =>
if (id.isSynthesizable) {
id.topBinding match {
diff --git a/core/src/main/scala/chisel3/VerificationStatement.scala b/core/src/main/scala/chisel3/VerificationStatement.scala
new file mode 100644
index 00000000..23adc192
--- /dev/null
+++ b/core/src/main/scala/chisel3/VerificationStatement.scala
@@ -0,0 +1,236 @@
+// SPDX-License-Identifier: Apache-2.0
+
+package chisel3
+
+import scala.reflect.macros.blackbox.Context
+import scala.language.experimental.macros
+import chisel3.internal._
+import chisel3.internal.Builder.pushCommand
+import chisel3.internal.firrtl._
+import chisel3.internal.sourceinfo.SourceInfo
+
+import scala.reflect.macros.blackbox
+
+object assert {
+ /** Checks for a condition to be valid in the circuit at all times. If the
+ * condition evaluates to false, the circuit simulation stops with an error.
+ *
+ * Does not fire when in reset (defined as the encapsulating Module's
+ * reset). If your definition of reset is not the encapsulating Module's
+ * reset, you will need to gate this externally.
+ *
+ * May be called outside of a Module (like defined in a function), so
+ * functions using assert make the standard Module assumptions (single clock
+ * and single reset).
+ *
+ * @param cond condition, assertion fires (simulation fails) when false
+ * @param message optional format string to print when the assertion fires
+ * @param data optional bits to print in the message formatting
+ *
+ * @note See [[printf.apply(fmt:String* printf]] for format string documentation
+ * @note currently cannot be used in core Chisel / libraries because macro
+ * defs need to be compiled first and the SBT project is not set up to do
+ * that
+ */
+ // Macros currently can't take default arguments, so we need two functions to emulate defaults.
+ def apply(cond: Bool, message: String, data: Bits*)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Assert = macro _applyMacroWithMessage
+ def apply(cond: Bool)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Assert = macro _applyMacroWithNoMessage
+
+ /** An elaboration-time assertion. Calls the built-in Scala assert function. */
+ def apply(cond: Boolean, message: => String): Unit = Predef.assert(cond, message)
+ /** An elaboration-time assertion. Calls the built-in Scala assert function. */
+ def apply(cond: Boolean): Unit = Predef.assert(cond, "")
+
+ /** Named class for assertions. */
+ final class Assert private[chisel3]() extends VerificationStatement
+
+ import VerificationStatement._
+
+ def _applyMacroWithMessage(c: blackbox.Context)(cond: c.Tree, message: c.Tree, data: c.Tree*)(sourceInfo: c.Tree, compileOptions: c.Tree): c.Tree = {
+ import c.universe._
+ val apply_impl_do = symbolOf[this.type].asClass.module.info.member(TermName("_applyWithSourceLine"))
+ q"$apply_impl_do($cond, ${getLine(c)}, _root_.scala.Some($message), ..$data)($sourceInfo, $compileOptions)"
+ }
+
+ def _applyMacroWithNoMessage(c: blackbox.Context)(cond: c.Tree)(sourceInfo: c.Tree, compileOptions: c.Tree): c.Tree = {
+ import c.universe._
+ val apply_impl_do = symbolOf[this.type].asClass.module.info.member(TermName("_applyWithSourceLine"))
+ q"$apply_impl_do($cond, ${getLine(c)}, _root_.scala.None)($sourceInfo, $compileOptions)"
+ }
+
+ /** Used by our macros. Do not call directly! */
+ def _applyWithSourceLine(cond: Bool, line: SourceLineInfo, message: Option[String], data: Bits*)
+ (implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Assert = {
+ val id = new Assert()
+ when(!Module.reset.asBool()) {
+ Builder.pushCommand(Verification(id, Formal.Assert, sourceInfo, Module.clock.ref, cond.ref, ""))
+ failureMessage("Assertion", line, cond, message, data)
+ }
+ id
+ }
+}
+
+
+object assume {
+ /** Assumes a condition to be valid in the circuit at all times.
+ * Acts like an assertion in simulation and imposes a declarative
+ * assumption on the state explored by formal tools.
+ *
+ * Does not fire when in reset (defined as the encapsulating Module's
+ * reset). If your definition of reset is not the encapsulating Module's
+ * reset, you will need to gate this externally.
+ *
+ * May be called outside of a Module (like defined in a function), so
+ * functions using assert make the standard Module assumptions (single clock
+ * and single reset).
+ *
+ * @param cond condition, assertion fires (simulation fails) when false
+ * @param message optional format string to print when the assertion fires
+ * @param data optional bits to print in the message formatting
+ *
+ * @note See [[printf.apply(fmt:String* printf]] for format string documentation
+ */
+ // Macros currently can't take default arguments, so we need two functions to emulate defaults.
+ def apply(cond: Bool, message: String, data: Bits*)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Assume = macro _applyMacroWithMessage
+ def apply(cond: Bool)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Assume = macro _applyMacroWithNoMessage
+
+ /** An elaboration-time assumption. Calls the built-in Scala assume function. */
+ def apply(cond: Boolean, message: => String): Unit = Predef.assume(cond, message)
+ /** An elaboration-time assumption. Calls the built-in Scala assume function. */
+ def apply(cond: Boolean): Unit = Predef.assume(cond, "")
+
+ /** Named class for assumptions. */
+ final class Assume private[chisel3]() extends VerificationStatement
+
+ import VerificationStatement._
+
+ def _applyMacroWithMessage(c: blackbox.Context)(cond: c.Tree, message: c.Tree, data: c.Tree*)(sourceInfo: c.Tree, compileOptions: c.Tree): c.Tree = {
+ import c.universe._
+ val apply_impl_do = symbolOf[this.type].asClass.module.info.member(TermName("_applyWithSourceLine"))
+ q"$apply_impl_do($cond, ${getLine(c)}, _root_.scala.Some($message), ..$data)($sourceInfo, $compileOptions)"
+ }
+
+ def _applyMacroWithNoMessage(c: blackbox.Context)(cond: c.Tree)(sourceInfo: c.Tree, compileOptions: c.Tree): c.Tree = {
+ import c.universe._
+ val apply_impl_do = symbolOf[this.type].asClass.module.info.member(TermName("_applyWithSourceLine"))
+ q"$apply_impl_do($cond, ${getLine(c)}, _root_.scala.None)($sourceInfo, $compileOptions)"
+ }
+
+ /** Used by our macros. Do not call directly! */
+ def _applyWithSourceLine(cond: Bool, line: SourceLineInfo, message: Option[String], data: Bits*)
+ (implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Assume = {
+ val id = new Assume()
+ when(!Module.reset.asBool()) {
+ Builder.pushCommand(Verification(id, Formal.Assume, sourceInfo, Module.clock.ref, cond.ref, ""))
+ failureMessage("Assumption", line, cond, message, data)
+ }
+ id
+ }
+}
+
+
+object cover {
+ /** Declares a condition to be covered.
+ * At ever clock event, a counter is incremented iff the condition is active
+ * and reset is inactive.
+ *
+ * Does not fire when in reset (defined as the encapsulating Module's
+ * reset). If your definition of reset is not the encapsulating Module's
+ * reset, you will need to gate this externally.
+ *
+ * May be called outside of a Module (like defined in a function), so
+ * functions using assert make the standard Module assumptions (single clock
+ * and single reset).
+ *
+ * @param cond condition that will be sampled on every clock tick
+ * @param message a string describing the cover event
+ */
+ // Macros currently can't take default arguments, so we need two functions to emulate defaults.
+ def apply(cond: Bool, message: String)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Cover = macro _applyMacroWithMessage
+ def apply(cond: Bool)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Cover = macro _applyMacroWithNoMessage
+
+ /** Named class for cover statements. */
+ final class Cover private[chisel3]() extends VerificationStatement
+
+ import VerificationStatement._
+
+ def _applyMacroWithNoMessage(c: blackbox.Context)(cond: c.Tree)(sourceInfo: c.Tree, compileOptions: c.Tree): c.Tree = {
+ import c.universe._
+ val apply_impl_do = symbolOf[this.type].asClass.module.info.member(TermName("_applyWithSourceLine"))
+ q"$apply_impl_do($cond, ${getLine(c)}, _root_.scala.None)($sourceInfo, $compileOptions)"
+ }
+
+ def _applyMacroWithMessage(c: blackbox.Context)(cond: c.Tree, message: c.Tree)(sourceInfo: c.Tree, compileOptions: c.Tree): c.Tree = {
+ import c.universe._
+ val apply_impl_do = symbolOf[this.type].asClass.module.info.member(TermName("_applyWithSourceLine"))
+ q"$apply_impl_do($cond, ${getLine(c)}, _root_.scala.Some($message))($sourceInfo, $compileOptions)"
+ }
+
+ /** Used by our macros. Do not call directly! */
+ def _applyWithSourceLine(cond: Bool, line: SourceLineInfo, message: Option[String])
+ (implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Cover = {
+ val id = new Cover()
+ when(!Module.reset.asBool()) {
+ Builder.pushCommand(Verification(id, Formal.Cover, sourceInfo, Module.clock.ref, cond.ref, ""))
+ }
+ id
+ }
+}
+
+object stop {
+ /** Terminate execution, indicating success.
+ *
+ * @param message a string describing why the simulation was stopped
+ */
+ def apply(message: String = "")(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Stop = {
+ val stp = new Stop()
+ when (!Module.reset.asBool) {
+ pushCommand(Stop(stp, sourceInfo, Builder.forcedClock.ref, 0))
+ }
+ stp
+ }
+
+ /** Terminate execution with a failure code. */
+ @deprecated("Non-zero return codes are not well supported. Please use assert(false.B) if you want to indicate a failure.", "Chisel 3.5")
+ def apply(code: Int)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Stop = {
+ val stp = new Stop()
+ when (!Module.reset.asBool) {
+ pushCommand(Stop(stp, sourceInfo, Builder.forcedClock.ref, code))
+ }
+ stp
+ }
+
+ /** Named class for [[stop]]s. */
+ final class Stop private[chisel3]()extends VerificationStatement
+}
+
+/** Base class for all verification statements: Assert, Assume, Cover, Stop and Printf. */
+abstract class VerificationStatement extends NamedComponent {
+ _parent.foreach(_.addId(this))
+}
+
+/** Helper functions for common functionality required by stop, assert, assume or cover */
+private object VerificationStatement {
+
+ type SourceLineInfo = (String, Int, String)
+
+ def getLine(c: blackbox.Context): SourceLineInfo = {
+ val p = c.enclosingPosition
+ (p.source.file.name, p.line, p.lineContent.trim)
+ }
+
+ // creates a printf to inform the user of a failed assertion or assumption
+ def failureMessage(kind: String, lineInfo: SourceLineInfo, cond: Bool, message: Option[String], data: Seq[Bits])
+ (implicit sourceInfo: SourceInfo, compileOptions: CompileOptions) : Unit = {
+ val (filename, line, content) = lineInfo
+ val lineMsg = s"$filename:$line $content".replaceAll("%", "%%")
+ val fmt = message match {
+ case Some(msg) =>
+ s"$kind failed: $msg\n at $lineMsg\n"
+ case None => s"$kind failed\n at $lineMsg\n"
+ }
+ when(!cond) {
+ printf.printfWithoutReset(fmt, data:_*)
+ }
+ }
+}
diff --git a/core/src/main/scala/chisel3/experimental/package.scala b/core/src/main/scala/chisel3/experimental/package.scala
index 8018159f..0fc79487 100644
--- a/core/src/main/scala/chisel3/experimental/package.scala
+++ b/core/src/main/scala/chisel3/experimental/package.scala
@@ -166,9 +166,4 @@ 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))
- }
}
diff --git a/core/src/main/scala/chisel3/experimental/verification/package.scala b/core/src/main/scala/chisel3/experimental/verification/package.scala
deleted file mode 100644
index 190083fd..00000000
--- a/core/src/main/scala/chisel3/experimental/verification/package.scala
+++ /dev/null
@@ -1,60 +0,0 @@
-// SPDX-License-Identifier: Apache-2.0
-
-package chisel3.experimental
-
-import chisel3._
-import chisel3.internal.Builder
-import chisel3.internal.firrtl.{Formal, Verification}
-import chisel3.internal.sourceinfo.SourceInfo
-
-package object verification {
-
- object assert {
- /** Named class for assertions. */
- final class Assert(private[chisel3] val predicate: Bool) extends BaseSim
-
-
- def apply(predicate: Bool, msg: String = "")(
- implicit sourceInfo: SourceInfo,
- compileOptions: CompileOptions): Assert = {
- val a = new Assert(predicate)
- when (!Module.reset.asBool) {
- val clock = Module.clock
- Builder.pushCommand(Verification(a, Formal.Assert, sourceInfo, clock.ref, predicate.ref, msg))
- }
- a
- }
- }
-
- object assume {
- /** Named class for assumes. */
- final class Assume(private[chisel3] val predicate: Bool) extends BaseSim
-
- def apply(predicate: Bool, msg: String = "")(
- implicit sourceInfo: SourceInfo,
- compileOptions: CompileOptions): Assume = {
- val a = new Assume(predicate)
- when (!Module.reset.asBool) {
- val clock = Module.clock
- Builder.pushCommand(Verification(a, Formal.Assume, sourceInfo, clock.ref, predicate.ref, msg))
- }
- a
- }
- }
-
- object cover {
- /** Named class for covers. */
- final class Cover(private[chisel3] val predicate: Bool) extends BaseSim
-
- def apply(predicate: Bool, msg: String = "")(
- implicit sourceInfo: SourceInfo,
- compileOptions: CompileOptions): Cover = {
- val clock = Module.clock
- val c = new Cover(predicate)
- when (!Module.reset.asBool) {
- Builder.pushCommand(Verification(c, Formal.Cover, sourceInfo, clock.ref, predicate.ref, msg))
- }
- c
- }
- }
-}
diff --git a/core/src/main/scala/chisel3/internal/firrtl/Converter.scala b/core/src/main/scala/chisel3/internal/firrtl/Converter.scala
index f56c3b15..1dc52823 100644
--- a/core/src/main/scala/chisel3/internal/firrtl/Converter.scala
+++ b/core/src/main/scala/chisel3/internal/firrtl/Converter.scala
@@ -142,8 +142,8 @@ private[chisel3] object Converter {
Some(fir.IsInvalid(convert(info), convert(arg, ctx, info)))
case e @ DefInstance(info, id, _) =>
Some(fir.DefInstance(convert(info), e.name, id.name))
- case Stop(info, clock, ret) =>
- Some(fir.Stop(convert(info), ret, convert(clock, ctx, info), firrtl.Utils.one))
+ case e @ Stop(_, info, clock, ret) =>
+ Some(fir.Stop(convert(info), ret, convert(clock, ctx, info), firrtl.Utils.one, e.name))
case e @ Printf(_, info, clock, pable) =>
val (fmt, args) = unpack(pable, ctx)
Some(fir.Print(convert(info), fir.StringLit(fmt),
diff --git a/core/src/main/scala/chisel3/internal/firrtl/IR.scala b/core/src/main/scala/chisel3/internal/firrtl/IR.scala
index 0b568548..1a06cd36 100644
--- a/core/src/main/scala/chisel3/internal/firrtl/IR.scala
+++ b/core/src/main/scala/chisel3/internal/firrtl/IR.scala
@@ -784,7 +784,7 @@ case class Connect(sourceInfo: SourceInfo, loc: Node, exp: Arg) extends Command
case class BulkConnect(sourceInfo: SourceInfo, loc1: Node, loc2: Node) extends Command
case class Attach(sourceInfo: SourceInfo, locs: Seq[Node]) extends Command
case class ConnectInit(sourceInfo: SourceInfo, loc: Node, exp: Arg) extends Command
-case class Stop(sourceInfo: SourceInfo, clock: Arg, ret: Int) extends Command
+case class Stop(id: stop.Stop, sourceInfo: SourceInfo, clock: Arg, ret: Int) extends Definition
case class Port(id: Data, dir: SpecifiedDirection)
case class Printf(id: printf.Printf, sourceInfo: SourceInfo, clock: Arg, pable: Printable) extends Definition
object Formal extends Enumeration {
@@ -792,7 +792,7 @@ object Formal extends Enumeration {
val Assume = Value("assume")
val Cover = Value("cover")
}
-case class Verification[T <: BaseSim](id: T, op: Formal.Value, sourceInfo: SourceInfo, clock: Arg,
+case class Verification[T <: VerificationStatement](id: T, op: Formal.Value, sourceInfo: SourceInfo, clock: Arg,
predicate: Arg, message: String) extends Definition
abstract class Component extends Arg {
def id: BaseModule