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

Some confusion about skip option #57

Open
LIIT0215 opened this issue Mar 11, 2022 · 0 comments
Open

Some confusion about skip option #57

LIIT0215 opened this issue Mar 11, 2022 · 0 comments

Comments

@LIIT0215
Copy link

LIIT0215 commented Mar 11, 2022

Hello, I have carefully watched these docs and the introduction video for the risc-v formal framework and learned about the use of symbiyosys in order to know how this framework works. However, when I read the SBY file in the check part of the framework, I am confused about the skip in options . Considering it's a BMC process, I wonder why there is no assert error in these skipped steps? I appreciate for your early reply, thanks!

[options]
mode bmc
expect pass,fail
append 0
depth 21
skip 20

[engines]
smtbmc boolector
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant