chipsalliance / chipsalliance/chisel

`chisel3.cover` drops label in FIRRTL emission

Open
#5,114 1 comment 0 reactions 0 assignees View on GitHub
bug
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

Open the contributing 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.