[FIRRTL] (div) A/A mismatch

[drom]

The following FIRRTL program

circuit top_mod :
  module top_mod :
    input inp_1: UInt<14>
    output tmp4: UInt<14>
    tmp4 <= div(inp_1, inp_1)

Compiled with firtool --lower-to-rtl produces this Verilog:

module top_mod(
  input  [13:0] inp_1,
  output [13:0] tmp4);

  assign tmp4 = inp_1 / inp_1;	// top_mod.fir:3:3, :6:13
endmodule

Compiled with firrtl-1.4.0 produces this Verilog:

module top_mod(
  input  [13:0] inp_1,
  output [13:0] tmp4
);
  assign tmp4 = 14'h1;
endmodule

Yosys (Yosys 0.9+3755 (git sha1 442d19f6, clang 11.0.0 -fPIC -Os)) reports formal mismatch:

ERROR: Found 13 unproven $equiv cells in 'equiv_status -assert'.

[lattner]

I think we're generating the correct code here. The only case I can imagine a mismatch is when the divisor is zero, which is UB. Do you see a problem with the generated verilog?

[drom]

I think this is a good question for the broader discussion https://twitter.com/wavedrom/status/1342932252531945472
Agree that 0/0 is the case.
I would love to hear @cliffordwolf opinion on this issue.

[drom]

Related FIRRTL discussion chipsalliance/firrtl#2029
Do we want FIRTOOL to be (opinion-to-opinion) compatible with FIRRTL and use the LEC tool for a prof?

[seldridge]

@drom: One thing I should have mentioned to you is to also check without optimizations enabled.

If you run with firrtl -X mverilog this will run the "minimum Verilog compiler" which disables optimizations and produces inp_1 / inp_1 as expected.

We should strive for formal equivalence with the unoptimized code and be very careful about deviating there. If we deviate due to optimizations, I think that's fine as long as we understand why. However, I'd expect that we'd implement this same optimization at some point in the RTL dialect.

About the optimization... This optimization looks legal. I.e., inp_1 / inp_1 can be either one or X and the compiler can optimistically choose to collapse the X to one. You could make a similar optimization for something like:

assign bar = `x;
assign foo = sel ? baz : bar;

It's legal to let bar == baz to remove the mux, but formal tools probably won't like this.

[drom]

Is it a bit unfair to disable ALL optimizations just because of this one case?

[lattner]

Do we want FIRTOOL to be (opinion-to-opinion) compatible with FIRRTL and use the LEC tool for a prof?

I'm not sure what you mean here. I don't think we need an option-to-option drop in compatible replacement yet, but that may be useful down the road.

However, are you actually talking about behaviorally compatible? We aren't going to be exactly equivalent in terms of the performed optimizations in all cases.

In this case, I think we should just implement the fold for X/X in CIRCT though!

-Chris

[drom]

Yosys is very good at finding the equivalency of circuits with different levels of optimizations when optimizations can be proven by themselves. I have only 2 questionable cases with FIRRTL fuzzer.

[seldridge]

Clarifying: I'm suggesting we check formal equivalence against the SFC with optimizations off and with optimizations on. If the former differs, then that's highly indicative of a problem. If the latter differs then that's likely indicative of one of the following:

1. CIRCT is missing an optimization/fold.
2. This is an optimization/fold that we don't want to implement and we allow formal equivalence to disagree.

If we implement the optimization/fold, then things should agree again.

I think the questions are then do we fold a / a -> 1 and, if so, in what dialect does this happen.

Edit: I'm in the camp of adding this as a firrtl::DivOp fold.

[drom]

Just implementing A / A -> 1 optimization will not make it equivalent to FIRRTL output.
We need to apply this optimization exactly in those cases, where FIRRTL does it.
No more, no less. Example chipsalliance/firrtl#2029 (comment)

[lattner]

We need to apply this optimization exactly in those cases, where FIRRTL does it.

I'm not interested in that level of bug compatibility with SFC. We should just add the firrtl::DivOp fold in the natural way like @seldridge suggests. Anyone want to take a crack at it? It should be a simple addition of a fold() hook.

[lattner]

This definitely should be done in the RTL dialect, doing it in the firrtl dialect is also a good thing.

[drom]

This definitely should be done in the RTL dialect, doing it in the firrtl dialect is also a good thing.

IMHO A / A -> 1 is wrong optimization in Verilog RTL land. It is FIRRTL specific opinion and should stay in FIRRTL dialect.
It would be not vise to have such an RTL optimization step.

[lattner]

Why?

[drom]

https://twitter.com/wavedrom/status/1342932252531945472

SystemVerilog LRM

[lattner]

Got it makes sense! It would be good to add that as a comment to rtl::div's fold so future versions of us remember that :)

[stephenneuendorffer]

It could be replaced with a compare with zero and a mux, however, which is almost certainly simpler than any divider.

[seldridge]

Trying to generalize this... I think there're two questions:

1. Should Verilog formal equivalence be preserved across optimizations in another, earlier dialect?
2. What is the behavior that we define for rtl::div for a zero denominator?

The following examples try to provide some answers and direct the discussion.

Example 1

1. Foo.rtl is converted to Foo.1.v
2. Foo.rtl is optimized and then converted to Foo.2.v

Is there an expectation that Foo.1.v and Foo.2.v are formally equivalent by the Verilog standard?

Example 2

1. Foo.fir is converted to Foo.1.rtl and then converted to Foo.1.v
2. Foo.fir is optimized, converted to Foo.2.rtl, and then converted to Foo.2.v

Are Foo.1.v and Foo.2.v formally equivalent now?

Discussion

The FIRRTL spec allows for division by zero to be undefined which implies the compiler can optimize around it however it wants. Therefore, breaking formal equivalence in Example 2 seems fine. (This is an example of Verilog semantics not blocking optimization in an earlier dialect.) It would seem odd to curtail a legal FIRRTL optimization because of the backend target.

Is implementing the fold for FIRRTL's div op then non-controversial?

Whether or not formal equivalence is preserved in Example 1 should then depend on the semantics of rtl::div. Does this leave the divide-by-zero case up to the compiler to set or not?

[drom]

Oddly enough, so far, I was able to keep Example 2 equivalency intact on the large volume of randomly generated FIRRTL programs. Except for 5 categories:

1. CIRCT bugs (filing, got fixes very quickly)
2. FIRRTL bugs (filing)
3. Yosys LEC bugs (filing)
4. A / A -> 1 case. which is purely FIRRTL opinion. I was not able to tune Yosys LEC to agree with.
5. Other FIRRTL quirks (was able to tune LEC to agree)

Are we ready to sacrifice all (Example 2) equivalency stories for this one case? Or we should just disable it in FIRRTL?

[seldridge]

I think we're getting hung up on trusting LEC...

The FIRRTL specification states that A/0 is undefined. The compiler is free to exploit this however it wants.

I'm not proposing we sacrifice all equivalency checks. I'm saying that we have one optimization, A/A -> 1, which we understand creates this difference and we waive equivalency checks involving that expression.

I'd be curious what LEC says if we instead optimize A/A -> A != 0. The SV LRM (6.11.2) talks about converting 4-state values to 2-state values. There, x and z become zero. Would that fail formal equivalence even though the LRM seems to allow it?

[lattner]

I'm saying that we have one optimization, A/A -> 1, which we understand creates this difference and we waive equivalency checks involving that expression.

I agree, we should just do this for the firrtl dialect. @seldridge, can you take care of this, and also capture the undefined on zero behavior in the description for firrtl.div in the .td file?

I agree with the upthread comments that we have design space to decide what rtl.div does. Can we bring this to the wednesday open discussion?

[seldridge]

Sure, I can add the fold and the description.

A (bounded) discussion could be good, too!

[lattner]

thx!

[lattner]

This should be addressed by @seldridge 's patch.