[FIRRTL] duplicated `assert` and `$fatal` with dynamic subaccess

[Tang-Haojin]

Hi, I found that using assert with dynamic subaccess in firrtl would generate two different type but duplicated assert and $fatal in verilog.

Duplicated assert and $fatal with dynamic subaccess

FIRRTL version 3.3.0
circuit our :%[[
  {
    "class":"firrtl.transforms.DedupGroupAnnotation",
    "target":"~our|our",
    "group":"our"
  }
]]
  module our : @[src/main/scala/gcd/GCD.scala 16:7]
    input clock : Clock
    input reset : UInt<1>
    output io : { flip addr : UInt<1>, flip wen : UInt<1>[2]} @[src/main/scala/gcd/GCD.scala 17:14]

    node _T = eq(reset, UInt<1>(0h0)) @[src/main/scala/gcd/GCD.scala 21:9]
    when _T : @[src/main/scala/gcd/GCD.scala 21:9]
      node _T_1 = eq(io.wen[io.addr], UInt<1>(0h0)) @[src/main/scala/gcd/GCD.scala 21:9]
      when _T_1 : @[src/main/scala/gcd/GCD.scala 21:9]
        printf(clock, UInt<1>(0h1), "Assertion failed: gg!\n    at GCD.scala:21 assert(io.wen(io.addr), \"gg!\")\n") : printf @[src/main/scala/gcd/GCD.scala 21:9]
      assert(clock, io.wen[io.addr], UInt<1>(0h1), "") : assert @[src/main/scala/gcd/GCD.scala 21:9]

generates

// Generated by CIRCT firtool-1.62.0
// Standard header to adapt well known macros for prints and assertions.

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

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

