search

CakeML / hardware

Verilog development and verification project for HOL4
BSD 3-Clause "New" or "Revised" License
24 stars 5 forks source link

Project aims/capabilities/description? #1

Closed ben-marshall closed 5 years ago

ben-marshall commented 5 years ago

Hi there

I'm in the process of gathering a list of open-source tools for verifying hardware designs (Verilog/VHDL etc) and found this. It looks really interesting, but I'm not quite clear from the README / docs(?) exactly what the project does or is for?

I see it is part of a wider project around a verified ML implementation, and was wondering if you had extended this to verifying some hardware implementations?

Cheers, Ben

AndreasLoow commented 5 years ago

This project will enable hardware development inside the interactive theorem prover HOL4. You can describe hardware inside HOL, which enables you to prove properties about the described hardware using the tools available in HOL. One (important) example of a property one could be interested in is circuit correctness; that is, that a circuit follows a high-level specification. What this project does in particular is to provide an automatic way to translate (a type of) circuits (shallowly-)embedded in HOL to Verilog. This automatic translation also produces a proof, saying that the translation is correct (w.r.t. a formal semantics of Verilog we have developed). (This kind of extraction is otherwise usually carried out by unverified translations.) This combination of (1) proving things about circuits inside HOL and (2) having a way to extract one's circuits to a language accepted by commercial synthesis tools (in this case Verilog) allows you to e.g. build formally verified FPGA applications (down to the Verilog-level at least -- the commercial synthesis tools available today do not provide correctness theorems/proofs usable by HOL).

The project is indeed hosted under the CakeML project, but can be used for non-CakeML things (e.g. the regular expression matcher example under the regexp directory). But one of the things we are interested in is building verified stacks (fully-verified computer systems), and any meaningful computer system must be able to host its own toolchain -- this is where the CakeML compiler comes in.

More details ("aims/capabilities/description") will be provided in upcoming publications.

AndreasLoow commented 5 years ago

Closing this as the paper "A Proof-Producing Translator for Verilog Development in HOL" is now available at https://doi.org/10.1109/FormaliSE.2019.00020. The paper "Verified Compilation on a Verified Processor" (https://doi.org/10.1145/3314221.3314622) is relevant as well, as it shows one application of the repo's hardware development method.

ben-marshall commented 5 years ago

Awesome, thanks for the pointer :)