Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[FIRRTL] (dshr) unsign mismatch #367

Closed
drom opened this issue Dec 26, 2020 · 1 comment
Closed

[FIRRTL] (dshr) unsign mismatch #367

drom opened this issue Dec 26, 2020 · 1 comment
Labels
bug Something isn't working FIRRTL Involving the `firrtl` dialect
Milestone

Comments

@drom
Copy link
Contributor

drom commented Dec 26, 2020

The following FIRRTL program

circuit top_mod :
  module top_mod :
    input inp_4: SInt<6>
    input tmp7: UInt<1>
    output tmp13: UInt<1>
    tmp13 <= dshr(tmp7, asUInt(inp_4))

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

module top_mod(
  input  [5:0] inp_4,
  input        tmp7,
  output       tmp13);

  assign tmp13 = tmp7 >> inp_4[0];	// a_top_mod.fir:2:3, :6:14
endmodule

image

Compiled with firrtl-1.4.0 produces this Verilog:

module top_mod(
  input  [5:0] inp_4,
  input        tmp7,
  output       tmp13
);
  assign tmp13 = tmp7 >> inp_4;
endmodule

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

ERROR: Found 1 unproven $equiv cells in 'equiv_status -assert'.
@drom drom added the FIRRTL Involving the `firrtl` dialect label Dec 26, 2020
lattner added a commit that referenced this issue Dec 26, 2020
We cannot truncate the shift amount because an over large shift amount
should produce all zeros/sign in a dshr.  This merges together and
unifies the code with divide which had similar logic.

Also add verification that the RHS of a shift is unsigned.

This fixes issue #367 and #366.
@lattner
Copy link
Collaborator

lattner commented Dec 26, 2020

Fixed in d2fd8fc, thanks!

@lattner lattner closed this as completed Dec 26, 2020
@drom drom added this to the SiFive-1 milestone Mar 23, 2021
@darthscsi darthscsi added the bug Something isn't working label Apr 7, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working FIRRTL Involving the `firrtl` dialect
Projects
None yet
Development

No branches or pull requests

3 participants