[FIRRTL][HW] Improved Optimizations for Observability

[seldridge]

Preface: this is a heavily Chisel-focused example, but everything about it has to do with CIRCT and its optimizations...

There's a common pattern in DV-focused Chisel where a DV engineer wants to be able to observe a signal. Previously, the only tool available was dontTouch. We then provided probes. However, in the example that follows I'll demonstrate that this hasn't, yet, lived up to its promise of being more flexible that dontTouch in certain situations. Finally, certain patterns leave seeming dead code around even if no observability is added.

Consider the following:

//> using repository https://central.sonatype.com/repository/maven-snapshots
//> using scala 2.13.18
//> using dep org.chipsalliance::chisel:7.6.0
//> using plugin org.chipsalliance:::chisel-plugin:7.6.0
//> using options -unchecked -deprecation -language:reflectiveCalls -feature -Xcheckinit
//> using options -Xfatal-warnings -Ywarn-dead-code -Ywarn-unused -Ymacro-annotations

import chisel3._
import chisel3.experimental.{BaseModule, dedupGroup}
import chisel3.ltl.AssertProperty
import chisel3.ltl.Sequence.BoolSequence
import chisel3.probe.{RWProbe, RWProbeValue, define}
import circt.stage.ChiselStage

trait Common { this: BaseModule =>
  val a, b = IO(Input(Bool()))

  val full = a ^ b

  layer.block(layers.Verification) {
    layer.elideBlocks {
      AssertProperty(full |-> !full)
    }
  }
}

/** Bar is unoptimizable as it uses a `dontTouch`. */
class Bar extends Module with Common {
  dontTouch(full)
}

/** Baz has more flexibility as this is a RWProbe.  However, this currently
  * behaves the same as `Bar`.
  *
  * Note: this has no _user_ of the RWProbe meaning that this should be
  * optimized away.  More advanced examples would have a user of the RWProbe.
  */
class Baz extends Module with Common {
  val full_probe = IO(RWProbe(Bool(), layers.Verification))
  define(full_probe, RWProbeValue(full))
}

/** This is the basic module without any observability.  This can be further
  * optimized via automated inlining.
  */
class Qux extends Module with Common

class Foo extends Module {
  private val bar = Module(new Bar)
  private val baz = Module(new Baz)
  private val qux = Module(new Qux)
  bar.a :<= true.B
  bar.b :<= true.B
  baz.a :<= true.B
  baz.b :<= true.B
  qux.a :<= true.B
  qux.b :<= true.B
  dedupGroup(bar, "Bar")
  dedupGroup(baz, "Baz")
  dedupGroup(qux, "Qux")
}

object Main extends App {
  println(
    ChiselStage.emitSystemVerilog(
      gen = new Foo,
      firtoolOpts = Array(
        "-disable-all-randomization",
        "-strip-debug-info",
        "-disable-layers=Verification.Assert,Verification.Assume,Verification.Cover"
      )
    )
  )
}

which compiles to the following Verilog:

// Generated by CIRCT firtool-1.138.0
module Bar(
  input clock,
        reset
);

  wire full = 1'h0;
  wire full_0 = full;
endmodule

module Baz(
  input clock,
        reset
);

  wire full = 1'h0;
  wire full_0 = full;
endmodule

module Qux(
  input clock,
        reset
);

endmodule

module Foo(
  input clock,
        reset
);

  Bar bar (
    .clock (clock),
    .reset (reset)
  );
  Baz baz (
    .clock (clock),
    .reset (reset)
  );
  Qux qux (
    .clock (clock),
    .reset (reset)
  );
endmodule


// ----- 8< ----- FILE "verification/Bar_Verification.sv" ----- 8< -----

// Generated by CIRCT firtool-1.138.0
module Bar_Verification();
  reg  hasBeenResetReg;
  initial
    hasBeenResetReg = 1'bx;
  always @(posedge Bar.clock) begin
    if (Bar.reset)
      hasBeenResetReg <= 1'h1;
  end // always @(posedge)
  wire _GEN = ~(hasBeenResetReg === 1'h1 & Bar.reset === 1'h0);
  assert property (@(posedge Bar.clock) disable iff (_GEN) Bar.full_0 |-> ~Bar.full_0);
