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

ERROR: Assert `GetSize(subexpr) == 1' failed in backends/smt2/smt2.cc:410. #2577

Closed
rroohhh opened this issue Feb 6, 2021 · 2 comments · Fixed by #3797
Closed

ERROR: Assert `GetSize(subexpr) == 1' failed in backends/smt2/smt2.cc:410. #2577

rroohhh opened this issue Feb 6, 2021 · 2 comments · Fixed by #3797
Labels

Comments

@rroohhh
Copy link

rroohhh commented Feb 6, 2021

When running the following yosys script

read_ilang design.il
dffunmap
stat
write_smt2 -wires design_smt2.smt2

I get the following assertion error:

ERROR: Assert `GetSize(subexpr) == 1' failed in backends/smt2/smt2.cc:410. 

I minimized my testcase to the following using bugpoint (and a manual call of opt after bugpoint was done)

# Generated by Yosys 0.9+3755 (git sha1 UNKNOWN, g++ 7.5.0 -fPIC -Os)
autoidx 3073
attribute \keep 1
attribute \nmigen.hierarchy "top.dut.last_fifo.fifo"
attribute \generator "nMigen"
module \fifo
  attribute $bugpoint 1
  wire width 3 output 1 $auto$bugpoint.cc:253:simplify_something$306
  cell $mem \storage
    parameter \ABITS 0
    parameter \INIT 3'000
    parameter \MEMID "\\storage"
    parameter \OFFSET 0
    parameter \RD_CLK_ENABLE 1'0
    parameter \RD_CLK_POLARITY 1'1
    parameter \RD_PORTS 1
    parameter \RD_TRANSPARENT 1'1
    parameter \SIZE 1
    parameter \WIDTH 3
    parameter \WR_CLK_ENABLE 1'1
    parameter \WR_CLK_POLARITY 1'1
    parameter \WR_PORTS 1
    connect \RD_ADDR { }
    connect \RD_CLK 1'x
    connect \RD_DATA $auto$bugpoint.cc:253:simplify_something$306
    connect \RD_EN 1'x
    connect \WR_ADDR { }
    connect \WR_CLK 1'x
    connect \WR_DATA 3'xxx
    connect \WR_EN 3'xxx
  end
end

Here you can find the full design aswell.

@rroohhh
Copy link
Author

rroohhh commented Feb 6, 2021

(I just checked with version 0.9+3891 aswell and this is still happening)

@rroohhh
Copy link
Author

rroohhh commented Feb 13, 2021

Ok this boils down to to the memory size being 1 and therefore the read / write address having zero bits, and get_bv does not seem to support zero width signals.
I have no deeper understanding of the smt2 backend, so I am not sure where to take this from here...

@mwkmwkmwk mwkmwkmwk added the bug label Mar 1, 2021
ghost pushed a commit to kivikakk/yosys that referenced this issue Jun 7, 2023
Fixes YosysHQ#2577.

I first explored trying to do away with the address line related stuff
entirely here, changing the state from `(Array (_ BitVec <abits>) (_
BitVec <width>))` to just `(_ BitVec <width>)` where abits == 0, drop
the unnecessary `(select ...)` and `(store ...)` etc., but then ran into
trouble where smtbmc interacts with related entities.

It would be neater to use a single-member sort for the key (is there a
"Unit" equivalent?) instead of `(_ BitVec 1)` where we only use the
`#b0` index and not `#b1`, but this does get things working with
minimally invasive changes.

Tested with regular stat, `--stdt`, and `--stbv`; it looks like there's
another latent stbv bug (probably similar to YosysHQ#525) I noted while
testing.  I think it's because we `makebits()` for the "#final" memstate
variant at both lines 1245 and 801.
@ghost ghost mentioned this issue Jun 7, 2023
@jix jix closed this as completed in #3797 Jun 19, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants