In "examples/smtbmc/demo1.v" verification，the “assert” statement cannot be recognized

[zsxpdsyz]

When I try to use "make" to formally verify the "examples/smtbmc/demo1.v". I checked the Makefile and find the workflow of the verification is: firstly, using yosys script to rewrite the verilog design to smt2 format. Then, using yosys-smtbmc to perform formal verification.

But I observed the formal check are always passed, then I read the .smt2 file, I found there is no assert or assume statement in the file. This may be a reason for check always passed?

I want to ask: How can we modify the code to perform the correct verification?

[georgerennie]

yosys-smtbmc wraps the .smt2 file and adds the assert statements to perform the verification before passing it to the actual smt solvers (through their stdin). This allows it to incrementally unroll more cycles of the design over time. If you wanted to perform some other verification with this format the smt2 format Yosys generates is described in the write_smt2 help https://yosyshq.readthedocs.io/projects/yosys/en/latest/cmd/write_smt2.html

[KrystalDelusion]

Depending on what you're trying to do, you may also be better off using SBY instead of trying to use yosys-smtbmc directly.

[zsxpdsyz]

Thank you. I use the scripts generated by SBY to complete the verification. BTW, these scripts are more complex than that in document.