Design and implementation of formal verification methodology using Boolean satisfiability
Functional verification is an important phase in the design flow of digital circuits as it is used to verify a design when changes occur. It ensures that the functionality of the original design is not affected by the changes. Logic simulation is a widely used technique for the verification of a des...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Final Year Project (FYP) |
| Language: | English |
| Published: |
2011
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/10356/42896 |
| _version_ | 1826111618721775616 |
|---|---|
| author | Phone, Thet Khaing. |
| author2 | Gwee Bah Hwee |
| author_facet | Gwee Bah Hwee Phone, Thet Khaing. |
| author_sort | Phone, Thet Khaing. |
| collection | NTU |
| description | Functional verification is an important phase in the design flow of digital circuits as it is used to verify a design when changes occur. It ensures that the functionality of the original design is not affected by the changes. Logic simulation is a widely used technique for the verification of a design. Formal verification is an alternative technique for logic simulation as it is impossible to verify the overall design completely and detect design bugs by logic simulation since the quality of simulation results deeply depend on given input patterns.
To address this, formal verification uses mathematical techniques to compare the original representation to the new representation. Formal verification method breaks the designs into mathematical representations and then formally proves that the two design representations are equivalent. Formal verification is realized on top of the basic Boolean reasoning techniques such as binary decision diagram (BDD), automatic test-pattern generation (ATPG) and Boolean satisfiability (SAT) as logic circuits compute Boolean functions.
In this report, a design methodology for formal verification of digital combinational circuit using Boolean satisfiability had been proposed and a new formal verification tool Verification-Satisfiability (VeriSat) had been implemented. |
| first_indexed | 2024-10-01T02:53:42Z |
| format | Final Year Project (FYP) |
| id | ntu-10356/42896 |
| institution | Nanyang Technological University |
| language | English |
| last_indexed | 2024-10-01T02:53:42Z |
| publishDate | 2011 |
| record_format | dspace |
| spelling | ntu-10356/428962023-07-07T16:44:58Z Design and implementation of formal verification methodology using Boolean satisfiability Phone, Thet Khaing. Gwee Bah Hwee School of Electrical and Electronic Engineering DRNTU::Engineering::Electrical and electronic engineering::Electronic systems Functional verification is an important phase in the design flow of digital circuits as it is used to verify a design when changes occur. It ensures that the functionality of the original design is not affected by the changes. Logic simulation is a widely used technique for the verification of a design. Formal verification is an alternative technique for logic simulation as it is impossible to verify the overall design completely and detect design bugs by logic simulation since the quality of simulation results deeply depend on given input patterns. To address this, formal verification uses mathematical techniques to compare the original representation to the new representation. Formal verification method breaks the designs into mathematical representations and then formally proves that the two design representations are equivalent. Formal verification is realized on top of the basic Boolean reasoning techniques such as binary decision diagram (BDD), automatic test-pattern generation (ATPG) and Boolean satisfiability (SAT) as logic circuits compute Boolean functions. In this report, a design methodology for formal verification of digital combinational circuit using Boolean satisfiability had been proposed and a new formal verification tool Verification-Satisfiability (VeriSat) had been implemented. Bachelor of Engineering 2011-02-17T06:30:51Z 2011-02-17T06:30:51Z 2010 2010 Final Year Project (FYP) http://hdl.handle.net/10356/42896 en Nanyang Technological University 146 p. application/pdf |
| spellingShingle | DRNTU::Engineering::Electrical and electronic engineering::Electronic systems Phone, Thet Khaing. Design and implementation of formal verification methodology using Boolean satisfiability |
| title | Design and implementation of formal verification methodology using Boolean satisfiability |
| title_full | Design and implementation of formal verification methodology using Boolean satisfiability |
| title_fullStr | Design and implementation of formal verification methodology using Boolean satisfiability |
| title_full_unstemmed | Design and implementation of formal verification methodology using Boolean satisfiability |
| title_short | Design and implementation of formal verification methodology using Boolean satisfiability |
| title_sort | design and implementation of formal verification methodology using boolean satisfiability |
| topic | DRNTU::Engineering::Electrical and electronic engineering::Electronic systems |
| url | http://hdl.handle.net/10356/42896 |
| work_keys_str_mv | AT phonethetkhaing designandimplementationofformalverificationmethodologyusingbooleansatisfiability |