Applied formal semantics in hardware compiler frameworks
Published : 8 February 2020
The development of RISC-V instruction set architecture (ISA) is supported by new methodologies and tools which are dedicated to increase the productivity of hardware designs (i.e., high-level design languages and specialized compilation chains). At the language level, Chisel and FIRRTL Hardware Description Languages (HDLs) aim to raise the level of abstraction of hardware design. It thus becomes appealing to formally reason on functional and temporal properties of these high-level designs and rely on appropriate compilation extensions to transfer these high-level properties down to the level of generated Verilog, for example.
In this PhD proposal, we target a formal verification framework for computer architectures to support the specification and verification of timing-related safety and security properties. The following two contributions are expected of this PhD thesis: 1) the design and implementation of a verification infrastructure based on formal executable semantics of Chisel and FIRRTL HDLs and 2) the design and implementation of an assertion language to express timing safety and security properties, which are to be verified with the aforementioned formal infrastructure. The scientific contributions of this thesis are expected to evaluated on a selection of the rich-set of architecture designs provided by the RISC-V ecosystem.