search

B-Lang-org / bsc

Bluespec Compiler (BSC)
Other
906 stars 143 forks source link

Assume statements are recognized, but not allowed in any context #392

Open danielkasza opened 2 years ago

danielkasza commented 2 years ago

It appears that assume statements are recognized by the compiler, but they are not allowed in any context.

quark17 commented 2 years ago

Can you have a look at Issue #326 and see if that helps any? For example, the default behavior of BSV is to attempt to synthesize SVA statements into logic, which only works for a subset of SVA; if you compile with -passthrough-assertions then BSC passes the assertions through (instead of synthesizing them) which should not be as limited.

(Also, if you could include the output you are seeing and, if possible, an example input, that would be helpful.)

danielkasza commented 2 years ago

@quark17, I am using the -passthrough-assertions flag. In all context I've tried, I am getting:

As far as I can tell, this comes from https://github.com/B-Lang-org/bsc/blob/93be312c41ad82edb0a004dadb7fbf231bb4de4d/src/comp/Parser/BSV/CVParser.lhs#L5783

which checks for allowAssume. I could not find any code that would set allowAssume to true.