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.

Sign up for GitHub

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

Fix potential name collision caused by LTL properties #4551

Merged
merged 8 commits into from
Dec 7, 2024
Merged

Fix potential name collision caused by LTL properties #4551

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
e898cf1
reproduce LTL name collision in unit test
tmckay-sifive Dec 5, 2024
1463989
fix test
tmckay-sifive Dec 5, 2024
c644b0b
do not suggest names for LTL intrinsics
tmckay-sifive Dec 5, 2024
77fbf0e
update tests
tmckay-sifive Dec 6, 2024
dcfcf11
Merge branch 'main' into tmckay/ltl-name-collision
tmckay-sifive Dec 6, 2024
71f5810
suggestName, but with ltl_ prefix
tmckay-sifive Dec 6, 2024
5023a5b
update tests
tmckay-sifive Dec 6, 2024
788e093
Run formatting
jackkoenig Dec 7, 2024
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
4 changes: 2 additions & 2 deletions src/main/scala-2/chisel3/util/circt/LTLIntrinsics.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. */
Expand All @@ -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. */
Expand Down
148 changes: 88 additions & 60 deletions src/test/scala/chiselTests/LTLSpec.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<delay = 1, length = 0> : UInt<1>, a) $sourceLoc")
chirrtl should include(f"node delay_1 = intrinsic(circt_ltl_delay<delay = 2, length = 2> : UInt<1>, b) $sourceLoc")
chirrtl should include(f"node delay_2 = intrinsic(circt_ltl_delay<delay = 5> : UInt<1>, c) $sourceLoc")
chirrtl should include(f"node delay_3 = intrinsic(circt_ltl_delay<delay = 1, length = 0> : 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<delay = 0> : 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<delay = 1> : 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<delay = 1, length = 0> : UInt<1>, a) $sourceLoc"
)
chirrtl should include(
f"node ltl_delay_1 = intrinsic(circt_ltl_delay<delay = 2, length = 2> : UInt<1>, b) $sourceLoc"
)
chirrtl should include(f"node ltl_delay_2 = intrinsic(circt_ltl_delay<delay = 5> : UInt<1>, c) $sourceLoc")
chirrtl should include(
f"node ltl_delay_3 = intrinsic(circt_ltl_delay<delay = 1, length = 0> : 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<delay = 0> : 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<delay = 1> : 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)
Expand All @@ -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)
Expand All @@ -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<base = 1, more = 0> : UInt<1>, a) $sourceLoc")
chirrtl should include(f"node repeat_1 = intrinsic(circt_ltl_repeat<base = 2, more = 2> : UInt<1>, b) $sourceLoc")
chirrtl should include(f"node repeat_2 = intrinsic(circt_ltl_repeat<base = 5> : UInt<1>, c) $sourceLoc")
chirrtl should include(f"node ltl_repeat = intrinsic(circt_ltl_repeat<base = 1, more = 0> : UInt<1>, a) $sourceLoc")
chirrtl should include(
f"node ltl_repeat_1 = intrinsic(circt_ltl_repeat<base = 2, more = 2> : UInt<1>, b) $sourceLoc"
)
chirrtl should include(f"node ltl_repeat_2 = intrinsic(circt_ltl_repeat<base = 5> : UInt<1>, c) $sourceLoc")
chirrtl should include(
f"node goto_repeat = intrinsic(circt_ltl_goto_repeat<base = 1, more = 2> : UInt<1>, d) $sourceLoc"
f"node ltl_goto_repeat = intrinsic(circt_ltl_goto_repeat<base = 1, more = 2> : UInt<1>, d) $sourceLoc"
)
chirrtl should include(
f"node non_consecutive_repeat = intrinsic(circt_ltl_non_consecutive_repeat<base = 1, more = 2> : UInt<1>, e) $sourceLoc"
f"node ltl_non_consecutive_repeat = intrinsic(circt_ltl_non_consecutive_repeat<base = 1, more = 2> : UInt<1>, e) $sourceLoc"
)
}
it should "compile sequence repeat operations" in {
Expand Down Expand Up @@ -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<delay = 1, length = 0> : 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<delay = 1, length = 0> : 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)
Expand Down Expand Up @@ -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<delay = 1, length = 0> : UInt<1>, UInt<1>(0h1)) $sourceLoc"
f"node ltl_delay = intrinsic(circt_ltl_delay<delay = 1, length = 0> : 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<delay = 1, length = 0> : 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<delay = 1, length = 0> : 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)
Expand Down Expand Up @@ -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")
}
}

Expand Down Expand Up @@ -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 {
Expand All @@ -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<delay = 1, length = 0> : 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<delay = 1, length = 0> : 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<delay = 1, length = 0> : 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<delay = 1, length = 0> : 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<delay = 2, length = 0> : 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<delay = 2, length = 0> : 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<delay = 42, length = 1295> : UInt<1>, b) $sourceLoc"
s"node ltl_delay_3 = intrinsic(circt_ltl_delay<delay = 42, length = 1295> : 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<delay = 9001> : 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<delay = 9001> : 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)
Expand Down