Rapid, Formal Verification with Automated and Executable, Cycle-accurate simulators, and Generated Testbenches.

Advances in silicon integration technology have allowed the emergence of extremely complex Systems-on-Chip and Application-Specific Integrated Circuits. This complexity impacted severely the verification time and effort of delayed products, that due to this they often miss the market window. Engineering teams have experienced exponential verification time increase with the linear complexity increase and the largest proportion of effort is due to segmented, long, tedious, bug-prone and repetitive low level verification. This work presents a High-level Synthesis – driven formal verification method, aimed in quickly verifying high-level software or hardware code which rapidly converges results from different abstraction levels in a formal design flow. First the benefits of formal techniques are explained and the proposed methodology is outlined. Then 4 converging aspects of our formal methodology, and namely high-level program code verification, cycle-accurate verification, RTL verification and automatically-generated test-benches are explained, discussed and cross-compared. The aim is to rapidly converge all types of possible formal verification types before the final implementation is ported to the manufacturer to create the IC. Our methods are formal and rapid in nature since the automatically generated cycle-accurate simulator, the FSM RTL model and the test benches are extracted from the internal formally Synthesized state schedule models, after the optimization phase is concluded. A large number of benchmarks and real-life applications, were synthesized and verified with the discussed method and in all cases the formal methods caught specification or functional bugs early in the design flow, allowing the rapid implementation of the products.