search

SymbioticEDA / riscv-formal

RISC-V Formal Verification Framework
ISC License
573 stars 94 forks source link

Add a "mode" option to cfg file #28

Closed AlAlves closed 5 years ago

AlAlves commented 5 years ago

Add a "mode" option on .cfg file to define whether you are going for a bmc or an induction proof

cliffordwolf commented 5 years ago

The formal test-bench used by riscv-formal (rvfi_testbench) only activates the checker in cycle RISCV_FORMAL_CHECK_CYCLE. Thus, changing the SBY mode from bmc to prove will not change what is proven.

Thus for a complete proof rvfi_testbench must be changed so that trig and check are unconstrained, for example by connecting them primary inputs of rvfi_testbench. A new configuration variable, for example RISCV_FORMAL_UNBOUNDED, should control this.