From 5871a65195c7ad96edb9c58dd94cddd942815dfb Mon Sep 17 00:00:00 2001 From: Trevor McKay Date: Fri, 6 Dec 2024 17:33:38 -0800 Subject: [PATCH] Fix potential name collision caused by LTL properties (#4551) --- .../chisel3/util/circt/LTLIntrinsics.scala | 4 +- src/test/scala/chiselTests/LTLSpec.scala | 148 +++++++++++------- 2 files changed, 90 insertions(+), 62 deletions(-) diff --git a/src/main/scala-2/chisel3/util/circt/LTLIntrinsics.scala b/src/main/scala-2/chisel3/util/circt/LTLIntrinsics.scala index 30341f6027..929f3226f0 100644 --- a/src/main/scala-2/chisel3/util/circt/LTLIntrinsics.scala +++ b/src/main/scala-2/chisel3/util/circt/LTLIntrinsics.scala @@ -37,7 +37,7 @@ private[chisel3] object UnaryLTLIntrinsic { )( implicit sourceInfo: SourceInfo ): Bool = - BaseIntrinsic(f"ltl_$intrinsicName", Bool(), params)(_in).suggestName(intrinsicName) + BaseIntrinsic(f"ltl_$intrinsicName", Bool(), params)(_in).suggestName(f"ltl_$intrinsicName") } /** Base instrinsic for all binary intrinsics with `lhs`, `rhs`, and `out` ports. */ @@ -50,7 +50,7 @@ private[chisel3] object BinaryLTLIntrinsic { )( implicit sourceInfo: SourceInfo ): Bool = - BaseIntrinsic(f"ltl_$intrinsicName", Bool(), params)(lhs, rhs).suggestName(intrinsicName) + BaseIntrinsic(f"ltl_$intrinsicName", Bool(), params)(lhs, rhs).suggestName(f"ltl_$intrinsicName") } /** A wrapper intrinsic for the CIRCT `ltl.and` operation. */ diff --git a/src/test/scala/chiselTests/LTLSpec.scala b/src/test/scala/chiselTests/LTLSpec.scala index 78e6017a14..c600e9328d 100644 --- a/src/test/scala/chiselTests/LTLSpec.scala +++ b/src/test/scala/chiselTests/LTLSpec.scala @@ -49,15 +49,21 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { chirrtl should include("input a : UInt<1>") chirrtl should include("input b : UInt<1>") chirrtl should include("input c : UInt<1>") - chirrtl should include(f"node delay = intrinsic(circt_ltl_delay : UInt<1>, a) $sourceLoc") - chirrtl should include(f"node delay_1 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") - chirrtl should include(f"node delay_2 = intrinsic(circt_ltl_delay : UInt<1>, c) $sourceLoc") - chirrtl should include(f"node delay_3 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") - chirrtl should include(f"node concat = intrinsic(circt_ltl_concat : UInt<1>, a, delay_3) $sourceLoc") - chirrtl should include(f"node delay_4 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") - chirrtl should include(f"node concat_1 = intrinsic(circt_ltl_concat : UInt<1>, a, delay_4) $sourceLoc") - chirrtl should include(f"node delay_5 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") - chirrtl should include(f"node concat_2 = intrinsic(circt_ltl_concat : UInt<1>, a, delay_5) $sourceLoc") + chirrtl should include( + f"node ltl_delay = intrinsic(circt_ltl_delay : UInt<1>, a) $sourceLoc" + ) + chirrtl should include( + f"node ltl_delay_1 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc" + ) + chirrtl should include(f"node ltl_delay_2 = intrinsic(circt_ltl_delay : UInt<1>, c) $sourceLoc") + chirrtl should include( + f"node ltl_delay_3 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc" + ) + chirrtl should include(f"node ltl_concat = intrinsic(circt_ltl_concat : UInt<1>, a, ltl_delay_3) $sourceLoc") + chirrtl should include(f"node ltl_delay_4 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") + chirrtl should include(f"node ltl_concat_1 = intrinsic(circt_ltl_concat : UInt<1>, a, ltl_delay_4) $sourceLoc") + chirrtl should include(f"node ltl_delay_5 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") + chirrtl should include(f"node ltl_concat_2 = intrinsic(circt_ltl_concat : UInt<1>, a, ltl_delay_5) $sourceLoc") } it should "compile sequence delay operations" in { ChiselStage.emitSystemVerilog(new DelaysMod) @@ -78,8 +84,8 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { chirrtl should include("input d : UInt<1>") chirrtl should include("input e : UInt<1>") chirrtl should include(f"intrinsic(circt_ltl_concat : UInt<1>, a, b) $sourceLoc") - chirrtl should include(f"node concat_1 = intrinsic(circt_ltl_concat : UInt<1>, c, d) $sourceLoc") - chirrtl should include(f"intrinsic(circt_ltl_concat : UInt<1>, concat_1, e) $sourceLoc") + chirrtl should include(f"node ltl_concat_1 = intrinsic(circt_ltl_concat : UInt<1>, c, d) $sourceLoc") + chirrtl should include(f"intrinsic(circt_ltl_concat : UInt<1>, ltl_concat_1, e) $sourceLoc") } it should "compile sequence concat operations" in { ChiselStage.emitSystemVerilog(new ConcatMod) @@ -102,14 +108,16 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { chirrtl should include("input c : UInt<1>") chirrtl should include("input d : UInt<1>") chirrtl should include("input e : UInt<1>") - chirrtl should include(f"node repeat = intrinsic(circt_ltl_repeat : UInt<1>, a) $sourceLoc") - chirrtl should include(f"node repeat_1 = intrinsic(circt_ltl_repeat : UInt<1>, b) $sourceLoc") - chirrtl should include(f"node repeat_2 = intrinsic(circt_ltl_repeat : UInt<1>, c) $sourceLoc") + chirrtl should include(f"node ltl_repeat = intrinsic(circt_ltl_repeat : UInt<1>, a) $sourceLoc") + chirrtl should include( + f"node ltl_repeat_1 = intrinsic(circt_ltl_repeat : UInt<1>, b) $sourceLoc" + ) + chirrtl should include(f"node ltl_repeat_2 = intrinsic(circt_ltl_repeat : UInt<1>, c) $sourceLoc") chirrtl should include( - f"node goto_repeat = intrinsic(circt_ltl_goto_repeat : UInt<1>, d) $sourceLoc" + f"node ltl_goto_repeat = intrinsic(circt_ltl_goto_repeat : UInt<1>, d) $sourceLoc" ) chirrtl should include( - f"node non_consecutive_repeat = intrinsic(circt_ltl_non_consecutive_repeat : UInt<1>, e) $sourceLoc" + f"node ltl_non_consecutive_repeat = intrinsic(circt_ltl_non_consecutive_repeat : UInt<1>, e) $sourceLoc" ) } it should "compile sequence repeat operations" in { @@ -140,28 +148,38 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { val sourceLoc = "@[Foo.scala 1:2]" // Sequences - chirrtl should include(f"node delay = intrinsic(circt_ltl_delay : UInt<1>, a) $sourceLoc") - chirrtl should include(f"node and = intrinsic(circt_ltl_and : UInt<1>, delay, b) $sourceLoc") - chirrtl should include(f"node or = intrinsic(circt_ltl_or : UInt<1>, delay, b) $sourceLoc") - chirrtl should include(f"node intersect = intrinsic(circt_ltl_intersect : UInt<1>, delay, b) $sourceLoc") - chirrtl should include(f"node intersect_1 = intrinsic(circt_ltl_intersect : UInt<1>, intersect, and) $sourceLoc") - chirrtl should include(f"node intersect_2 = intrinsic(circt_ltl_intersect : UInt<1>, intersect_1, or) $sourceLoc") - chirrtl should include(f"node clock_1 = intrinsic(circt_ltl_clock : UInt<1>, delay, clock) $sourceLoc") + chirrtl should include( + f"node ltl_delay = intrinsic(circt_ltl_delay : UInt<1>, a) $sourceLoc" + ) + chirrtl should include(f"node ltl_and = intrinsic(circt_ltl_and : UInt<1>, ltl_delay, b) $sourceLoc") + chirrtl should include(f"node ltl_or = intrinsic(circt_ltl_or : UInt<1>, ltl_delay, b) $sourceLoc") + chirrtl should include(f"node ltl_intersect = intrinsic(circt_ltl_intersect : UInt<1>, ltl_delay, b) $sourceLoc") + chirrtl should include( + f"node ltl_intersect_1 = intrinsic(circt_ltl_intersect : UInt<1>, ltl_intersect, ltl_and) $sourceLoc" + ) + chirrtl should include( + f"node ltl_intersect_2 = intrinsic(circt_ltl_intersect : UInt<1>, ltl_intersect_1, ltl_or) $sourceLoc" + ) + chirrtl should include(f"node ltl_clock = intrinsic(circt_ltl_clock : UInt<1>, ltl_delay, clock) $sourceLoc") // Properties - chirrtl should include(f"node eventually = intrinsic(circt_ltl_eventually : UInt<1>, a) $sourceLoc") - chirrtl should include(f"node and_1 = intrinsic(circt_ltl_and : UInt<1>, eventually, b) $sourceLoc") - chirrtl should include(f"node or_1 = intrinsic(circt_ltl_or : UInt<1>, eventually, b) $sourceLoc") - chirrtl should include(f"node intersect_3 = intrinsic(circt_ltl_intersect : UInt<1>, eventually, b) $sourceLoc") + chirrtl should include(f"node ltl_eventually = intrinsic(circt_ltl_eventually : UInt<1>, a) $sourceLoc") + chirrtl should include(f"node ltl_and_1 = intrinsic(circt_ltl_and : UInt<1>, ltl_eventually, b) $sourceLoc") + chirrtl should include(f"node ltl_or_1 = intrinsic(circt_ltl_or : UInt<1>, ltl_eventually, b) $sourceLoc") chirrtl should include( - f"node intersect_4 = intrinsic(circt_ltl_intersect : UInt<1>, intersect_3, and_1) $sourceLoc" + f"node ltl_intersect_3 = intrinsic(circt_ltl_intersect : UInt<1>, ltl_eventually, b) $sourceLoc" ) - chirrtl should include(f"node intersect_5 = intrinsic(circt_ltl_intersect : UInt<1>, intersect_4, or_1) $sourceLoc") - chirrtl should include(f"node clock_2 = intrinsic(circt_ltl_clock : UInt<1>, eventually, clock) $sourceLoc") + chirrtl should include( + f"node ltl_intersect_4 = intrinsic(circt_ltl_intersect : UInt<1>, ltl_intersect_3, ltl_and_1) $sourceLoc" + ) + chirrtl should include( + f"node ltl_intersect_5 = intrinsic(circt_ltl_intersect : UInt<1>, ltl_intersect_4, ltl_or_1) $sourceLoc" + ) + chirrtl should include(f"node ltl_clock_1 = intrinsic(circt_ltl_clock : UInt<1>, ltl_eventually, clock) $sourceLoc") // Until - chirrtl should include(f"node until = intrinsic(circt_ltl_until : UInt<1>, delay, b) $sourceLoc") - chirrtl should include(f"node until_1 = intrinsic(circt_ltl_until : UInt<1>, eventually, b) $sourceLoc") + chirrtl should include(f"node ltl_until = intrinsic(circt_ltl_until : UInt<1>, ltl_delay, b) $sourceLoc") + chirrtl should include(f"node ltl_until_1 = intrinsic(circt_ltl_until : UInt<1>, ltl_eventually, b) $sourceLoc") } it should "compile and, or, intersect, and clock operations" in { ChiselStage.emitSystemVerilog(new AndOrClockMod) @@ -199,15 +217,19 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { // Non-overlapping (emitted as `a ## true |-> b`) chirrtl should include( - f"node delay = intrinsic(circt_ltl_delay : UInt<1>, UInt<1>(0h1)) $sourceLoc" + f"node ltl_delay = intrinsic(circt_ltl_delay : UInt<1>, UInt<1>(0h1)) $sourceLoc" + ) + chirrtl should include(f"node ltl_concat = intrinsic(circt_ltl_concat : UInt<1>, a, ltl_delay) $sourceLoc") + chirrtl should include( + f"node ltl_implication_2 = intrinsic(circt_ltl_implication : UInt<1>, ltl_concat, b) $sourceLoc" + ) + chirrtl should include( + f"node ltl_delay_1 = intrinsic(circt_ltl_delay : UInt<1>, UInt<1>(0h1)) $sourceLoc" ) - chirrtl should include(f"node concat = intrinsic(circt_ltl_concat : UInt<1>, a, delay) $sourceLoc") - chirrtl should include(f"node implication_2 = intrinsic(circt_ltl_implication : UInt<1>, concat, b) $sourceLoc") + chirrtl should include(f"node ltl_concat_1 = intrinsic(circt_ltl_concat : UInt<1>, a, ltl_delay_1) $sourceLoc") chirrtl should include( - f"node delay_1 = intrinsic(circt_ltl_delay : UInt<1>, UInt<1>(0h1)) $sourceLoc" + f"node ltl_implication_3 = intrinsic(circt_ltl_implication : UInt<1>, ltl_concat_1, b) $sourceLoc" ) - chirrtl should include(f"node concat_1 = intrinsic(circt_ltl_concat : UInt<1>, a, delay_1) $sourceLoc") - chirrtl should include(f"node implication_3 = intrinsic(circt_ltl_implication : UInt<1>, concat_1, b) $sourceLoc") } it should "compile property implication operation" in { ChiselStage.emitSystemVerilog(new PropImplicationMod) @@ -280,9 +302,9 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { val sourceLoc = "@[Foo.scala 1:2]" chirrtl should include("node has_been_reset = intrinsic(circt_has_been_reset : UInt<1>, clock, reset)") chirrtl should include("node disable = eq(has_been_reset, UInt<1>(0h0))") - chirrtl should include(f"node clock_1 = intrinsic(circt_ltl_clock : UInt<1>, a, clock) $sourceLoc") + chirrtl should include(f"node ltl_clock = intrinsic(circt_ltl_clock : UInt<1>, a, clock) $sourceLoc") chirrtl should include(f"node _T = eq(disable, UInt<1>(0h0)) $sourceLoc") - chirrtl should include(f"intrinsic(circt_verif_$op, clock_1, _T) $sourceLoc") + chirrtl should include(f"intrinsic(circt_verif_$op, ltl_clock, _T) $sourceLoc") } } @@ -311,17 +333,17 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { AssertProperty(a, clock = Some(c), disable = Some(b.asDisable)) }) // with clock; emitted as `assert(clock(a, c))` - chirrtl should include("node clock = intrinsic(circt_ltl_clock : UInt<1>, a, c)") - chirrtl should include("intrinsic(circt_verif_assert, clock)") + chirrtl should include("node ltl_clock = intrinsic(circt_ltl_clock : UInt<1>, a, c)") + chirrtl should include("intrinsic(circt_verif_assert, ltl_clock)") // with disable; emitted as `assert(a, disable)` chirrtl should include("node _T = eq(b, UInt<1>(0h0))") chirrtl should include("intrinsic(circt_verif_assert, a, _T)") // with clock and disable; emitted as `assert(clock(disable(a, b), c))` - chirrtl should include("node clock_1 = intrinsic(circt_ltl_clock : UInt<1>, a, c)") + chirrtl should include("node ltl_clock_1 = intrinsic(circt_ltl_clock : UInt<1>, a, c)") chirrtl should include("node _T_1 = eq(b, UInt<1>(0h0))") - chirrtl should include("intrinsic(circt_verif_assert, clock_1, _T_1)") + chirrtl should include("intrinsic(circt_verif_assert, ltl_clock_1, _T_1)") } class SequenceConvMod extends RawModule { @@ -343,34 +365,40 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { chirrtl should include(s"intrinsic(circt_verif_assert, a) $sourceLoc") // a b - chirrtl should include(s"node concat = intrinsic(circt_ltl_concat : UInt<1>, a, b) $sourceLoc") - chirrtl should include(s"intrinsic(circt_verif_assert, concat) $sourceLoc") + chirrtl should include(s"node ltl_concat = intrinsic(circt_ltl_concat : UInt<1>, a, b) $sourceLoc") + chirrtl should include(s"intrinsic(circt_verif_assert, ltl_concat) $sourceLoc") // Delay() a - chirrtl should include(s"node delay = intrinsic(circt_ltl_delay : UInt<1>, a) $sourceLoc") - chirrtl should include(s"intrinsic(circt_verif_assert, delay) $sourceLoc") + chirrtl should include( + s"node ltl_delay = intrinsic(circt_ltl_delay : UInt<1>, a) $sourceLoc" + ) + chirrtl should include(s"intrinsic(circt_verif_assert, ltl_delay) $sourceLoc") // a Delay() b - chirrtl should include(s"node delay_1 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") - chirrtl should include(s"node concat_1 = intrinsic(circt_ltl_concat : UInt<1>, a, delay_1) $sourceLoc") - chirrtl should include(s"intrinsic(circt_verif_assert, concat_1) $sourceLoc") + chirrtl should include( + s"node ltl_delay_1 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc" + ) + chirrtl should include(s"node ltl_concat_1 = intrinsic(circt_ltl_concat : UInt<1>, a, ltl_delay_1) $sourceLoc") + chirrtl should include(s"intrinsic(circt_verif_assert, ltl_concat_1) $sourceLoc") // a Delay(2) b - chirrtl should include(s"node delay_2 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") - chirrtl should include(s"node concat_2 = intrinsic(circt_ltl_concat : UInt<1>, a, delay_2) $sourceLoc") - chirrtl should include(s"intrinsic(circt_verif_assert, concat_2) $sourceLoc") + chirrtl should include( + s"node ltl_delay_2 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc" + ) + chirrtl should include(s"node ltl_concat_2 = intrinsic(circt_ltl_concat : UInt<1>, a, ltl_delay_2) $sourceLoc") + chirrtl should include(s"intrinsic(circt_verif_assert, ltl_concat_2) $sourceLoc") // a Delay(42, 1337) b chirrtl should include( - s"node delay_3 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc" + s"node ltl_delay_3 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc" ) - chirrtl should include(s"node concat_3 = intrinsic(circt_ltl_concat : UInt<1>, a, delay_3) $sourceLoc") - chirrtl should include(s"intrinsic(circt_verif_assert, concat_3) $sourceLoc") + chirrtl should include(s"node ltl_concat_3 = intrinsic(circt_ltl_concat : UInt<1>, a, ltl_delay_3) $sourceLoc") + chirrtl should include(s"intrinsic(circt_verif_assert, ltl_concat_3) $sourceLoc") // a Delay(9001, None) sb - chirrtl should include(s"node delay_4 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") - chirrtl should include(s"node concat_4 = intrinsic(circt_ltl_concat : UInt<1>, a, delay_4) $sourceLoc") - chirrtl should include(s"intrinsic(circt_verif_assert, concat_4) $sourceLoc") + chirrtl should include(s"node ltl_delay_4 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") + chirrtl should include(s"node ltl_concat_4 = intrinsic(circt_ltl_concat : UInt<1>, a, ltl_delay_4) $sourceLoc") + chirrtl should include(s"intrinsic(circt_verif_assert, ltl_concat_4) $sourceLoc") } it should "compile Sequence(...) convenience constructor" in { ChiselStage.emitSystemVerilog(new SequenceConvMod)