llvm / llvm/circt

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

Open
#6,930 0 comments 1 reaction 0 assignees View on GitHub
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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.