Hello everyone,
During benchmarking on riscv-formal cores (NERV, PicoRV32, SERV, VexRiscv) with the itp engine, I found fixpoint convergence works correctly with skip=0 but returns bounded results only when skip>0. The underlying reason is that pure BMC cannot rule out paths through invalid reset states without inductive reasoning, so with skip=10 for example, a spurious counterexample can appear at the first checked timeframe.
Has anyone encountered similar limitations with other engines? Are there established patterns in sby for handling designs that require non-zero skip with proof-producing engines?
Thanks!