Formal hardware verification based on signal correlation properties

This paper deals with special challenges in the formal verification of high-performance circuits that involve redundant number representations and partial compressions. Our particular focus is the verification of circuits where symbolic consideration of number representations is not sufficient, but where additionally properties beyond operand values need to be considered to show correct operation. As a solution, we consider theorem proving techniques in PVS and we propose a framework that allows for reasoning about signal correlation properties in redundant representations. We develop a library for redundant representations that includes support of basic circuits for partial compression and that verifies several fundamental properties regarding signal correlation and partial compression in the computed results. We outline the applicability of our library in the verification of several practical circuits.