Skip to content

Commit

Permalink
Fix potential name collision caused by LTL properties (#4551)
Browse files Browse the repository at this point in the history
  • Loading branch information
tmckay-sifive authored Dec 7, 2024
1 parent b5384d9 commit 5871a65
Show file tree
Hide file tree
Showing 2 changed files with 90 additions and 62 deletions.
4 changes: 2 additions & 2 deletions src/main/scala-2/chisel3/util/circt/LTLIntrinsics.scala
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
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

0 comments on commit 5871a65

Please sign in to comment.