Formal proof between two designs having different level of abstraction

This paper presents a solution for formal verification between two designs described at different levels of abstraction, thus containing sequential differences such as pipelining, timing constraints, interfaces, etc... Sequential Equivalence Checking allows in some case to perform formal proof between these design descriptions. SLEC (Calypto Design Systems, Inc) is a tool that offers an equivalence checker solution, able to compare an untimed algorithm description (C+ + level) versus its Register Transfer Level (RTL) implementation. This work consisted in interoperability testing the integration of SLEC inside a High-Level Synthesis (HLS) tool. This integration reduces verification time by eliminating testbenches and assertion creation. We will illustrate issues encountered and the way they were fixed through the formal proof run on LDPC encoder or UWB algorithms HLS synthesis results.