circt
circt copied to clipboard
[FIRRTL] circt_intrinsic_ifelsefatal missed optimization opportunity
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".