The current formal flow is not scaling. Some instructions are taking >40 hours to prove. This is because multiple assertions are active at once, or single assertions are trying to express too much.
I've created a basic tool which makes generating parts of the formal environment easier, and lets one split groups of assertions into individual ones. We can then run more, smaller proof jobs which will hopefully complete quicker.
The tasks here are to:
[ ] Copy the existing assertions into the new fvm-tool format.
[ ] Add a new flow/fvm/ directory and make flow which will automate everything.
[ ] Add a flow section which uses Yosys to generate the N required testbenches, one for each assertion, in SMT2 format.
[ ] Add a flow section which can run one or many of the proofs in parallel, initially using the make -j flag.
The current formal flow is not scaling. Some instructions are taking >40 hours to prove. This is because multiple assertions are active at once, or single assertions are trying to express too much.
I've created a basic tool which makes generating parts of the formal environment easier, and lets one split groups of assertions into individual ones. We can then run more, smaller proof jobs which will hopefully complete quicker.
The tasks here are to:
flow/fvm/
directory and make flow which will automate everything.N
required testbenches, one for each assertion, in SMT2 format.make -j
flag.