Complete formal proofs for LSU, Dcache and CPU modules - Githubissues

openrisc / mor1kx

mor1kx - an OpenRISC 1000 processor IP core

Other

490 stars 146 forks source link

Complete formal proofs for LSU, Dcache and CPU modules #151

Open stffrdhrn opened 2 years ago

stffrdhrn commented 2 years ago

When fixing #146 I rewrote formal properties to do a better job of simulating real Load/Store and Dcache transactions.

I was able to track down the bug and fix it. However, the formal verification for LSU, Dcache and CPU now has a few limitations.

The mor1k_lsu_cappuccino, mor1k_cappuccino and mor1k formal no longer passes induction, only bmc is enabled
The LSU validation runs with dmmu off, this was done to simplify scope and focus on the d-cache bug
The D-Cache and/or DMMU validation runs with only a single way, this was done for simplification, but we should test multiple way