Make LTL properties use Clock and Disable by default

[jackkoenig]

Built on top of #3497 so currently PR-ed against it, will be rebased on main once #3497 is merged.

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

• API modification

Desired Merge Strategy

• Squash

Release Notes

Properties in package chisel3.ltl will now be clocked and disabled by default (if there is an implicit clock and disable). Default disable is not hasBeenReset of the current implicit reset (if one exists). The clock and disable can be removed by setting them to None via withClock, withReset, and withDisable APIs.

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.5.x, 3.6.x, or 5.x depending on impact, API modification or big change: 6.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.

[jackkoenig]

I have no idea where this x2 comes from and at this point I'm too afraid to ask

Jokes aside, I'm looking into it.

[jackkoenig]

Looks like a product of the desugaring of the function taking default arguments:

class Example extends RawModule {
  val a, b = IO(Input(Bool()))
  val c = IO(Input(Clock()))
  AssertProperty(a, disable = Some(b.asDisable))
}

By the time the Chisel plugin sees it, it has be lowered to:

class Example extends chisel3.RawModule {
  def <init>(): Example = {
    Example.super.<init>();
    ()
  };
  private[this] val a: chisel3.Bool = Example.this.IO[chisel3.Bool](chisel3.Input.apply[chisel3.Bool](chisel3.`package`.Bool.apply()))((chisel3.experimental.SourceLine.apply("src/main/scala/Jack.scala", 9, 16): chisel3.experimental.SourceInfo));
  <stable> <accessor> def a: chisel3.Bool = Example.this.a;
  private[this] val b: chisel3.Bool = Example.this.IO[chisel3.Bool](chisel3.Input.apply[chisel3.Bool](chisel3.`package`.Bool.apply()))((chisel3.experimental.SourceLine.apply("src/main/scala/Jack.scala", 9, 16): chisel3.experimental.SourceInfo));
  <stable> <accessor> def b: chisel3.Bool = Example.this.b;
  private[this] val c: chisel3.Clock = Example.this.IO[chisel3.Clock](chisel3.Input.apply[chisel3.Clock](chisel3.Clock.apply()))((chisel3.experimental.SourceLine.apply("src/main/scala/Jack.scala", 10, 13): chisel3.experimental.SourceInfo));
  <stable> <accessor> def c: chisel3.Clock = Example.this.c;
  {
    <artifact> val x$1: chisel3.ltl.Sequence.BoolSequence = chisel3.ltl.Sequence.BoolSequence(Example.this.a);
    <artifact> val x$2: Some[chisel3.Disable] @scala.reflect.internal.annotations.uncheckedBounds = scala.Some.apply[chisel3.Disable](Example.this.b.do_asDisable(scala.Predef.implicitly[chisel3.experimental.SourceInfo]((chisel3.experimental.SourceLine.apply("src/main/scala/Jack.scala", 12, 38): chisel3.experimental.SourceInfo))));
    <artifact> val x$3: Option[chisel3.Clock] @scala.reflect.internal.annotations.uncheckedBounds = chisel3.ltl.AssertProperty.apply$default$2;
    <artifact> val x$4: Option[String] @scala.reflect.internal.annotations.uncheckedBounds = chisel3.ltl.AssertProperty.apply$default$4;
    chisel3.ltl.AssertProperty.apply(x$1, x$3, x$2, x$4)
  }
}

I think there's an interesting question about having the plugin detect these synthetic names (I think that's what the <artifact> decorator is indicating) and ignore them. That could have wide-ranging impacts on emitted FIRRTL and thus Verilog though so I think it should be done completely separately from this PR.

[jackkoenig]

If you change the input Chisel to:

class Example extends RawModule {
  val a, b = IO(Input(Bool()))
  val c = IO(Input(Clock()))
  AssertProperty(a, None, Some(b.asDisable), None)
}

Then these artifact vals don't exist and the name of the node is _T.

FWIW I'd like to get rid of the need for this node (the pointless bit-extract on an already 1-bit UInt), but that also is a separate PR.

[seldridge]

This is surprising.

This is the type of thing that FileCheck would help with. (The test really shouldn't care about the change even if we should be tracking this with an improvement to the naming plugin.)

[sequencer]

This solved me a long time question...
Thanks Jack...
You might need to take a look at your diplomacy framework, IIRC, BundleBridge has the same issue, and I didn't spend time on it, but directly suggest name,

[seldridge]

LGTM

Great job factoring these PRs. It's nice to see this one as such a minor change built on the others.

[seldridge]

This is surprising.

This is the type of thing that FileCheck would help with. (The test really shouldn't care about the change even if we should be tracking this with an improvement to the naming plugin.)

[sequencer]

This solved me a long time question...
Thanks Jack...
You might need to take a look at your diplomacy framework, IIRC, BundleBridge has the same issue, and I didn't spend time on it, but directly suggest name,