This talk summarizes lessons from several years of experimenting with automatic generation of compiler toolchains from processor description languages (PDL), using approaches ranging from superoptimization via logic programming to SMT-based binary analysis, and presents a new experimental system which builds on these lessons. The new approach takes ISA specifications written in the Sail PDL, as the starting point for software-tools synthesis and verification. Sail is used by practicing engineers to create full-scale formalizations of real ISAs; on the other hand, Sail is based on Lem and is mathematically rigorous. This talk demonstrates how the tool transforms a short sequence of POWER instructions into a proof of an invariant of the final state holding universally over the space of allowed behaviors.
Continue the conversation in Slack
Open Zoom