Formal Verification Using SLEC(Sequential Logic Equivalence Checker)

Abstract

Verification of different designs using automated tools has become the widely used methodology for the Electronic Design Automation(EDA) industry. SLEC(Sequential Logic Equivalence checker) is one such tool which uses formal verification. Formal verification is a method of proving or disproving the functionality of any design using Formal methods. Formal Verification does not require input vectors like simulation. It verifies two designs by comparing boolean equation of both the designs,generated using formal algorithms. SLEC(Sequential Logic Equivalence Checker) is a sequential equivalence checker which compares two designs:specification design (SPEC) and Implementation design (IMPL) which may be structurally not equivalent. Formal Verification using SLEC in HLS(High Level Synthesis) is the main motto of this thesis. The ow of HLS using Mentor's Catapult and SLEC(Sequential Logic Equivalence Checker) was studied and performed. Different features of SLEC HLS ow were tested. Bug finding and reporting was done in Bugzilla. Automation work required for the tool was done using scripting. SLEC uses formal verification which leads to better coverage,better resource allocation, lower power consumption and lesser area. SLEC can prove two designs formally equivalent inspite of structural differences.