From 29702d7dd10a9eb7595a102bfffcee665bcf7394 Mon Sep 17 00:00:00 2001 From: mergify[bot] Date: Mon, 15 Aug 2022 20:37:55 +0000 Subject: Printables for verification preconditions (backport #2663) (#2680) * Printables for verification preconditions (#2663) Add support for printable within assert and assume verification statements Co-authored-by: Girish Pai Co-authored-by: Megan Wachs Co-authored-by: Jack Koenig (cherry picked from commit 7df5653309b5e48e1732b335610d9a7e8449f903) * Waive MiMa false positive Co-authored-by: Aditya Naik <91489422+adkian-sifive@users.noreply.github.com> Co-authored-by: Jack Koenig --- .../main/scala/chisel3/VerificationStatement.scala | 230 ++++++++++++++++++--- 1 file changed, 198 insertions(+), 32 deletions(-) (limited to 'core') diff --git a/core/src/main/scala/chisel3/VerificationStatement.scala b/core/src/main/scala/chisel3/VerificationStatement.scala index 7229c412..1b13b86c 100644 --- a/core/src/main/scala/chisel3/VerificationStatement.scala +++ b/core/src/main/scala/chisel3/VerificationStatement.scala @@ -11,37 +11,71 @@ import chisel3.internal.sourceinfo.SourceInfo import scala.reflect.macros.blackbox -object assert { +/** Scaladoc information for internal verification statement macros + * that are used in objects assert, assume and cover. + * + * @groupdesc VerifPrintMacros + * + *

+ * '''These internal methods are not part of the public-facing API!''' + *

+ *
+ * + * @groupprio VerifPrintMacros 1001 + */ +trait VerifPrintMacrosDoc + +object assert extends VerifPrintMacrosDoc { + + /** Checks for a condition to be valid in the circuit at rising clock edge + * when not in reset. If the condition evaluates to false, the circuit + * simulation stops with an error. + * + * @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 _applyMacroWithStringMessage /** 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. + * Does not fire when in reset (defined as the current implicit reset, e.g. as set by + * the enclosing `withReset` or Module.reset. * * 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 + * @param cond condition, assertion fires (simulation fails) on a rising clock edge when false and reset is not asserted + * @param message optional chisel Printable type message * - * @note See [[printf.apply(fmt:String* printf]] for format string documentation + * @note See [[printf.apply(fmt:Printable)]] for documentation on printf using Printables * @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* + message: Printable )( implicit sourceInfo: SourceInfo, compileOptions: CompileOptions - ): Assert = macro _applyMacroWithMessage + ): Assert = macro _applyMacroWithPrintableMessage + def apply(cond: Bool)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Assert = macro _applyMacroWithNoMessage @@ -56,6 +90,11 @@ object assert { import VerificationStatement._ + /** @group VerifPrintMacros */ + @deprecated( + "This method has been deprecated in favor of _applyMacroWithStringMessage. Please use the same.", + "Chisel 3.5" + ) def _applyMacroWithMessage( c: blackbox.Context )(cond: c.Tree, @@ -65,10 +104,38 @@ object assert { 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)" + val apply_impl_do = symbolOf[this.type].asClass.module.info.member(TermName("_applyWithSourceLinePrintable")) + q"$apply_impl_do($cond, ${getLine(c)},_root_.scala.Some(_root_.chisel3.Printable.pack($message,..$data)))($sourceInfo, $compileOptions)" } + /** @group VerifPrintMacros */ + def _applyMacroWithStringMessage( + 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("_applyWithSourceLinePrintable")) + q"$apply_impl_do($cond, ${getLine(c)},_root_.scala.Some(_root_.chisel3.Printable.pack($message,..$data)))($sourceInfo, $compileOptions)" + } + + /** @group VerifPrintMacros */ + def _applyMacroWithPrintableMessage( + 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("_applyWithSourceLinePrintable")) + q"$apply_impl_do($cond, ${getLine(c)}, _root_.scala.Some($message))($sourceInfo, $compileOptions)" + } + + /** @group VerifPrintMacros */ def _applyMacroWithNoMessage( c: blackbox.Context )(cond: c.Tree @@ -76,11 +143,14 @@ object assert { compileOptions: c.Tree ): c.Tree = { import c.universe._ - val apply_impl_do = symbolOf[this.type].asClass.module.info.member(TermName("_applyWithSourceLine")) + val apply_impl_do = symbolOf[this.type].asClass.module.info.member(TermName("_applyWithSourceLinePrintable")) q"$apply_impl_do($cond, ${getLine(c)}, _root_.scala.None)($sourceInfo, $compileOptions)" } - /** Used by our macros. Do not call directly! */ + /** This will be removed in Chisel 3.6 in favor of the Printable version + * + * @group VerifPrintMacros + */ def _applyWithSourceLine( cond: Bool, line: SourceLineInfo, @@ -92,14 +162,31 @@ object assert { ): Assert = { val id = new Assert() when(!Module.reset.asBool()) { - failureMessage("Assertion", line, cond, message, data) + failureMessage("Assertion", line, cond, message.map(Printable.pack(_, data: _*))) + Builder.pushCommand(Verification(id, Formal.Assert, sourceInfo, Module.clock.ref, cond.ref, "")) + } + id + } + + /** @group VerifPrintMacros */ + def _applyWithSourceLinePrintable( + cond: Bool, + line: SourceLineInfo, + message: Option[Printable] + )( + implicit sourceInfo: SourceInfo, + compileOptions: CompileOptions + ): Assert = { + val id = new Assert() + when(!Module.reset.asBool()) { + failureMessage("Assertion", line, cond, message) Builder.pushCommand(Verification(id, Formal.Assert, sourceInfo, Module.clock.ref, cond.ref, "")) } id } } -object assume { +object assume extends VerifPrintMacrosDoc { /** Assumes a condition to be valid in the circuit at all times. * Acts like an assertion in simulation and imposes a declarative @@ -127,7 +214,33 @@ object assume { )( implicit sourceInfo: SourceInfo, compileOptions: CompileOptions - ): Assume = macro _applyMacroWithMessage + ): Assume = macro _applyMacroWithStringMessage + + /** 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 Printable type message when the assertion fires + * + * @note See [[printf.apply(fmt:Printable]] for documentation on printf using Printables + */ + def apply( + cond: Bool, + message: Printable + )( + implicit sourceInfo: SourceInfo, + compileOptions: CompileOptions + ): Assume = macro _applyMacroWithPrintableMessage + def apply(cond: Bool)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): Assume = macro _applyMacroWithNoMessage @@ -142,6 +255,11 @@ object assume { import VerificationStatement._ + /** @group VerifPrintMacros */ + @deprecated( + "This method has been deprecated in favor of _applyMacroWithStringMessage. Please use the same.", + "Chisel 3.5" + ) def _applyMacroWithMessage( c: blackbox.Context )(cond: c.Tree, @@ -151,10 +269,38 @@ object assume { 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)" + val apply_impl_do = symbolOf[this.type].asClass.module.info.member(TermName("_applyWithSourceLinePrintable")) + q"$apply_impl_do($cond, ${getLine(c)}, _root_.scala.Some(_root_.chisel3.Printable.pack($message, ..$data)))($sourceInfo, $compileOptions)" } + /** @group VerifPrintMacros */ + def _applyMacroWithStringMessage( + 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("_applyWithSourceLinePrintable")) + q"$apply_impl_do($cond, ${getLine(c)}, _root_.scala.Some(_root_.chisel3.Printable.pack($message, ..$data)))($sourceInfo, $compileOptions)" + } + + /** @group VerifPrintMacros */ + def _applyMacroWithPrintableMessage( + 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("_applyWithSourceLinePrintable")) + q"$apply_impl_do($cond, ${getLine(c)}, _root_.scala.Some($message))($sourceInfo, $compileOptions)" + } + + /** @group VerifPrintMacros */ def _applyMacroWithNoMessage( c: blackbox.Context )(cond: c.Tree @@ -162,11 +308,14 @@ object assume { compileOptions: c.Tree ): c.Tree = { import c.universe._ - val apply_impl_do = symbolOf[this.type].asClass.module.info.member(TermName("_applyWithSourceLine")) + val apply_impl_do = symbolOf[this.type].asClass.module.info.member(TermName("_applyWithSourceLinePrintable")) q"$apply_impl_do($cond, ${getLine(c)}, _root_.scala.None)($sourceInfo, $compileOptions)" } - /** Used by our macros. Do not call directly! */ + /** This will be removed in Chisel 3.6 in favor of the Printable version + * + * @group VerifPrintMacros + */ def _applyWithSourceLine( cond: Bool, line: SourceLineInfo, @@ -178,14 +327,31 @@ object assume { ): Assume = { val id = new Assume() when(!Module.reset.asBool()) { - failureMessage("Assumption", line, cond, message, data) + failureMessage("Assumption", line, cond, message.map(Printable.pack(_, data: _*))) + Builder.pushCommand(Verification(id, Formal.Assume, sourceInfo, Module.clock.ref, cond.ref, "")) + } + id + } + + /** @group VerifPrintMacros */ + def _applyWithSourceLinePrintable( + cond: Bool, + line: SourceLineInfo, + message: Option[Printable] + )( + implicit sourceInfo: SourceInfo, + compileOptions: CompileOptions + ): Assume = { + val id = new Assume() + when(!Module.reset.asBool()) { + failureMessage("Assumption", line, cond, message) Builder.pushCommand(Verification(id, Formal.Assume, sourceInfo, Module.clock.ref, cond.ref, "")) } id } } -object cover { +object cover extends VerifPrintMacrosDoc { /** Declares a condition to be covered. * At ever clock event, a counter is incremented iff the condition is active @@ -213,6 +379,7 @@ object cover { import VerificationStatement._ + /** @group VerifPrintMacros */ def _applyMacroWithNoMessage( c: blackbox.Context )(cond: c.Tree @@ -224,6 +391,7 @@ object cover { q"$apply_impl_do($cond, ${getLine(c)}, _root_.scala.None)($sourceInfo, $compileOptions)" } + /** @group VerifPrintMacros */ def _applyMacroWithMessage( c: blackbox.Context )(cond: c.Tree, @@ -236,7 +404,7 @@ object cover { q"$apply_impl_do($cond, ${getLine(c)}, _root_.scala.Some($message))($sourceInfo, $compileOptions)" } - /** Used by our macros. Do not call directly! */ + /** @group VerifPrintMacros */ def _applyWithSourceLine( cond: Bool, line: SourceLineInfo, @@ -299,13 +467,11 @@ private object VerificationStatement { (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] + message: Option[Printable] )( implicit sourceInfo: SourceInfo, compileOptions: CompileOptions @@ -314,11 +480,11 @@ private object VerificationStatement { 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" + p"$kind failed: $msg\n at $lineMsg\n" + case None => p"$kind failed\n at $lineMsg\n" } when(!cond) { - printf.printfWithoutReset(fmt, data: _*) + printf.printfWithoutReset(fmt) } } } -- cgit v1.2.3