Episode 5 -
Architecture specifications such as ARMv8-A and RISC-V are the ultimate foundation for software verification and the correctness criteria for hardware verification. They should define the allowed sequential and relaxed-memory concurrency behaviour of programs, but hitherto there has been no integration of full-scale instruction-set architecture (ISA) semantics with axiomatic concurrency models, these ISA semantics can be surprisingly large and intricate, e.g. 100k+lines for ARMv8-A.
Sail is a custom domain-specific language for ISA semantics, in which we have developed formal models for ARMv8-A, RISC-V, and MIPS. In this talk I will discuss our work on formalising these architectures, and present a tool Isla, which is capable of simulating relaxed memory models over these large architecture specifications using symbolic execution. This allows us to consider aspects of the concurrent behavior of these architectures not previously considered by other tools, but which are relevant to systems software such as operating systems and hypervisors. These aspects include feature such as instruction fetch behavior and address translation.
Relevant links:In this talk, we will give an introduction to rule-based programming and its suitability for formal reasoning of hardware design. We will specifically present the semantics of the Koika language, an EDSL in Coq, that allows precise reasoning about the functional and performance (cycle count) properties of hardware design.
Relevant links:
This talk describes the specification, implementation and formal verification inside the Coq theorem prover of the AES crypto accelerator component of the OpenTitan silicon roof of trust. The approach we take is inspired by Adam Chlipala in his book Certified Programming with Dependent Types. We have developed a Lava-like domain specific hardware description language called Cava in Coq’s Gallina language which is designed to help describe low level data-path style circuits with a view to having tight control over resource utilization and performance. This allows us to specify, implement and formally verify high assurance systems in one model where specifications are plain Gallina functions that specify the desired behaviour of hardware components. Our system can extract circuit descriptions from our Coq DSL to SystemVerilog for implementation on FPGA circuits.
We are also planning on building on this work to also tackle the co-design of software and hardware where we extract both C code (or RISC-V machine code) and SystemVerilog and a register or bus-interface so we can reason about the end-to-end behaviour of a system comprising hardware and software.