Formal co-verification of pipelined datapaths

We consider the formal co-verification of various pipelined implementations of a specific instruction set architecture (ISA). The simpler hardware implementations in this variety are complemented by software emulations for the ISA instructions that find no native hardware support. The comprehensive verification of such implementations makes it necessary that software and hardware layers have to be considered jointly and need to be specified in a common framework. We use a modular specification, implementation and verification approach based on theorem proving techniques in PVS that allows the scaling of the implementations and the adaptation of the formal verification efforts even in between the corner cases that we are constructing in detail and thereby enable the formally verified co-design of individual operations of the instruction set guided by cost and performance trade-offs.