This PR adds a few lines of Makefile that tell coqc to output a hex file containing the RISC-V binary for the SHA256 driver produced by the bedrock2 compiler, and further commands to turn this into an object file (.o) and then into a library file (.a) that OpenTitan's build system, meson, accepts.
It also adds a README.md with instructions on how to run OpenTitan's verilator-based SHA256 functional test with OpenTitan's SHA256 driver replaced by our bedrock2-generated RISC-V binary, and the functional test still passed :tada:
The only kind of difficulties encountered were how to tell the build system what to do. The bedrock2-generated RISC-V binary worked on the first try, so it seems that software verification using Coq can actually save you from having to debug your software :sweat_smile:
This PR adds a few lines of
Makefilethat tellcoqcto output a hex file containing the RISC-V binary for the SHA256 driver produced by the bedrock2 compiler, and further commands to turn this into an object file (.o) and then into a library file (.a) that OpenTitan's build system,meson, accepts. It also adds aREADME.mdwith instructions on how to run OpenTitan's verilator-based SHA256 functional test with OpenTitan's SHA256 driver replaced by our bedrock2-generated RISC-V binary, and the functional test still passed :tada: The only kind of difficulties encountered were how to tell the build system what to do. The bedrock2-generated RISC-V binary worked on the first try, so it seems that software verification using Coq can actually save you from having to debug your software :sweat_smile: