Building Verified Hardware and Verified Stacks in HOL
Andreas Lööw · Chalmers Research (Chalmers University of Technology) · 2021
This thesis explores building provably correct software and hardware inside the HOL4 interactive theorem prover. Interactive theorem provers such as HOL4 are proof environments where manual (human) and automated (machine) proofs can be composed in logically safe ways and all proof steps (be it manual or automated) are mechanically checked.In this thesis, we are in particular interested in systems consisting of both software and hardware, such as so-called verified stacks. A verified stack is a computer system accompanied by a correctness theorem ensuring the correctness of its running software down to the computer system's hardware implementation.One contribution of this thesis is that we provide new tools to build verified stacks. Specifically, we provide a new proof-producing Verilog code generator capable of translating hardware circuits proved correct inside HOL4 to the hardware description language Verilog. We also provide a verified Verilog synthesis tool, called Lutsig, for (a class of) FPGAs. Lutsig translates Verilog designs, such as those generated by our proof-producing Verilog code generator, to technology-mapped netlists. With the combined help of the Verilog code generator and Lutsig, it is possible for hardware designers to design and prove circuits correct inside HOL4 and then translate their circuits down to the netlist level while simultaneously carrying along proved properties.Another contribution is that we apply the new tools in concrete case studies. In particular, one of our case studies contributes to the tradition of building verified stacks as follows. In the case study, we use our Verilog code generator in the construction of a verified proof-of-concept processor that we synthesize for an FPGA board. Building upon this work, we use the processor as the hardware basis for verified stacks based on CakeML programs, including a stack for compiling CakeML programs and a stack for checking proofs. To be able to construct such stacks, we adapt and extend the verified CakeML compiler and its development methodology to support targeting the new processor we have constructed. The CakeML compiler previously only supported compilation to x86, ARM and other architectures without verified implementations.