-
Notifications
You must be signed in to change notification settings - Fork 63
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
Avoid breaking up bitvectors in Verilog output #1369
Conversation
src/SAWScript/Prover/Exporter.hs
Outdated
do w <- W4Sim.bvPackBE sym bs | ||
case w of | ||
W4Sim.DBV bv -> return [Some bv] | ||
W4Sim.ZBV -> fail "write_verilog: bitvectors of size zero unsupported" |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think you can probably just return []
here? I think it's better to avoid failure cases if we can.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess the consideration is whether this function should be generic (which it otherwise mostly is) or should be specific to Verilog generation. Verilog doesn't allow vectors of size zero, so in the latter case this is the result we want. At the same time, I also like to avoid failure cases whenever possible... And I'd prefer to do something other than fail
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looking at this some more, I think this will fail on empty vectors at any type, which you probably also don't want.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh, and now that I look further I think your previous suggestion was right. Returning an empty list for a zero-size bit vector will result in no value on the Verilog side, not an empty value, so it'll be fine. I'll update it so that any zero-size vector will go through okay.
Flattening a value containing an empty bit vector is now valid. It simply won't appear in the list of output values.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good to me.
Previously, when translating What4 to Verilog, all
VVector
values were translated into multiple Verilog ports, one for each element. OnlyVWord
values were translated into Verilog bitvectors. Now,VVector
values with Boolean elements also get translated into Verilog bitvectors.