Duplicate expressions possibly due to spilled event control expressions in LTL statements

[jackkoenig]

Consider the following:

//> using scala "2.13.12"
//> using repository sonatype-s01:snapshots
//> using dep "org.chipsalliance::chisel::7.0.0-M1+74-3c558514-SNAPSHOT"
//> using plugin "org.chipsalliance:::chisel-plugin::7.0.0-M1+74-3c558514-SNAPSHOT"
//> using options "-unchecked", "-deprecation", "-language:reflectiveCalls", "-feature", "-Xcheckinit", "-Xfatal-warnings", "-Ymacro-annotations"

import chisel3._
import circt.stage.ChiselStage

import chisel3.ltl._
import chisel3.ltl.Sequence._
import chisel3.ltl.Property._

class Foo extends Module {
  val a, b, c, d, e = IO(Input(Bool()))

  AssertProperty(a |=> b ### c)
  CoverProperty(d |-> eventually(e), label = Some("cool_prop"))
}

object Main extends App {
  println(ChiselStage.emitCHIRRTL(new Foo))
  println(
    ChiselStage.emitSystemVerilogFile(
      new Foo,
      firtoolOpts = Array("--strip-debug-info")
    )
  )
}

If you run this with Scala-CLI (see instructions), you get the following Verilog:

// Generated by CIRCT firtool-1.73.0
module Foo(
  input clock,
        reset,
        a,
        b,
        c,
        d,
        e
);

  reg  hasBeenResetReg;
  initial
    hasBeenResetReg = 1'bx;
  always @(posedge clock) begin
    if (reset)
      hasBeenResetReg <= 1'h1;
  end // always @(posedge)
  wire hasBeenReset = hasBeenResetReg === 1'h1 & reset === 1'h0;
  wire disable_0 = ~hasBeenReset;
  assert property (@(posedge clock) disable iff (disable_0) a |=> b ##1 c);
  wire x4 = ~hasBeenReset;
  cool_prop: cover property (@(posedge clock) disable iff (x4) d |-> (s_eventually e));
endmodule

x4 is redundant with disable_0. I assume this is due to a late spilling of the expression, but this seems like a good CSE candidate.