Too often we design a hardware artifact, we verify it using testing, and in some cases formal verification, and finally we may attribute a semantics to an existing circuit to see if we can understand what it means. For developing high assurance hardware (e.g. crypto circuits, silicon root of trust) this is a very unsatisfactory state of affairs. The difficulties are compounded when we try to somehow transcribe a circuit implementation in a hugely complex hardware description language like Verilog into the logic of a theorem prover.
This talk describes an attempt to do things differently that views the formal specification and verification of hardware as an act of development intertwined with the implementation. Formal specification at the outset is very much used as a way of developing, thinking, and exploring the design space rather than being an after thought for a fait accompli.
Our approach is very much inspired by the Kami project at MIT which is currently being used to develop RISC-V processors at the company SiFive. We instead focus on low level circuits and crypto accelerators and we have developed a different set of abstractions suited for describing and attributing semantics to low level circuit blocks. The approach we take involves recasting the Lava hardware description language originally developed in Haskell as a DSL in the Coq theorem prover. Circuit descriptions are composed using overloaded monadic combinators which are parameterized on the type of values flowing over the wires. For one interpretation we can generate circuit graphs with cycles which represent circuit netlists which can be converted to SystemVerilog hardware description (via Coq's Haskell extraction mechanism). Another interpretation of exactly the same structure yields a model of the circuit behaviour which can be used for formal verification against a formal specification (recurrence equations over streams in our case). We apply this technique to the specification and verification of the circuit blocks that comprise the OpenTitan silicon root of trust specification and reference implementation.