Duplicate expressions possibly due to spilled event control expressions in LTL statements
- Dominant language
- C++
- Stars
- 2.2k
- Forks
- 524
- Avg merge
- 3d 2h
- Merged PRs (30d)
- 46
Description
Consider the following:
```scala
//> 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](https://www.chisel-lang.org/docs/installation#quickstart-with-scala-cli)), you get the following Verilog:
```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.
Contributor guide
No contributing guide indexed for this repository
Research direction
Run the Scala-CLI reproduction and compare the emitted CHIRRTL and SystemVerilog around the two disable expressions. Start by tracing the firtool path that produces disable_0 and x4; done means the redundant expression is eliminated without changing the assertion or cover-property behavior.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- cpp, scala
- Domain
- compilers
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100