VTechWorks staff will be away for the winter holidays starting Tuesday, December 24, 2024, through Wednesday, January 1, 2025, and will not be replying to requests during this time. Thank you for your patience, and happy holidays!
 

Sequential Equivalence Checking of Circuits with Different State Encodings by Pruning Simulation-based Multi-Node Invariants

dc.contributor.authorYuan, Zeyingen
dc.contributor.committeechairHsiao, Michael S.en
dc.contributor.committeememberWang, Chaoen
dc.contributor.committeememberSchaumont, Patrick R.en
dc.contributor.departmentElectrical and Computer Engineeringen
dc.date.accessioned2015-10-06T08:00:28Zen
dc.date.available2015-10-06T08:00:28Zen
dc.date.issued2015-10-05en
dc.description.abstractVerification is an important step for Integrated Circuit (IC) design. In fact, literature has reported that up to 70% of the design effort is spent on checking if the design is functionally correct. One of the core verification tasks is Equivalence Checking (EC), which attempts to check if two structurally different designs are functionally equivalent for all reachable states. Powerful equivalence checking can also provide opportunities for more aggressive logic optimizations, meeting different goals such as smaller area, better performance, etc. The success of Combinational Equivalence Checking (CEC) has laid a foundation to industry-level combinational logic synthesis and optimization. However, Sequential Equivalence Checking (SEC) still faces much challenge, especially for those complex circuits that have different state encodings and few internal signal equivalences. In this thesis, we propose a novel simulation-based multi-node inductive invariant generation and pruning technique to check the equivalence of sequential circuits that have different state encodings and very few equivalent signals between them. By first grouping flip-flops into smaller subsets to make it scalable for large designs, we then propose a constrained logic synthesis technique to prune potential multi-node invariants without inadvertently losing important constraints. Our pruning technique guarantees the same conclusion for different instances (proving SEC or not) compared to previous approaches in which merging of such potential invariants might lose important relations if the merged relation does not turn out to be a true invariant. Experimental results show that the smaller invariant set can be very effective for sequential equivalence checking of such hard SEC instances. Our approach is up to 20x-- faster compared to previous mining-based methods for larger circuits.en
dc.description.degreeMaster of Scienceen
dc.format.mediumETDen
dc.identifier.othervt_gsexam:5720en
dc.identifier.urihttp://hdl.handle.net/10919/56693en
dc.publisherVirginia Techen
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subjectSequential Equivalence Checking(SEC)en
dc.subjectMulti-node Inductive Invariantsen
dc.subjectConstrained Logic Synthesisen
dc.titleSequential Equivalence Checking of Circuits with Different State Encodings by Pruning Simulation-based Multi-Node Invariantsen
dc.typeThesisen
thesis.degree.disciplineComputer Engineeringen
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen
thesis.degree.levelmastersen
thesis.degree.nameMaster of Scienceen

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Yuan_Z_T_2015.pdf
Size:
1.66 MB
Format:
Adobe Portable Document Format

Collections