From e898cf141c414864f22e70ab047b866c804dddac Mon Sep 17 00:00:00 2001 From: Trevor McKay Date: Thu, 5 Dec 2024 14:48:25 -0800 Subject: [PATCH 1/7] reproduce LTL name collision in unit test --- src/test/scala/chiselTests/LTLSpec.scala | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/test/scala/chiselTests/LTLSpec.scala b/src/test/scala/chiselTests/LTLSpec.scala index 78e6017a14..76f74b6572 100644 --- a/src/test/scala/chiselTests/LTLSpec.scala +++ b/src/test/scala/chiselTests/LTLSpec.scala @@ -407,4 +407,23 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { assert(assertBlockLoc < delayIntrinsicLoc) assert(assumeblockLoc < implicationIntrinsicLoc) } + + it should "not produce name collisions" in { + class Test extends RawModule { + val io = IO(Input(UInt(8.W))) + + val clockWire = Wire(Clock()) + val resetWire = Wire(Reset()) + + withClockAndReset(clockWire, resetWire) { + AssertProperty(Property.eventually(io.orR)) + } + + val clock = IO(Input(Clock())) + val reset = IO(Input(Reset())) + + clockWire := clock + resetWire := reset + } + } } From 146398913fcfef43f4101e391bed869cc10f45da Mon Sep 17 00:00:00 2001 From: Trevor McKay Date: Thu, 5 Dec 2024 15:33:32 -0800 Subject: [PATCH 2/7] fix test --- src/test/scala/chiselTests/LTLSpec.scala | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/test/scala/chiselTests/LTLSpec.scala b/src/test/scala/chiselTests/LTLSpec.scala index 76f74b6572..9313a1a490 100644 --- a/src/test/scala/chiselTests/LTLSpec.scala +++ b/src/test/scala/chiselTests/LTLSpec.scala @@ -413,17 +413,15 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { val io = IO(Input(UInt(8.W))) val clockWire = Wire(Clock()) - val resetWire = Wire(Reset()) - withClockAndReset(clockWire, resetWire) { + withClock(clockWire) { AssertProperty(Property.eventually(io.orR)) } val clock = IO(Input(Clock())) - val reset = IO(Input(Reset())) - clockWire := clock - resetWire := reset } + + val chirrtl = ChiselStage.emitCHIRRTL(new Test) } } From c644b0bf0b381ba23b4a9ae00a6d9d1728c78d5f Mon Sep 17 00:00:00 2001 From: Trevor McKay Date: Thu, 5 Dec 2024 15:54:28 -0800 Subject: [PATCH 3/7] do not suggest names for LTL intrinsics --- src/main/scala-2/chisel3/util/circt/LTLIntrinsics.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 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..2e2e6da773 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) } /** 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) } /** A wrapper intrinsic for the CIRCT `ltl.and` operation. */ From 77fbf0ea4ef1c30331de04dbc39132cb16f7d6d0 Mon Sep 17 00:00:00 2001 From: Trevor McKay Date: Thu, 5 Dec 2024 19:39:59 -0800 Subject: [PATCH 4/7] update tests --- src/test/scala/chiselTests/LTLSpec.scala | 136 +++++++++++------------ 1 file changed, 68 insertions(+), 68 deletions(-) diff --git a/src/test/scala/chiselTests/LTLSpec.scala b/src/test/scala/chiselTests/LTLSpec.scala index 9313a1a490..9cc9db39d6 100644 --- a/src/test/scala/chiselTests/LTLSpec.scala +++ b/src/test/scala/chiselTests/LTLSpec.scala @@ -49,15 +49,15 @@ 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 _T = intrinsic(circt_ltl_delay : UInt<1>, a) $sourceLoc") + chirrtl should include(f"node _T_1 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") + chirrtl should include(f"node _T_2 = intrinsic(circt_ltl_delay : UInt<1>, c) $sourceLoc") + chirrtl should include(f"node _T_3 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") + chirrtl should include(f"node _T_4 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_3) $sourceLoc") + chirrtl should include(f"node _T_5 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") + chirrtl should include(f"node _T_6 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_5) $sourceLoc") + chirrtl should include(f"node _T_7 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") + chirrtl should include(f"node _T_8 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_7) $sourceLoc") } it should "compile sequence delay operations" in { ChiselStage.emitSystemVerilog(new DelaysMod) @@ -77,9 +77,9 @@ 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"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 _T = intrinsic(circt_ltl_concat : UInt<1>, a, b) $sourceLoc") + chirrtl should include(f"node _T_1 = intrinsic(circt_ltl_concat : UInt<1>, c, d) $sourceLoc") + chirrtl should include(f"node _T_2 = intrinsic(circt_ltl_concat : UInt<1>, _T_1, e) $sourceLoc") } it should "compile sequence concat operations" in { ChiselStage.emitSystemVerilog(new ConcatMod) @@ -102,14 +102,14 @@ 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 _T = intrinsic(circt_ltl_repeat : UInt<1>, a) $sourceLoc") + chirrtl should include(f"node _T_1 = intrinsic(circt_ltl_repeat : UInt<1>, b) $sourceLoc") + chirrtl should include(f"node _T_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 _T_3 = 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 _T_4 = intrinsic(circt_ltl_non_consecutive_repeat : UInt<1>, e) $sourceLoc" ) } it should "compile sequence repeat operations" in { @@ -140,28 +140,28 @@ 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 _T = intrinsic(circt_ltl_delay : UInt<1>, a) $sourceLoc") + chirrtl should include(f"node _T_1 = intrinsic(circt_ltl_and : UInt<1>, _T, b) $sourceLoc") + chirrtl should include(f"node _T_2 = intrinsic(circt_ltl_or : UInt<1>, _T, b) $sourceLoc") + chirrtl should include(f"node _T_3 = intrinsic(circt_ltl_intersect : UInt<1>, _T, b) $sourceLoc") + chirrtl should include(f"node _T_4 = intrinsic(circt_ltl_intersect : UInt<1>, _T_3, _T_1) $sourceLoc") + chirrtl should include(f"node _T_5 = intrinsic(circt_ltl_intersect : UInt<1>, _T_4, _T_2) $sourceLoc") + chirrtl should include(f"node _T_6 = intrinsic(circt_ltl_clock : UInt<1>, _T, 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 _T_7 = intrinsic(circt_ltl_eventually : UInt<1>, a) $sourceLoc") + chirrtl should include(f"node _T_8 = intrinsic(circt_ltl_and : UInt<1>, _T_7, b) $sourceLoc") + chirrtl should include(f"node _T_9 = intrinsic(circt_ltl_or : UInt<1>, _T_7, b) $sourceLoc") + chirrtl should include(f"node _T_10 = intrinsic(circt_ltl_intersect : UInt<1>, _T_7, b) $sourceLoc") chirrtl should include( - f"node intersect_4 = intrinsic(circt_ltl_intersect : UInt<1>, intersect_3, and_1) $sourceLoc" + f"node _T_11 = intrinsic(circt_ltl_intersect : UInt<1>, _T_10, _T_8) $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 _T_12 = intrinsic(circt_ltl_intersect : UInt<1>, _T_11, _T_9) $sourceLoc") + chirrtl should include(f"node _T_13 = intrinsic(circt_ltl_clock : UInt<1>, _T_7, 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 _T_14 = intrinsic(circt_ltl_until : UInt<1>, _T, b) $sourceLoc") + chirrtl should include(f"node _T_15 = intrinsic(circt_ltl_until : UInt<1>, _T_7, b) $sourceLoc") } it should "compile and, or, intersect, and clock operations" in { ChiselStage.emitSystemVerilog(new AndOrClockMod) @@ -194,20 +194,20 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { val sourceLoc = "@[Foo.scala 1:2]" // Overlapping - chirrtl should include(f"intrinsic(circt_ltl_implication : UInt<1>, a, b) $sourceLoc") - chirrtl should include(f"intrinsic(circt_ltl_implication : UInt<1>, a, b) $sourceLoc") + chirrtl should include(f"node _T = intrinsic(circt_ltl_implication : UInt<1>, a, b) $sourceLoc") + chirrtl should include(f"node _T_1 = intrinsic(circt_ltl_implication : UInt<1>, a, b) $sourceLoc") // 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 _T_2 = 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 _T_3 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_2) $sourceLoc") + chirrtl should include(f"node _T_4 = intrinsic(circt_ltl_implication : UInt<1>, _T_3, b) $sourceLoc") chirrtl should include( - f"node delay_1 = intrinsic(circt_ltl_delay : UInt<1>, UInt<1>(0h1)) $sourceLoc" + f"node _T_5 = intrinsic(circt_ltl_delay : UInt<1>, UInt<1>(0h1)) $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") + chirrtl should include(f"node _T_6 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_5) $sourceLoc") + chirrtl should include(f"node _T_7 = intrinsic(circt_ltl_implication : UInt<1>, _T_6, b) $sourceLoc") } it should "compile property implication operation" in { ChiselStage.emitSystemVerilog(new PropImplicationMod) @@ -280,9 +280,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 _T = eq(disable, UInt<1>(0h0)) $sourceLoc") - chirrtl should include(f"intrinsic(circt_verif_$op, clock_1, _T) $sourceLoc") + chirrtl should include(f"node _T = intrinsic(circt_ltl_clock : UInt<1>, a, clock) $sourceLoc") + chirrtl should include(f"node _T_1 = eq(disable, UInt<1>(0h0)) $sourceLoc") + chirrtl should include(f"intrinsic(circt_verif_$op, _T, _T_1) $sourceLoc") } } @@ -311,17 +311,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 _T = intrinsic(circt_ltl_clock : UInt<1>, a, c)") + chirrtl should include("intrinsic(circt_verif_assert, _T)") // 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)") + chirrtl should include("node _T_1 = eq(b, UInt<1>(0h0))") + chirrtl should include("intrinsic(circt_verif_assert, a, _T_1)") // 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 _T_1 = eq(b, UInt<1>(0h0))") - chirrtl should include("intrinsic(circt_verif_assert, clock_1, _T_1)") + chirrtl should include("node _T_2 = intrinsic(circt_ltl_clock : UInt<1>, a, c)") + chirrtl should include("node _T_3 = eq(b, UInt<1>(0h0))") + chirrtl should include("intrinsic(circt_verif_assert, _T_2, _T_3)") } class SequenceConvMod extends RawModule { @@ -343,34 +343,34 @@ 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 _T = intrinsic(circt_ltl_concat : UInt<1>, a, b) $sourceLoc") + chirrtl should include(s"intrinsic(circt_verif_assert, _T) $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 _T_1 = intrinsic(circt_ltl_delay : UInt<1>, a) $sourceLoc") + chirrtl should include(s"intrinsic(circt_verif_assert, _T_1) $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 _T_2 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") + chirrtl should include(s"node _T_3 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_2) $sourceLoc") + chirrtl should include(s"intrinsic(circt_verif_assert, _T_3) $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 _T_4 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") + chirrtl should include(s"node _T_5 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_4) $sourceLoc") + chirrtl should include(s"intrinsic(circt_verif_assert, _T_5) $sourceLoc") // a Delay(42, 1337) b chirrtl should include( - s"node delay_3 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc" + s"node _T_6 = 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 _T_7 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_6) $sourceLoc") + chirrtl should include(s"intrinsic(circt_verif_assert, _T_7) $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 _T_8 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") + chirrtl should include(s"node _T_9 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_8) $sourceLoc") + chirrtl should include(s"intrinsic(circt_verif_assert, _T_9) $sourceLoc") } it should "compile Sequence(...) convenience constructor" in { ChiselStage.emitSystemVerilog(new SequenceConvMod) @@ -408,7 +408,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { assert(assumeblockLoc < implicationIntrinsicLoc) } - it should "not produce name collisions" in { + it should "not produce name collisions with clock" in { class Test extends RawModule { val io = IO(Input(UInt(8.W))) From 71f5810cf64539ef19990a2bdaecc87bba55a1b5 Mon Sep 17 00:00:00 2001 From: Trevor McKay Date: Fri, 6 Dec 2024 11:39:29 -0800 Subject: [PATCH 5/7] suggestName, but with ltl_ prefix --- src/main/scala-2/chisel3/util/circt/LTLIntrinsics.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala-2/chisel3/util/circt/LTLIntrinsics.scala b/src/main/scala-2/chisel3/util/circt/LTLIntrinsics.scala index 2e2e6da773..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) + 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) + BaseIntrinsic(f"ltl_$intrinsicName", Bool(), params)(lhs, rhs).suggestName(f"ltl_$intrinsicName") } /** A wrapper intrinsic for the CIRCT `ltl.and` operation. */ From 5023a5b834f430f3bea379ecbf03e85e5bbf3a45 Mon Sep 17 00:00:00 2001 From: Trevor McKay Date: Fri, 6 Dec 2024 11:59:39 -0800 Subject: [PATCH 6/7] update tests --- src/test/scala/chiselTests/LTLSpec.scala | 151 ++++++++++------------- 1 file changed, 67 insertions(+), 84 deletions(-) diff --git a/src/test/scala/chiselTests/LTLSpec.scala b/src/test/scala/chiselTests/LTLSpec.scala index 9cc9db39d6..a46faafcd5 100644 --- a/src/test/scala/chiselTests/LTLSpec.scala +++ b/src/test/scala/chiselTests/LTLSpec.scala @@ -49,15 +49,15 @@ 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 _T = intrinsic(circt_ltl_delay : UInt<1>, a) $sourceLoc") - chirrtl should include(f"node _T_1 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") - chirrtl should include(f"node _T_2 = intrinsic(circt_ltl_delay : UInt<1>, c) $sourceLoc") - chirrtl should include(f"node _T_3 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") - chirrtl should include(f"node _T_4 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_3) $sourceLoc") - chirrtl should include(f"node _T_5 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") - chirrtl should include(f"node _T_6 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_5) $sourceLoc") - chirrtl should include(f"node _T_7 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") - chirrtl should include(f"node _T_8 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_7) $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) @@ -77,9 +77,9 @@ 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 _T = intrinsic(circt_ltl_concat : UInt<1>, a, b) $sourceLoc") - chirrtl should include(f"node _T_1 = intrinsic(circt_ltl_concat : UInt<1>, c, d) $sourceLoc") - chirrtl should include(f"node _T_2 = intrinsic(circt_ltl_concat : UInt<1>, _T_1, e) $sourceLoc") + chirrtl should include(f"intrinsic(circt_ltl_concat : UInt<1>, a, b) $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 +102,14 @@ 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 _T = intrinsic(circt_ltl_repeat : UInt<1>, a) $sourceLoc") - chirrtl should include(f"node _T_1 = intrinsic(circt_ltl_repeat : UInt<1>, b) $sourceLoc") - chirrtl should include(f"node _T_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 _T_3 = 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 _T_4 = 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 +140,28 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { val sourceLoc = "@[Foo.scala 1:2]" // Sequences - chirrtl should include(f"node _T = intrinsic(circt_ltl_delay : UInt<1>, a) $sourceLoc") - chirrtl should include(f"node _T_1 = intrinsic(circt_ltl_and : UInt<1>, _T, b) $sourceLoc") - chirrtl should include(f"node _T_2 = intrinsic(circt_ltl_or : UInt<1>, _T, b) $sourceLoc") - chirrtl should include(f"node _T_3 = intrinsic(circt_ltl_intersect : UInt<1>, _T, b) $sourceLoc") - chirrtl should include(f"node _T_4 = intrinsic(circt_ltl_intersect : UInt<1>, _T_3, _T_1) $sourceLoc") - chirrtl should include(f"node _T_5 = intrinsic(circt_ltl_intersect : UInt<1>, _T_4, _T_2) $sourceLoc") - chirrtl should include(f"node _T_6 = intrinsic(circt_ltl_clock : UInt<1>, _T, 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 _T_7 = intrinsic(circt_ltl_eventually : UInt<1>, a) $sourceLoc") - chirrtl should include(f"node _T_8 = intrinsic(circt_ltl_and : UInt<1>, _T_7, b) $sourceLoc") - chirrtl should include(f"node _T_9 = intrinsic(circt_ltl_or : UInt<1>, _T_7, b) $sourceLoc") - chirrtl should include(f"node _T_10 = intrinsic(circt_ltl_intersect : UInt<1>, _T_7, 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 ltl_intersect_3 = intrinsic(circt_ltl_intersect : UInt<1>, ltl_eventually, b) $sourceLoc") chirrtl should include( - f"node _T_11 = intrinsic(circt_ltl_intersect : UInt<1>, _T_10, _T_8) $sourceLoc" + f"node ltl_intersect_4 = intrinsic(circt_ltl_intersect : UInt<1>, ltl_intersect_3, ltl_and_1) $sourceLoc" ) - chirrtl should include(f"node _T_12 = intrinsic(circt_ltl_intersect : UInt<1>, _T_11, _T_9) $sourceLoc") - chirrtl should include(f"node _T_13 = intrinsic(circt_ltl_clock : UInt<1>, _T_7, clock) $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 _T_14 = intrinsic(circt_ltl_until : UInt<1>, _T, b) $sourceLoc") - chirrtl should include(f"node _T_15 = intrinsic(circt_ltl_until : UInt<1>, _T_7, 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) @@ -194,20 +194,20 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { val sourceLoc = "@[Foo.scala 1:2]" // Overlapping - chirrtl should include(f"node _T = intrinsic(circt_ltl_implication : UInt<1>, a, b) $sourceLoc") - chirrtl should include(f"node _T_1 = intrinsic(circt_ltl_implication : UInt<1>, a, b) $sourceLoc") + chirrtl should include(f"intrinsic(circt_ltl_implication : UInt<1>, a, b) $sourceLoc") + chirrtl should include(f"intrinsic(circt_ltl_implication : UInt<1>, a, b) $sourceLoc") // Non-overlapping (emitted as `a ## true |-> b`) chirrtl should include( - f"node _T_2 = 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 _T_3 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_2) $sourceLoc") - chirrtl should include(f"node _T_4 = intrinsic(circt_ltl_implication : UInt<1>, _T_3, b) $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 _T_5 = intrinsic(circt_ltl_delay : UInt<1>, UInt<1>(0h1)) $sourceLoc" + f"node ltl_delay_1 = intrinsic(circt_ltl_delay : UInt<1>, UInt<1>(0h1)) $sourceLoc" ) - chirrtl should include(f"node _T_6 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_5) $sourceLoc") - chirrtl should include(f"node _T_7 = intrinsic(circt_ltl_implication : UInt<1>, _T_6, 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 ltl_implication_3 = intrinsic(circt_ltl_implication : UInt<1>, ltl_concat_1, b) $sourceLoc") } it should "compile property implication operation" in { ChiselStage.emitSystemVerilog(new PropImplicationMod) @@ -280,9 +280,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 _T = intrinsic(circt_ltl_clock : UInt<1>, a, clock) $sourceLoc") - chirrtl should include(f"node _T_1 = eq(disable, UInt<1>(0h0)) $sourceLoc") - chirrtl should include(f"intrinsic(circt_verif_$op, _T, _T_1) $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, ltl_clock, _T) $sourceLoc") } } @@ -311,17 +311,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 _T = intrinsic(circt_ltl_clock : UInt<1>, a, c)") - chirrtl should include("intrinsic(circt_verif_assert, _T)") + 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_1 = eq(b, UInt<1>(0h0))") - chirrtl should include("intrinsic(circt_verif_assert, a, _T_1)") + 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 _T_2 = intrinsic(circt_ltl_clock : UInt<1>, a, c)") - chirrtl should include("node _T_3 = eq(b, UInt<1>(0h0))") - chirrtl should include("intrinsic(circt_verif_assert, _T_2, _T_3)") + 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, ltl_clock_1, _T_1)") } class SequenceConvMod extends RawModule { @@ -343,34 +343,34 @@ 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 _T = intrinsic(circt_ltl_concat : UInt<1>, a, b) $sourceLoc") - chirrtl should include(s"intrinsic(circt_verif_assert, _T) $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 _T_1 = intrinsic(circt_ltl_delay : UInt<1>, a) $sourceLoc") - chirrtl should include(s"intrinsic(circt_verif_assert, _T_1) $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 _T_2 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") - chirrtl should include(s"node _T_3 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_2) $sourceLoc") - chirrtl should include(s"intrinsic(circt_verif_assert, _T_3) $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 _T_4 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") - chirrtl should include(s"node _T_5 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_4) $sourceLoc") - chirrtl should include(s"intrinsic(circt_verif_assert, _T_5) $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 _T_6 = 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 _T_7 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_6) $sourceLoc") - chirrtl should include(s"intrinsic(circt_verif_assert, _T_7) $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 _T_8 = intrinsic(circt_ltl_delay : UInt<1>, b) $sourceLoc") - chirrtl should include(s"node _T_9 = intrinsic(circt_ltl_concat : UInt<1>, a, _T_8) $sourceLoc") - chirrtl should include(s"intrinsic(circt_verif_assert, _T_9) $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) @@ -407,21 +407,4 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { assert(assertBlockLoc < delayIntrinsicLoc) assert(assumeblockLoc < implicationIntrinsicLoc) } - - it should "not produce name collisions with clock" in { - class Test extends RawModule { - val io = IO(Input(UInt(8.W))) - - val clockWire = Wire(Clock()) - - withClock(clockWire) { - AssertProperty(Property.eventually(io.orR)) - } - - val clock = IO(Input(Clock())) - clockWire := clock - } - - val chirrtl = ChiselStage.emitCHIRRTL(new Test) - } } From 788e0932077a3655842a662ab9901aa131d0143a Mon Sep 17 00:00:00 2001 From: Jack Koenig Date: Fri, 6 Dec 2024 17:11:14 -0800 Subject: [PATCH 7/7] Run formatting --- src/test/scala/chiselTests/LTLSpec.scala | 56 ++++++++++++++++++------ 1 file changed, 42 insertions(+), 14 deletions(-) diff --git a/src/test/scala/chiselTests/LTLSpec.scala b/src/test/scala/chiselTests/LTLSpec.scala index a46faafcd5..c600e9328d 100644 --- a/src/test/scala/chiselTests/LTLSpec.scala +++ b/src/test/scala/chiselTests/LTLSpec.scala @@ -49,10 +49,16 @@ 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 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 = 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_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") @@ -103,7 +109,9 @@ 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"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_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 ltl_goto_repeat = intrinsic(circt_ltl_goto_repeat : UInt<1>, d) $sourceLoc" @@ -140,23 +148,33 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { val sourceLoc = "@[Foo.scala 1:2]" // Sequences - chirrtl should include(f"node ltl_delay = intrinsic(circt_ltl_delay : UInt<1>, a) $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_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 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 ltl_intersect_3 = intrinsic(circt_ltl_intersect : UInt<1>, ltl_eventually, b) $sourceLoc") + chirrtl should include( + f"node ltl_intersect_3 = intrinsic(circt_ltl_intersect : UInt<1>, ltl_eventually, b) $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_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 @@ -202,12 +220,16 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { 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_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 ltl_concat_1 = intrinsic(circt_ltl_concat : UInt<1>, a, ltl_delay_1) $sourceLoc") - chirrtl should include(f"node ltl_implication_3 = intrinsic(circt_ltl_implication : UInt<1>, ltl_concat_1, b) $sourceLoc") + chirrtl should include( + f"node ltl_implication_3 = intrinsic(circt_ltl_implication : UInt<1>, ltl_concat_1, b) $sourceLoc" + ) } it should "compile property implication operation" in { ChiselStage.emitSystemVerilog(new PropImplicationMod) @@ -347,16 +369,22 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { chirrtl should include(s"intrinsic(circt_verif_assert, ltl_concat) $sourceLoc") // Delay() a - chirrtl should include(s"node ltl_delay = intrinsic(circt_ltl_delay : UInt<1>, a) $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 ltl_delay_1 = intrinsic(circt_ltl_delay : UInt<1>, b) $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 ltl_delay_2 = intrinsic(circt_ltl_delay : UInt<1>, b) $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")