Warning that Verilog may cause mismatches between simulation and synthesis

[Ramlakshmi3733]

The formal verification tool flags this as a warning (not error). I have attached the MLIR output and a corrected version below.

Warning: Variable(s) is(are) being read asynchronously. This may cause simulation-synthesis mismatches. (Signal: _T_0 Block: testcase_mfc.sv Line: 43) The problem with this description is that the simulation model does not react to changes in reset_data while reset_enable is held high. In Verilog, you can't add _T_0 to the sensitivity list without breaking the model. You must verify that your model does not rely on the fact that during reset, the simulator holds tmp50 steady even though _TMP_50 changes. The synthesized register will be transparent during reset.

Or change the RTL, to have constant driving reset line.

_The FIR file_circuit top_mod :

  module top_mod :
    input clock: Clock
    input reset: UInt<1>
    input arst: AsyncReset
    input inp_i: SInt<170>
    output out_i: SInt<170>
    reg tmp50: SInt<2>, clock with: (reset => (arst, SInt<2>(0)))
    tmp50 <= inp_i
    out_i <= tmp50

**The output that produces the warning (just the relevant section):

 always_ff @(posedge clock or posedge arst**) begin      // testcase.fir:9:5
    if (arst)   // testcase.fir:9:5
      **tmp50 <= _T_0;    // testcase.fir:9:5**
    else        // testcase.fir:9:5
      tmp50 <= _T;      // testcase.fir:10:11
  end // always_ff @(posedge or posedge)

The structure that is read without warnings:

module top_mod(
  input          clock,
  input          reset,
  input          arst,
  input  [169:0] inp_i,
  output [169:0] out_i
);
`ifdef RANDOMIZE_REG_INIT
  reg [31:0] _RAND_0;
`endif // RANDOMIZE_REG_INIT
  reg [1:0] tmp50;
  assign out_i = {{168{tmp50[1]}},tmp50};
  always @(posedge clock or posedge arst) begin
    if (arst) begin
      **tmp50 <= 2'sh0;**
    end else begin
      tmp50 <= inp_i[1:0];
    end
  end

[seldridge]

This is an interesting one.

Fundamentally, the async reset initial value should be a constant. Otherwise the init could have setup/hold time violations and then asserting the async reset is a dice roll.

The SFC, to avoid this, actually mandates that the async reset init must be a constant and does limited constant propagation to try to enforce this. It will error if you use a non-constant value here.

The MFC output isn't wrong---the reset init is a constant. However, it needs copy/constant propagation to generate Verilog where this is obvious to the formal tool. Solving this with the public/private proposal and aggressive, medieval application of copy/constant propagation on anything private should fix this. This is another situation where "legal" Verilog requires limited optimizations because it's a wacky language.

Later we can add an error if an init isn't a constant and avoid actually bad Verilog into the downstream tools. (We can error before ever generating code that the formal tool will warn on.)

[fabianschuiki]

For reference, lowering the example FIRRTL input to the RTL dialect with firtool -lower-to-rtl yields (abbreviated):

rtl.module @top_mod(%clock: i1, %reset: i1, %arst: i1, %inp_i: i170) -> (%out_i: i170) {
  %c0_i2 = rtl.constant 0 : i2
  %true = rtl.constant true
  %tmp50 = sv.reg  : !rtl.inout<i2>
  sv.alwaysff(posedge %clock)  {
    sv.passign %tmp50, %0 : i2
  }(asyncreset : posedge %arst)  {
    sv.passign %tmp50, %c0_i2 : i2  // <--- interesting here
  }
  %0 = comb.extract %inp_i from 0 : (i170) -> i2
  %1 = sv.read_inout %tmp50 : !rtl.inout<i2>
  %2 = comb.sext %1 : (i2) -> i170
  rtl.output %2 : i170
}

The interesting portion is sv.passign %tmp50, %c0_i2 in the reset branch of the flip-flop, which actually directly has the constant operand %c0_i2. Constant folding should guarantee that if the reset value is a constant then the reset SSA value should be a rtl.constant operation. So this could be an easy thing to pick up in ExportVerilog.

[darthscsi]

The exportverilog changes caused this. expressions in different blocks are not inlined. The constant needs to be sunk into to block it's used in or constants need to be a special case in emission.

[darthscsi]

If the constants generated localparams does this still cause problems?

[fabianschuiki]

If the constants generated localparams does this still cause problems?

I think that would fix the issue in a pretty elegant way!

[fabianschuiki]

Localparams would also help ensure that we didn't break SV's darn longest static prefix rules on lvalues with stuff like constant array indexes. That's cool!

[darthscsi]

That would be a better way to make constant pools, but still not ideal. This test case should change:

diff --git a/test/ExportVerilog/rtl-dialect.mlir b/test/ExportVerilog/rtl-dialect.mlir
index e56ac573..4b78f405 100644
--- a/test/ExportVerilog/rtl-dialect.mlir
+++ b/test/ExportVerilog/rtl-dialect.mlir
@@ -599,11 +599,10 @@ rtl.module @longvariadic(%a: i8) -> (%b: i8) {
 // CHECK-EMPTY:
 // CHECK-NEXT:   reg memory_r_en_pipe[0:0];
 // CHECK-EMPTY:
-// CHECK-NEXT:   wire _T = 1'h0;
 // CHECK-NEXT:   always_ff @(posedge clock)
-// CHECK-NEXT:     memory_r_en_pipe[_T] <= _T;
+// CHECK-NEXT:     memory_r_en_pipe[1'h0] <= 1'h0;
 // CHECK-NEXT:   initial
-// CHECK-NEXT:     memory_r_en_pipe[_T] = _T;
+// CHECK-NEXT:     memory_r_en_pipe[1'h0] = 1'h0;
 // CHECK-NEXT: endmodule
 rtl.module @ArrayLHS(%clock: i1) -> () {
   %false = rtl.constant false

[darthscsi]

At minimum assigns need to not spill their rhs if they are constants, even if they are long constants.

[darthscsi]

localparams might be a hack to allow spilling constants without breaking resets. @Ramlakshmi3733 reports that putting the constants in localparams makes the tools happy.

[fabianschuiki]

Now the question is do we prefer localparams or force-inlining constants during emission where it's necessary 😃 ?

[darthscsi]

inlining where possible, localparam makes a globally visible name.

[lattner]

There are really two things going on here:

1) we need to sink constants and other expressions so we have fewer unnecessary cross block expressions emitted out of line (this affects simulator performance and readability of verilog). This should be just "nice to have" right now, and should be a change to the rtlcleanup pass.

2) We need have guaranteed "constantness" for constants apparently, even if they get assigned to temporaries whatever reason. I agree that emitting them as localparams is a good way to go, I'll take a look at the patch!