module our(	// src/main/scala/gcd/GCD.scala:16:7
  input clock,
        reset,
        io_addr,	// src/main/scala/gcd/GCD.scala:17:14
        io_wen_0,	// src/main/scala/gcd/GCD.scala:17:14
        io_wen_1	// src/main/scala/gcd/GCD.scala:17:14
);

  wire _GEN = io_addr ? io_wen_1 : io_wen_0;	// src/main/scala/gcd/GCD.scala:21:9
  `ifndef SYNTHESIS	// src/main/scala/gcd/GCD.scala:21:9
    always @(posedge clock) begin	// src/main/scala/gcd/GCD.scala:21:9
      if (~reset & ~_GEN) begin	// src/main/scala/gcd/GCD.scala:21:9
        if (`ASSERT_VERBOSE_COND_)	// src/main/scala/gcd/GCD.scala:21:9
          $error("Assertion failed: gg!\n    at GCD.scala:21 assert(io.wen(io.addr), \"gg!\")\n");	// src/main/scala/gcd/GCD.scala:21:9
        if (`STOP_COND_)	// src/main/scala/gcd/GCD.scala:21:9
          $fatal;	// src/main/scala/gcd/GCD.scala:21:9
      end
    end // always @(posedge)
  `endif // not def SYNTHESIS
  always @(posedge clock) begin	// src/main/scala/gcd/GCD.scala:21:9
    if (~reset)	// src/main/scala/gcd/GCD.scala:21:9
      assert__assert: assert(_GEN);	// src/main/scala/gcd/GCD.scala:21:9
  end // always @(posedge)
endmodule

Here firtool not only generates

      if (~reset & ~_GEN) begin	// src/main/scala/gcd/GCD.scala:21:9
        if (`ASSERT_VERBOSE_COND_)	// src/main/scala/gcd/GCD.scala:21:9
          $error("Assertion failed: gg!\n    at GCD.scala:21 assert(io.wen(io.addr), \"gg!\")\n");	// src/main/scala/gcd/GCD.scala:21:9
        if (`STOP_COND_)	// src/main/scala/gcd/GCD.scala:21:9
          $fatal;	// src/main/scala/gcd/GCD.scala:21:9
      end

but also generates

    if (~reset)	// src/main/scala/gcd/GCD.scala:21:9
      assert__assert: assert(_GEN);	// src/main/scala/gcd/GCD.scala:21:9

which is duplicted.

Only one $fatal generated with static subaccess

If we change io.addr to 0, like:

FIRRTL version 3.3.0
circuit our :%[[
  {
    "class":"firrtl.transforms.DedupGroupAnnotation",
    "target":"~our|our",
    "group":"our"
  }
]]
  module our : @[src/main/scala/gcd/GCD.scala 16:7]
    input clock : Clock
    input reset : UInt<1>
    output io : { flip addr : UInt<1>, flip wen : UInt<1>[2]} @[src/main/scala/gcd/GCD.scala 17:14]

    node _T = eq(reset, UInt<1>(0h0)) @[src/main/scala/gcd/GCD.scala 21:9]
    when _T : @[src/main/scala/gcd/GCD.scala 21:9]
      node _T_1 = eq(io.wen[0], UInt<1>(0h0)) @[src/main/scala/gcd/GCD.scala 21:9]
      when _T_1 : @[src/main/scala/gcd/GCD.scala 21:9]
        printf(clock, UInt<1>(0h1), "Assertion failed: gg!\n    at GCD.scala:21 assert(io.wen(0.U), \"gg!\")\n") : printf @[src/main/scala/gcd/GCD.scala 21:9]
      assert(clock, io.wen[0], UInt<1>(0h1), "") : assert @[src/main/scala/gcd/GCD.scala 21:9]

it would generate only one $fatal without duplicated assert:

// Generated by CIRCT firtool-1.62.0
// Standard header to adapt well known macros for prints and assertions.

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

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

module our(	// src/main/scala/gcd/GCD.scala:16:7
  input clock,
        reset,
        io_addr,	// src/main/scala/gcd/GCD.scala:17:14
        io_wen_0,	// src/main/scala/gcd/GCD.scala:17:14
        io_wen_1	// src/main/scala/gcd/GCD.scala:17:14
);

  `ifndef SYNTHESIS	// src/main/scala/gcd/GCD.scala:21:9
    always @(posedge clock) begin	// src/main/scala/gcd/GCD.scala:21:9
      if (~reset & ~io_wen_0) begin	// src/main/scala/gcd/GCD.scala:21:9
        if (`ASSERT_VERBOSE_COND_)	// src/main/scala/gcd/GCD.scala:21:9
          $error("Assertion failed: gg!\n    at GCD.scala:21 assert(io.wen(0.U), \"gg!\")\n");	// src/main/scala/gcd/GCD.scala:21:9
        if (`STOP_COND_)	// src/main/scala/gcd/GCD.scala:21:9
          $fatal;	// src/main/scala/gcd/GCD.scala:21:9
      end
    end // always @(posedge)
  `endif // not def SYNTHESIS
endmodule

Expected behaviour

Dynamic subaccess with assert in firrtl may not generate assert but only generate $fatal and $error in verilog.

[uenoku]

There has been a weird heuristic that eliminates a following assert and it seems it doesn't correctly handles your example https://github.com/llvm/circt/blob/cb19b5458d173d6cfe55b7fa8aee594f2d06d660/lib/Dialect/FIRRTL/Import/FIRParserAsserts.cpp#L313-L329

I guess a better approach for this problem would be not to emit assert in the first place ... not sure the historical reason we emit this though.

[Tang-Haojin]

Thank you for your reply. I know little about the implementation detail of circt, but I found that the assert in Verilog here is a little similar to what we get if we turn on --emit-chisel-asserts-as-sva (but not the same).

Message ID: @.***>

[uenoku]

FYI we are actively working on eliminating pattern matchings (e.g. https://github.com/llvm/circt/pull/6621). Hopefully we can replace printf-encoded assertions with proper ops within weeks.