circt icon indicating copy to clipboard operation
circt copied to clipboard

[FIRRTL] circt_intrinsic_ifelsefatal missed optimization opportunity

Open seldridge opened this issue 6 months ago • 1 comments

This was uncovered while trying to move verification statements automatically into layers in Chisel. I'm seeing a missed opportunity for eliminating a circt_chisel_ifelsefatal intrinsic.

Consider the following where the assertion predicate reduces to 0:

FIRRTL version 4.0.0
circuit Foo:
  layer A, bind:
  public module Foo:
    input clock: Clock
    input a: UInt<2>
    output c: UInt<2>

    node b = bits(a, 1, 0)
    layerblock A :
      intrinsic(circt_chisel_ifelsefatal<format = "bar">, clock, eq(a, b), UInt<1>(1))

    ; This user of b is important!
    connect c, b

When compiled firtool Foo.fir this leaves a trivially dead assertion in the design:

// Generated by CIRCT firtool-1.81.1-18-g6aa871500

// Users can define 'STOP_COND' to add an extra gate to stop conditions.
`ifndef STOP_COND_
  `ifdef STOP_COND
    `define STOP_COND_ (`STOP_COND)
  `else  // STOP_COND
    `define STOP_COND_ 1
  `endif // STOP_COND
`endif // not def STOP_COND_

// Users can define 'ASSERT_VERBOSE_COND' to add an extra gate to assert error printing.
`ifndef ASSERT_VERBOSE_COND_
  `ifdef ASSERT_VERBOSE_COND
    `define ASSERT_VERBOSE_COND_ (`ASSERT_VERBOSE_COND)
  `else  // ASSERT_VERBOSE_COND
    `define ASSERT_VERBOSE_COND_ 1
  `endif // ASSERT_VERBOSE_COND
`endif // not def ASSERT_VERBOSE_COND_
module Foo_A(
  input [1:0] a,
              b,
  input       clock
);

  `ifndef SYNTHESIS
    always @(posedge clock) begin
      if (a != b) begin
        if (`ASSERT_VERBOSE_COND_)
          $error("bar");
        if (`STOP_COND_)
          $fatal;
      end
    end // always @(posedge)
  `endif // not def SYNTHESIS
endmodule

module Foo(
  input        clock,
  input  [1:0] a,
  output [1:0] c
);

  assign c = a;
endmodule


// ----- 8< ----- FILE "layers_Foo_A.sv" ----- 8< -----

// Generated by CIRCT firtool-1.81.1-18-g6aa871500
`ifndef layers_Foo_A
`define layers_Foo_A
bind Foo Foo_A a_0 (
  .a     (a),
  .b     (a),
  .clock (clock)
);
`endif // layers_Foo_A

However, if there is nothing to block LayerSink from moving the node b into the layerblock and optimization happens. This can be shown with the slightly modified circuit which removes the user of b:

FIRRTL version 4.0.0
circuit Foo:
  layer A, bind:
  public module Foo:
    input clock: Clock
    input a: UInt<2>
    output c: UInt<2>

    node b = bits(a, 1, 0)
    layerblock A :
      intrinsic(circt_chisel_ifelsefatal<format = "bar">, clock, eq(a, b), UInt<1>(1))

    invalidate c
// Generated by CIRCT firtool-1.81.1-18-g6aa871500
module Foo(
  input        clock,
  input  [1:0] a,
  output [1:0] c
);

  assign c = 2'h0;
endmodule


// ----- 8< ----- FILE "layers_Foo_A.sv" ----- 8< -----

// Generated by CIRCT firtool-1.81.1-18-g6aa871500
`ifndef layers_Foo_A
`define layers_Foo_A
`endif // layers_Foo_A

~I haven't tracked down the issue, yet. I expect it is something to do with optimizations or canonicalizations not working across layerblocks and this then relying on LayerSink to make the optimization available.~

The canonicalizer is responsible for removing this pattern. This runs after LowerLayers. At that point, this analysis is no longer easy to do as it would require doing canonicalization across a module boundary or some notion of "inter module value numbering".

seldridge avatar Aug 19 '24 22:08 seldridge