Skip to content

chisel3.cover drops label in FIRRTL emission #5114

@seldridge

Description

@seldridge

Consider the following:

//> 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:

// 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
// 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 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 

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions