Validation of SLEC for RTL Front End

Abstract

Formal verification is a procedure to verify design specification using mathematical reasoning. It uses formula to verify whether design specs are preserved in generated implementation (Impl-RTL) or not. Irrespective of input values, formally verified design holds true. Formal verification is done using 2 methods: Equivalence checking and model checking. Equivalence checker -equivalence checking tools- uses two designs to be proven functionally equal. Formal verification tool which uses equivalence checking method, checks functional correctness between RTL and gate level netlist. In sequential equivalence checking methodology, state-space travelling is avoided. Instead of one-to-one state mapping, only initial states and outputs are considered and outputs are compared for defining equality between spec and impl design. SLEC is Sequential Logic Equivalence Checker that formally verifies 2 designs. Validation and quality assurance of formal verification tool SLEC - Sequential Logic Equivalence Checker in different area such as RTL front end, HLS is basic motto of this thesis. Necessity of verification of designs and need for automation of verification methodology, different simulating and synthesized tools are developed in Electronics Design Automation (EDA) industry. So validation and testing of those automated tools are necessary. So that maximum benefits can be achieved in terms of code coverage, area and power required, functionality, resource allocation. In this project, understanding of steps of formal verification and validation of SLEC with respect to design and language is primary focus using manual testing, flow testing and regressive testing.