Formal checks integration with simulation flows. - Githubissues

scarv / xcrypto

XCrypto: a cryptographic ISE for RISC-V

MIT License

90 stars 10 forks source link

Formal checks integration with simulation flows. #43

Closed ben-marshall closed 5 years ago

ben-marshall commented 5 years ago

The old simulation model of the COP has been removed in favour of purly using the formal checkers.
This work will add the formal checkers back into the simulation testbench.
The aim is to remove the duplication of effort. Where there used to be a model of each instruction in both the formal flow and the simulation flow, now there is just the formal checks, re-used in both the formal flow and simulation flow.

Todo:

[x] Move formal interface abstraction logic from formal testbench into its own module.
[ ] Integrate formal checkers into icarus simulation flow.