search

openhwgroup / cv32e40p

CV32E40P is an in-order 4-stage RISC-V RV32IMFCXpulp CPU based on RI5CY from PULP-Platform
https://docs.openhwgroup.org/projects/cv32e40p-user-manual/en/latest
Other
966 stars 424 forks source link

Code coverage holes formal analysis #994

Closed YoannPruvost closed 6 months ago

YoannPruvost commented 6 months ago

During code coverage analysis, some holes where too complex to waive by code review. We decided to use formal tool to prove that those holes where indeed unreachable in our configurations.

This PR contains the source files and makefile to reproduce our formal runs.

I left some commented out code as reference as those where effort to prove more holes and can be use in the future if needed

MikeOpenHWGroup commented 6 months ago

Nicely done @YoannPruvost, thanks for this Contribution.