Synthesis-Embedded Verification

The proliferation of computing systems and subsystems combined with the need for high performance, product security and low energy have forced the development of tools that generate hardware systems and hardware components automatically from higher-level of algorithmic descriptions. The technology background behind this phenomenon is called High-Level Synthesis (HLS) and it has been an active research topic for at least the last 3 decades. HLS hasn't been established as a de facto design approach in industry because of problems with the quality of the generated hardware descriptions and the lack of complete automation and compatibility with all the programming constructs that sometimes require manual rewriting of the whole module in order for the HLS tool to be able to process it. One greater problem is that often the available HLS tools generate bugs in the generated hardware which are difficult to trace and correct, as the generated architecture usually contains hundreds of FSM states. Moreover, verification tasks and flows which are disjoint from the synthesis flows often fails to find all bugs and it is difficult to learn and run easy as in the case of formal verification. Here, we discuss a unique verification strategy that it is integrated in the synthesis flow and it doesn't require any verification skills at all, but only how to compile and run C programs, which are driven by run-time options activated by keystrokes. Moreover, because the verified model is the same as this of the synthesis process, it reassures that the verified module is exactly the same as the generated hardware, so the same regression tests can run as in the high-level specification C/Ada program model. The generated cycle accurate simulators are C programs that model the execution of the formal synthesized FSMs. Because of the synthesis transformation formal model with logic inference that we use, the whole synthesis/verification flow of our approach is formal.