chipsalliance / chipsalliance/chisel
`chisel3.cover` drops label in FIRRTL emission
- Dominant language
- Scala
- Stars
- 4.8k
- Forks
- 658
- Avg merge
- 18h 59m
- Merged PRs (30d)
- 14
Description
Consider the following:
``` scala
//> using repository https://central.sonatype.com/repository/maven-snapshots
//> using scala 2.13.18
//> using dep org.chipsalliance::chisel:7.4.0
//> using plugin org.chipsalliance:::chisel-plugin:7.4.0
//> using options -unchecked -deprecation -language:reflectiveCalls -feature -Xcheckinit
//> using options -Xfatal-warnings -Ywarn-dead-code -Ywarn-unused -Ymacro-annotations
import chisel3._
import circt.stage.ChiselStage
class Bar(useProperty: Boolean, name: String) extends Module {
val en = IO(Input(Bool()))
useProperty match {
case true => ltl.CoverProperty(en, name)
case false => cover(en, name)
}
override def desiredName = name
}
class Foo(useProperty: Boolean) extends Module {
val en = IO(Input(Bool()))
Seq("Bar", "Baz").foreach { case name =>
val child = Module(new Bar(useProperty, name))
child.en :<= en
}
}
object Main extends App {
Seq(false, true).foreach { case useProperty =>
println(
ChiselStage.emitCHIRRTL(
gen = new Foo(useProperty)
)
)
println(
ChiselStage.emitSystemVerilog(
gen = new Foo(useProperty),
firtoolOpts = Array("-default-layer-specialization=enable", "-strip-debug-info")
)
)
}
}
```
Just looking at the Verilog output, this will deduplicate the two instances of `Bar` and collapse their covers even though they have different messages/labels. This is not desired. However, if using `chisel3.ltl.CoverProperty`, then this will _not_ deduplicate as the label is preserved:
``` verilog
// Generated by CIRCT firtool-1.137.0
module Bar(
input clock,
reset,
en
);
always @(posedge clock) begin
if (~reset)
cover__cover: cover(en);
end // always @(posedge)
endmodule
module Foo(
input clock,
reset,
en
);
Bar child (
.clock (clock),
.reset (reset),
.en (en)
);
Bar child_1 (
.clock (clock),
.reset (reset),
.en (en)
);
endmodule
```
``` verilog
// Generated by CIRCT firtool-1.137.0
module Bar(
input clock,
reset,
en
);
reg hasBeenResetReg;
initial
hasBeenResetReg = 1'bx;
always @(posedge clock) begin
if (reset)
hasBeenResetReg <= 1'h1;
end // always @(posedge)
wire _GEN = ~(hasBeenResetReg === 1'h1 & reset === 1'h0);
Bar: cover property (@(posedge clock) disable iff (_GEN) en);
endmodule
module Baz(
input clock,
reset,
en
);
reg hasBeenResetReg;
initial
hasBeenResetReg = 1'bx;
always @(posedge clock) begin
if (reset)
hasBeenResetReg <= 1'h1;
end // always @(posedge)
wire _GEN = ~(hasBeenResetReg === 1'h1 & reset === 1'h0);
Baz: cover property (@(posedge clock) disable iff (_GEN) en);
endmodule
module Foo(
input clock,
reset,
en
);
Bar child (
.clock (clock),
.reset (reset),
.en (en)
);
Baz child_1 (
.clock (clock),
.reset (reset),
.en (en)
);
endmodule
```
The root reason for this is that the message for `chisel3.cover` is dropped in the FIRRTL emission:
``` firrtl
FIRRTL version 6.0.0
circuit Foo :
layer Verification, bind, "verification" :
layer Assert, bind, "verification/assert" :
layer Temporal, inline :
layer Assume, bind, "verification/assume" :
layer Temporal, inline :
layer Cover, bind, "verification/cover" :
layer Temporal, inline :
module Bar :
input clock : Clock
input reset : Reset
input en : UInt<1>
skip
layerblock Verification :
layerblock Cover :
node _T = asUInt(reset)
node _T_1 = eq(_T, UInt<1>(0h0))
when _T_1 :
cover(clock, en, UInt<1>(0h1), "") : cover
module Baz :
input clock : Clock
input reset : Reset
input en : UInt<1>
skip
layerblock Verification :
layerblock Cover :
node _T = asUInt(reset)
node _T_1 = eq(_T, UInt<1>(0h0))
when _T_1 :
cover(clock, en, UInt<1>(0h1), "") : cover
public module Foo :
input clock : Clock
input reset : UInt<1>
input en : UInt<1>
inst child of Bar
connect child.clock, clock
connect child.reset, reset
connect child.en, en
inst child_1 of Baz
connect child_1.clock, clock
connect child_1.reset, reset
connect child_1.en, en
```
Contributor guide
Research direction
Start with the chisel3.cover path and compare it with ltl.CoverProperty, using ChiselStage.emitCHIRRTL and emitSystemVerilog from the reproducer. Trace how the cover message or label reaches FIRRTL emission, then verify that distinct labels survive emission and prevent the two Bar instances from being deduplicated incorrectly.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- scala
- Domain
- compilers
- Issue type
- Bug
- Difficulty
- 3/5
- Estimated time
- 1-2 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 45/100