endmodule


// ----- 8< ----- FILE "verification/layers-Bar-Verification.sv" ----- 8< -----

// Generated by CIRCT firtool-1.138.0
`ifndef layers_Bar_Verification
  `define layers_Bar_Verification
  bind Bar Bar_Verification verification ();
`endif // not def layers_Bar_Verification

// ----- 8< ----- FILE "verification/Baz_Verification.sv" ----- 8< -----

// Generated by CIRCT firtool-1.138.0
module Baz_Verification();
  reg  hasBeenResetReg;
  initial
    hasBeenResetReg = 1'bx;
  always @(posedge Baz.clock) begin
    if (Baz.reset)
      hasBeenResetReg <= 1'h1;
  end // always @(posedge)
  wire _GEN = ~(hasBeenResetReg === 1'h1 & Baz.reset === 1'h0);
  assert property (@(posedge Baz.clock) disable iff (_GEN) Baz.full_0 |-> ~Baz.full_0);
endmodule


// ----- 8< ----- FILE "verification/layers-Baz-Verification.sv" ----- 8< -----

// Generated by CIRCT firtool-1.138.0
`ifndef layers_Baz_Verification
  `define layers_Baz_Verification
  bind Baz Baz_Verification verification ();
`endif // not def layers_Baz_Verification

// ----- 8< ----- FILE "verification/Qux_Verification.sv" ----- 8< -----

