Fix potential name collision caused by LTL properties

[tmckay-sifive]

Contributor Checklist

• Did you add Scaladoc to every public function/method?
• Did you add at least one test demonstrating the PR?
• Did you delete any extraneous printlns/debugging code?
• Did you specify the type of improvement?
• Did you add appropriate documentation in docs/src?
• Did you request a desired merge strategy?
• Did you add text to be included in the Release Notes for this change?

Type of Improvement

• Bugfix

Desired Merge Strategy

• Squash: The PR will be squashed and merged (choose this if you have no preference).

Release Notes

Some nodes created by LTL properties had suggestName called on them, potentially leading to name collisions with user code.

Reviewer Checklist (only modified by reviewer)

• Did you add the appropriate labels? (Select the most appropriate one based on the "Type of Improvement")
• Did you mark the proper milestone (Bug fix: 3.6.x, 5.x, or 6.x depending on impact, API modification or big change: 7.0)?
• Did you review?
• Did you check whether all relevant Contributor checkboxes have been checked?
• Did you do one of the following when ready to merge:
  • Squash: You/ the contributor Enable auto-merge (squash), clean up the commit message, and label with Please Merge.
  • Merge: Ensure that contributor has cleaned up their commit history, then merge with Create a merge commit.

[tmckay-sifive]

I added this test to reproduce the bug. It seems like a silly test now that there is no possibility for a name collision. However, it also felt wrong to delete a test, even if it is trivially passing.

Should we keep it?

[jackkoenig]

We should keep it, but possibly extend it to check the names that come out

[tmckay-sifive]

Sounds good, will add the extended test shortly

[jackkoenig]

Removing these suggestNames makes the naming quality a lot worse (as evidenced by the updates to the tests) so I think we want to find a different way to solve this. Can you explain a bit more about what is problematic about the collision you were seeing? Was something failing?

[tmckay-sifive]

The issue I was encountering was that the properties and sequences in the LTL library create nodes for the intrinsics. These nodes are named the same as the intrinsic kind.

This can result in confusing name collisions, especially for intrinsics with names that are likely to show up in user code e.g. clock or delay.

This is a case I constructed to produce the error.

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
}

[error] (unknown): Attempted to name Test.clock: IO[Clock] with a duplicated name 'clock'. Use suggestName to seed a unique name
[error] There were 1 error(s) during hardware elaboration.

The assert property creates a node named clock, but it is not obvious that it would do so. Then, when attempting to create another node clock in user code, Chisel complains about the name collision.

More broadly I think the issue is that calling suggestName inside Chisel can make it very tough to determine why name collisions are happening.

[jackkoenig]

I see, so the issue is that the port comes after the property. I do think the real solution is that Chisel needs to track where the previously named thing was so we can point to it. But I see your point that this was hard to debug and we certainly want to reduce the odds that this happens to users.

How about something a bit lighter touch--keep the .suggestName, but use names that are less likely to collide with signals named by users, e.g. suggest ltl_clock instead of clock?

[jackkoenig]

LGTM!