Software verification and hardware verification are traditionally considered separate enterprises, but our experience suggests that activities in software verification have natural counter parts in hardware verification and vice versa. We believe that there ought to be more technology transfer between the two. In this text, we describe one such instance of technology transfer from the world of interactive theorem proving: we outline how we have adapted the functional-programming-based software-verification flow of the CakeML project to a hardware-verification flow for Verilog. The work described here has been carried out in the HOL4 interactive theorem prover.
Tianrui Wei University of California, Berkeley, Shangyin Tan University of California at Berkeley, Koushik Sen University of California at Berkeley, Krste Asanovic University of California Berkeley