// Generated by CIRCT firtool-1.138.0
module Qux_Verification();
  reg  hasBeenResetReg;
  initial
    hasBeenResetReg = 1'bx;
  always @(posedge Qux.clock) begin
    if (Qux.reset)
      hasBeenResetReg <= 1'h1;
  end // always @(posedge)
  wire _GEN = ~(hasBeenResetReg === 1'h1 & Qux.reset === 1'h0);
  assert property (@(posedge Qux.clock) disable iff (_GEN) 1'h1);
endmodule


// ----- 8< ----- FILE "verification/layers-Qux-Verification.sv" ----- 8< -----

// Generated by CIRCT firtool-1.138.0
`ifndef layers_Qux_Verification
  `define layers_Qux_Verification
  bind Qux Qux_Verification verification ();
`endif // not def layers_Qux_Verification

// ----- 8< ----- FILE "verification/layers-Foo-Verification.sv" ----- 8< -----

// Generated by CIRCT firtool-1.138.0
`ifndef layers_Foo_Verification
  `define layers_Foo_Verification
  `include "layers-Bar-Verification.sv"
  `include "layers-Baz-Verification.sv"
  `include "layers-Qux-Verification.sv"
`endif // not def layers_Foo_Verification

There's three modules here of interest:

1. Bar which uses a dontTouch to make a signal observable. This is, expectedly, very unoptimized.
2. Baz which uses a RWProbe to make a signal observable. This is an extremely strong observable guarantee. However, this behaves exactly the same as (1).
3. Qux which drops all observability, but due to the layer structure, results in a dead module in the final output.

Okay, this issue is essentially a collection of challenge problems:

• How to better optimize Baz? Can the RWProbe be moved around? Is there a cost metric (really more just "quality" cost) where input-only modules are penalized or modules without much in them are penalized in favor of moving things around?
• How to better optimize Qux? Can we turn on input-only module inlining like has been proposed for the HW Dialect ([Firtool] Add FlattenModules pass with command-line options #9285)? Since bind modules are essentially free, can we more aggressively move bind instantiations around if it results in fewer ports? (Basically a cost metric that says "fewer ports are better".)
• In all of Bar, Baz, and Qux the only user of the module inputs clock and reset wind up being binds. While input probes cannot sanely exist, this may motivate relocating the bind into Bar up one level in the hierarchy.

[preechapon250]

Duplicate of #9383

[preechapon250]

#9385

[preechapon250]

#9390

[preechapon250]

Preface: this is a heavily Chisel-focused example, but everything about it has to do with CIRCT and its optimizations...

There's a common pattern in DV-focused Chisel where a DV engineer wants to be able to observe a signal. Previously, the only tool available was dontTouch. We then provided probes. However, in the example that follows I'll demonstrate that this hasn't, yet, lived up to its promise of being more flexible that dontTouch in certain situations. Finally, certain patterns leave seeming dead code around even if no observability is added.

Consider the following:

//> using repository https://central.sonatype.com/repository/maven-snapshots
//> using scala 2.13.18
//> using dep org.chipsalliance::chisel:7.6.0
//> using plugin org.chipsalliance:::chisel-plugin:7.6.0
//> using options -unchecked -deprecation -language:reflectiveCalls -feature -Xcheckinit
//> using options -Xfatal-warnings -Ywarn-dead-code -Ywarn-unused -Ymacro-annotations

import chisel3._
import chisel3.experimental.{BaseModule, dedupGroup}
import chisel3.ltl.AssertProperty
import chisel3.ltl.Sequence.BoolSequence
import chisel3.probe.{RWProbe, RWProbeValue, define}
import circt.stage.ChiselStage

trait Common { this: BaseModule =>
val a, b = IO(Input(Bool()))

val full = a ^ b

layer.block(layers.Verification) {
layer.elideBlocks {
AssertProperty(full |-> !full)
}
}
}

/** Bar is unoptimizable as it uses a dontTouch. */
class Bar extends Module with Common {
dontTouch(full)
}

/** Baz has more flexibility as this is a RWProbe. However, this currently

• behaves the same as Bar.
• Note: this has no user of the RWProbe meaning that this should be
• optimized away. More advanced examples would have a user of the RWProbe.
  */
  class Baz extends Module with Common {
  val full_probe = IO(RWProbe(Bool(), layers.Verification))
  define(full_probe, RWProbeValue(full))
  }

/** This is the basic module without any observability. This can be further

• optimized via automated inlining.
  */
  class Qux extends Module with Common

class Foo extends Module {
private val bar = Module(new Bar)
private val baz = Module(new Baz)
private val qux = Module(new Qux)
bar.a :<= true.B
bar.b :<= true.B
baz.a :<= true.B
baz.b :<= true.B
qux.a :<= true.B
qux.b :<= true.B
dedupGroup(bar, "Bar")
dedupGroup(baz, "Baz")
dedupGroup(qux, "Qux")
}

object Main extends App {
println(
ChiselStage.emitSystemVerilog(
gen = new Foo,
firtoolOpts = Array(
"-disable-all-randomization",
"-strip-debug-info",
"-disable-layers=Verification.Assert,Verification.Assume,Verification.Cover"
)
)
)
}
which compiles to the following Verilog:

// Generated by CIRCT firtool-1.138.0
module Bar(
input clock,
reset
);

wire full = 1'h0;
wire full_0 = full;
endmodule

module Baz(
input clock,
reset
);

wire full = 1'h0;
wire full_0 = full;
endmodule

module Qux(
input clock,
reset
);

endmodule

module Foo(
input clock,
reset
);

Bar bar (
.clock (clock),
.reset (reset)
);
Baz baz (
.clock (clock),
.reset (reset)
);
Qux qux (
.clock (clock),
.reset (reset)
);
endmodule

// ----- 8< ----- FILE "verification/Bar_Verification.sv" ----- 8< -----

// Generated by CIRCT firtool-1.138.0
module Bar_Verification();
reg hasBeenResetReg;
initial
hasBeenResetReg = 1'bx;
always @(posedge Bar.clock) begin
if (Bar.reset)
hasBeenResetReg <= 1'h1;
end // always @(posedge)
wire _GEN = ~(hasBeenResetReg === 1'h1 & Bar.reset === 1'h0);
assert property (@(posedge Bar.clock) disable iff (_GEN) Bar.full_0 |-> ~Bar.full_0);
endmodule

// ----- 8< ----- FILE "verification/layers-Bar-Verification.sv" ----- 8< -----

// Generated by CIRCT firtool-1.138.0
ifndef layers_Bar_Verification define layers_Bar_Verification
bind Bar Bar_Verification verification ();
`endif // not def layers_Bar_Verification

// ----- 8< ----- FILE "verification/Baz_Verification.sv" ----- 8< -----

// Generated by CIRCT firtool-1.138.0
module Baz_Verification();
reg hasBeenResetReg;
initial
hasBeenResetReg = 1'bx;
always @(posedge Baz.clock) begin
if (Baz.reset)
hasBeenResetReg <= 1'h1;
end // always @(posedge)
wire _GEN = ~(hasBeenResetReg === 1'h1 & Baz.reset === 1'h0);
assert property (@(posedge Baz.clock) disable iff (_GEN) Baz.full_0 |-> ~Baz.full_0);
endmodule

// ----- 8< ----- FILE "verification/layers-Baz-Verification.sv" ----- 8< -----

// Generated by CIRCT firtool-1.138.0
ifndef layers_Baz_Verification define layers_Baz_Verification
bind Baz Baz_Verification verification ();
`endif // not def layers_Baz_Verification

// ----- 8< ----- FILE "verification/Qux_Verification.sv" ----- 8< -----

// Generated by CIRCT firtool-1.138.0
module Qux_Verification();
reg hasBeenResetReg;
initial
hasBeenResetReg = 1'bx;
always @(posedge Qux.clock) begin
if (Qux.reset)
hasBeenResetReg <= 1'h1;
end // always @(posedge)
wire _GEN = ~(hasBeenResetReg === 1'h1 & Qux.reset === 1'h0);
assert property (@(posedge Qux.clock) disable iff (_GEN) 1'h1);
endmodule

// ----- 8< ----- FILE "verification/layers-Qux-Verification.sv" ----- 8< -----

// Generated by CIRCT firtool-1.138.0
ifndef layers_Qux_Verification define layers_Qux_Verification
bind Qux Qux_Verification verification ();
`endif // not def layers_Qux_Verification

// ----- 8< ----- FILE "verification/layers-Foo-Verification.sv" ----- 8< -----

// Generated by CIRCT firtool-1.138.0
ifndef layers_Foo_Verification define layers_Foo_Verification
include "layers-Bar-Verification.sv" include "layers-Baz-Verification.sv"
include "layers-Qux-Verification.sv" endif // not def layers_Foo_Verification
There's three modules here of interest:

1. Bar which uses a dontTouch to make a signal observable. This is, expectedly, very unoptimized.
2. Baz which uses a RWProbe to make a signal observable. This is an extremely strong observable guarantee. However, this behaves exactly the same as (1).
3. Qux which drops all observability, but due to the layer structure, results in a dead module in the final output.

Okay, this issue is essentially a collection of challenge problems:

• How to better optimize Baz? Can the RWProbe be moved around? Is there a cost metric (really more just "quality" cost) where input-only modules are penalized or modules without much in them are penalized in favor of moving things around?[ ] How to better optimize Qux? Can we turn on input-only module inlining like has been proposed for the HW Dialect ([Firtool] Add FlattenModules pass with command-line options #9285)? Since bind modules are essentially free, can we more aggressively move bind instantiations around if it results in fewer ports? (Basically a cost metric that says "fewer ports are better".)[ ] In all of Bar, Baz, and Qux the only user of the module inputs clock and reset wind up being binds. While input probes cannot sanely exist, this may motivate relocating the bind into Bar up one level in the hierarchy.

[dtzSiFive]

• How to better optimize Baz? Can the RWProbe be moved around? Is there a cost metric (really more just "quality" cost) where input-only modules are penalized or modules without much in them are penalized in favor of moving things around?

No need to move it, we just need to properly DCE unused RWProbe's. Today the pipeline ordering means we don't know its unused until IMDCE, and we don't run InnerSymDCE to remove the symbol afterwards once its dead. Canonicalizers would drop the trivially unused full after.

Forceable had better optimizing-away properties, but is at odds with wanting to RWProbe a portion of an aggregate not only the entire declaration. It was discussed at the time that this was a down-side, but the idea that we would have many unused RWProbe's floating around (and folks grumpy they weren't optimized away + through) seemed minor compared to the benefits.

As for moving it, that's interesting as usual when you suggest it :). Where might the RWProbe'd signal be moved that would help here?