View Full Document

Recording Synthesis History for Sequential Verification



View the full content.
View Full Document
View Full Document

1 views

Unformatted text preview:

Recording Synthesis History for Sequential Verification Alan Mishchenko Robert Brayton Department of EECS University of California Berkeley alanmi brayton eecs berkeley edu Abstract Performing synthesis and verification in isolation has two undesirable consequences 1 verification runs the risk of becoming intractable and 2 strong sequential optimizations are not applied because they are hard to verify This paper develops a methodology for sequential equivalence checking using feedback from synthesis A format for recording synthesis information is proposed An implementation is described and experimentally compared against an efficient general purpose sequential equivalence checker that does not use synthesis information Experimental results confirm expected substantial savings in runtime of equivalence checking for large designs 1 Introduction In this paper we propose a methodology shift to a synthesis transparent process which records and uses the synthesis history in an efficient way It can promote the use of sequential synthesis and enable a scalable verification of the result Sequential synthesis can result in considerable reductions in delay e g see 19 and area however it is mostly avoided for reasons of non scalability of both synthesis and verification To circumvent this we believe that sequential synthesis and verification must go hand in hand to make sequential synthesis acceptable and propose a way to make this happen General sequential equivalence checking GSEC of two FSMs is PSPACE complete however if synthesis is restricted by one set of combinational transformations followed by one retiming or vice versa the problem is provably simpler On the other hand iterating retiming and combinational transformations makes the problem again PSPACE complete 12 even though this is a very restricted set of sequential transformations Also as in the case of combinational equivalence checking CEC 18 in practice the problem becomes simpler if there are structural



Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view Recording Synthesis History for Sequential Verification and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Recording Synthesis History for Sequential Verification and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?