From d1d38bd096fce8b92468720fbedc835ecda40e6b Mon Sep 17 00:00:00 2001 From: Kevin Laeufer Date: Thu, 23 Sep 2021 11:12:26 -0700 Subject: make all verification statements publically available (#2089) --- core/src/main/scala/chisel3/Assert.scala | 92 -------- core/src/main/scala/chisel3/Printf.scala | 3 +- core/src/main/scala/chisel3/RawModule.scala | 8 +- .../main/scala/chisel3/VerificationStatement.scala | 236 +++++++++++++++++++++ .../main/scala/chisel3/experimental/package.scala | 5 - .../experimental/verification/package.scala | 60 ------ .../scala/chisel3/internal/firrtl/Converter.scala | 4 +- .../main/scala/chisel3/internal/firrtl/IR.scala | 4 +- 8 files changed, 247 insertions(+), 165 deletions(-) delete mode 100644 core/src/main/scala/chisel3/Assert.scala create mode 100644 core/src/main/scala/chisel3/VerificationStatement.scala delete mode 100644 core/src/main/scala/chisel3/experimental/verification/package.scala (limited to 'core/src/main/scala/chisel3') 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 -- cgit v1.2.3