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！
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！