Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add ifElseFatal intrinsics; use it for chisel3.assert emission #4001

Merged
merged 2 commits into from
Apr 24, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions core/src/main/scala/chisel3/BlackBox.scala
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,9 @@ package experimental {
case class DoubleParam(value: Double) extends Param
case class StringParam(value: String) extends Param

/** Creates a parameter from the Printable's resulting format String */
case class PrintableParam(value: chisel3.Printable, context: BaseModule) extends Param

/** Unquoted String */
case class RawParam(value: String) extends Param

Expand Down
13 changes: 13 additions & 0 deletions core/src/main/scala/chisel3/Printable.scala
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,10 @@ sealed abstract class Printable {
*/
def unpack(ctx: Component): (String, Iterable[String])

/** Unpack into a Seq of captured Bits arguments
*/
def unpackArgs: Seq[Bits]

/** Allow for appending Printables like Strings */
final def +(that: Printable): Printables = Printables(List(this, that))

Expand Down Expand Up @@ -155,12 +159,16 @@ case class Printables(pables: Iterable[Printable]) extends Printable {
val (fmts, args) = pables.map(_.unpack(ctx)).unzip
(fmts.mkString, args.flatten)
}

final def unpackArgs: Seq[Bits] = pables.view.flatMap(_.unpackArgs).toList
}

/** Wrapper for printing Scala Strings */
case class PString(str: String) extends Printable {
final def unpack(ctx: Component): (String, Iterable[String]) =
(str.replaceAll("%", "%%"), List.empty)

final def unpackArgs: Seq[Bits] = List.empty
}

/** Superclass for Firrtl format specifiers for Bits */
Expand All @@ -169,6 +177,8 @@ sealed abstract class FirrtlFormat(private[chisel3] val specifier: Char) extends
def unpack(ctx: Component): (String, Iterable[String]) = {
(s"%$specifier", List(bits.ref.fullName(ctx)))
}

def unpackArgs: Seq[Bits] = List(bits)
}
object FirrtlFormat {
final val legalSpecifiers = List('d', 'x', 'b', 'c')
Expand Down Expand Up @@ -209,14 +219,17 @@ case class Character(bits: Bits) extends FirrtlFormat('c')
/** Put innermost name (eg. field of bundle) */
case class Name(data: Data) extends Printable {
final def unpack(ctx: Component): (String, Iterable[String]) = (data.ref.name, List.empty)
final def unpackArgs: Seq[Bits] = List.empty
}

/** Put full name within parent namespace (eg. bundleName.field) */
case class FullName(data: Data) extends Printable {
final def unpack(ctx: Component): (String, Iterable[String]) = (data.ref.fullName(ctx), List.empty)
final def unpackArgs: Seq[Bits] = List.empty
}

/** Represents escaped percents */
case object Percent extends Printable {
final def unpack(ctx: Component): (String, Iterable[String]) = ("%%", List.empty)
final def unpackArgs: Seq[Bits] = List.empty
}
57 changes: 19 additions & 38 deletions core/src/main/scala/chisel3/VerificationStatement.scala
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,8 @@ import scala.language.experimental.macros
import chisel3.internal._
import chisel3.internal.Builder.pushCommand
import chisel3.internal.firrtl.ir._
import chisel3.experimental.SourceInfo
import chisel3.experimental.{BaseModule, SourceInfo}
import chisel3.util.circt.IfElseFatalIntrinsic

import scala.annotation.nowarn
import scala.reflect.macros.blackbox
Expand Down Expand Up @@ -56,10 +57,6 @@ object assert extends VerifPrintMacrosDoc {
* 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) on a rising clock edge when false and reset is not asserted
* @param message optional chisel Printable type message
*
Expand Down Expand Up @@ -139,6 +136,19 @@ object assert extends VerifPrintMacrosDoc {
q"$apply_impl_do($cond, ${getLine(c)}, _root_.scala.None)($sourceInfo)"
}

private def emitIfElseFatalIntrinsic(
clock: Clock,
predicate: Bool,
enable: Bool,
format: Printable
)(
implicit sourceInfo: SourceInfo
): Assert = {
val id = Builder.forcedUserModule // It should be safe since we push commands anyway.
IfElseFatalIntrinsic(id, format, "chisel3_builtin", clock, predicate, enable, format.unpackArgs: _*)(sourceInfo)
new Assert()
}

/** This will be removed in Chisel 3.6 in favor of the Printable version
*
* @group VerifPrintMacros
Expand All @@ -151,12 +161,8 @@ object assert extends VerifPrintMacrosDoc {
)(
implicit sourceInfo: SourceInfo
): Assert = {
val id = new Assert()
when(!Module.reset.asBool) {
failureMessage("Assertion", line, cond, message.map(Printable.pack(_, data: _*)))
Builder.pushCommand(Verification(id, Formal.Assert, sourceInfo, Module.clock.ref, cond.ref, ""))
}
id
val pable = formatFailureMessage("Assertion", line, cond, message.map(Printable.pack(_, data: _*)))
emitIfElseFatalIntrinsic(Module.clock, cond, !Module.reset.asBool, pable)
}

/** @group VerifPrintMacros */
Expand All @@ -167,13 +173,9 @@ object assert extends VerifPrintMacrosDoc {
)(
implicit sourceInfo: SourceInfo
): Assert = {
val id = new Assert()
message.foreach(Printable.checkScope(_))
when(!Module.reset.asBool) {
failureMessage("Assertion", line, cond, message)
Builder.pushCommand(Verification(id, Formal.Assert, sourceInfo, Module.clock.ref, cond.ref, ""))
}
id
val pable = formatFailureMessage("Assertion", line, cond, message)
emitIfElseFatalIntrinsic(Module.clock, cond, !Module.reset.asBool, pable)
}
}

Expand Down Expand Up @@ -214,10 +216,6 @@ object assume extends VerifPrintMacrosDoc {
* 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
*
Expand Down Expand Up @@ -342,10 +340,6 @@ object cover extends VerifPrintMacrosDoc {
* 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
*/
Expand Down Expand Up @@ -462,17 +456,4 @@ private object VerificationStatement {
case None => p"$kind failed\n at $lineMsg\n"
}
}

def failureMessage(
kind: String,
lineInfo: SourceLineInfo,
cond: Bool,
message: Option[Printable]
)(
implicit sourceInfo: SourceInfo
): Unit = {
when(!cond) {
printf.printfWithoutReset(formatFailureMessage(kind, lineInfo, cond, message))
}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
package chisel3.util.circt

import chisel3._
import chisel3.internal._
import chisel3.experimental.{BaseModule, SourceInfo}

/** Create an `ifelsefatal` style assertion.
*/
private[chisel3] object IfElseFatalIntrinsic {
def apply(
id: BaseModule,
format: Printable,
label: String,
clock: Clock,
predicate: Bool,
enable: Bool,
data: Data*
)(
implicit sourceInfo: SourceInfo
): Unit = {
Intrinsic(
"circt_chisel_ifelsefatal",
"format" -> chisel3.experimental.PrintableParam(format, id),
"label" -> label
)((Seq(clock, predicate, enable) ++ data): _*)
}
}
9 changes: 7 additions & 2 deletions core/src/main/scala/chisel3/internal/firrtl/Converter.scala
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ import chisel3.internal.{castToInt, throwException, HasId}
import chisel3.internal.firrtl.ir._
import chisel3.EnumType
import scala.annotation.tailrec
import scala.collection.immutable.{Queue, VectorBuilder}
import scala.collection.immutable.{Queue, VectorBuilder, VectorMap}

private[chisel3] object Converter {
// TODO modeled on unpack method on Printable, refactor?
Expand Down Expand Up @@ -463,7 +463,12 @@ private[chisel3] object Converter {
case IntParam(value) => fir.IntParam(name, value)
case DoubleParam(value) => fir.DoubleParam(name, value)
case StringParam(value) => fir.StringParam(name, fir.StringLit(value))
case RawParam(value) => fir.RawStringParam(name, value)
case PrintableParam(value, id) => {
val ctx = id._component.get
val (fmt, _) = unpack(value, ctx)
fir.StringParam(name, fir.StringLit(fmt))
}
case RawParam(value) => fir.RawStringParam(name, value)
}

// TODO: Modify Panama CIRCT to account for type aliasing information. This is a temporary hack to
Expand Down
15 changes: 9 additions & 6 deletions src/test/scala/chiselTests/VerificationSpec.scala
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ class SimpleTest extends Module {
cover(io.in === 3.U)
when(io.in === 3.U) {
assume(io.in =/= 2.U)
assert(io.out === io.in)
assert(io.out === io.in, p"${FullName(io.in)}:${io.in} is equal to ${FullName(io.out)}:${io.out}")
}
}

Expand All @@ -30,16 +30,19 @@ class VerificationSpec extends ChiselPropSpec with Matchers {

property("basic equality check should work") {
val fir = ChiselStage.emitCHIRRTL(new SimpleTest)
val lines = fir.split("\n").map(_.trim).toIndexedSeq
val lines = fir.split("(\n|@)").map(_.trim).toIndexedSeq

// reset guard around the verification statement
assertContains(lines, "when _T_1 : ")
assertContains(lines, "when _T_1 :")
assertContains(lines, "cover(clock, _T, UInt<1>(0h1), \"\")")

assertContains(lines, "assume(clock, _T_3, UInt<1>(0h1), \"Assumption failed")

assertContains(lines, "when _T_7 : ")
assertContains(lines, "assert(clock, _T_5, UInt<1>(0h1), \"\")")
assertContains(lines, "node _T_5 = eq(io.out, io.in)")
assertContains(lines, "node _T_6 = eq(reset, UInt<1>(0h0))")
assertContains(
lines,
"""intrinsic(circt_chisel_ifelsefatal<format = "Assertion failed: io.in:%d is equal to io.out:%d\n at VerificationSpec.scala:20 assert(io.out === io.in, p\"${FullName(io.in)}:${io.in} is equal to ${FullName(io.out)}:${io.out}\")\n", label = "chisel3_builtin">, clock, _T_5, _T_6, io.in, io.out)"""
)
}

property("annotation of verification constructs should work") {
Expand Down
2 changes: 0 additions & 2 deletions src/test/scala/chiselTests/naming/NamePluginSpec.scala
Original file line number Diff line number Diff line change
Expand Up @@ -75,14 +75,12 @@ class NamePluginSpec extends ChiselFlatSpec with Utils {
val foo, bar = IO(Input(UInt(8.W)))

{
val x1 = chisel3.assert(1.U === 1.U)
val x2 = cover(foo =/= bar)
val x3 = chisel3.assume(foo =/= 123.U)
val x4 = printf("foo = %d\n", foo)
}
}
val chirrtl = ChiselStage.emitCHIRRTL(new Test)
(chirrtl should include).regex("assert.*: x1")
(chirrtl should include).regex("cover.*: x2")
(chirrtl should include).regex("assume.*: x3")
(chirrtl should include).regex("printf.*: x4")
Expand Down
6 changes: 2 additions & 4 deletions src/test/scala/chiselTests/naming/PrefixSpec.scala
Original file line number Diff line number Diff line change
Expand Up @@ -460,17 +460,15 @@ class PrefixSpec extends ChiselPropSpec with Utils {

{
val x5 = {
val x1 = chisel3.assert(1.U === 1.U)
val x2 = cover(foo =/= bar)
val x3 = chisel3.assume(foo =/= 123.U)
val x4 = printf("foo = %d\n", foo)
x1
x2
}
}
}
val chirrtl = ChiselStage.emitCHIRRTL(new Test)
(chirrtl should include).regex("assert.*: x5")
(chirrtl should include).regex("cover.*: x5_x2")
(chirrtl should include).regex("cover.*: x5")
(chirrtl should include).regex("assume.*: x5_x3")
Comment on lines 461 to 472
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I know this PR is just a re-application of 2 previously reverted PRs so I'm not going to block on this issue (since it was in a PR I previously approved), but this is not ideal. We should be able to maintain the old label behavior, but it will probably require a new Printable that wraps the Assert() object that we return from chisel3.assert.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, so instead of "chisel3_builtin" being the label for all of these, they get the "valname"/name included that would previously be mixed in by putting it in the "optional name" (trailing ": asdf" this test checks for)?

Yes that seems rather useful!

So Printable would help get a friendly name available (that's not available when IntrinsicExpr apply is called) so we could append it to the label StringParam while converting to the FIRRTL IR object, thereabouts? Makes sense to me!

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FYI previous behavior was just dropping optional names (assert_ label in the test) emitted for assert op. chisel3_builtin was used regardless of optional names.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So Printable would help get a friendly name available (that's not available when IntrinsicExpr apply is called) so we could append it to the label StringParam while converting to the FIRRTL IR object, thereabouts? Makes sense to me!

Exactly!

FYI previous behavior was just dropping optional names (assert_ label in the test) emitted for assert op. chisel3_builtin was used regardless of optional names.

Perhaps for these asserts in firtool, but the intent was always to try to replace printf-encoded with real asserts with reasonable label behavior. This has been used by ChiselTest users, we just never fully implemented it in firtool, nor for printf-encoded asserts, but we should.

(chirrtl should include).regex("printf.*: x5_x4")
}
Expand Down
Loading