make all verification statements publically available (#2089)

1 files changed, 236 insertions, 0 deletions

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:_*)
+    }
+  }
+}