On invariants to characterize the state space for sequential logic synthesis and formal verification
by Case, Michael Lee, Ph.D., UNIVERSITY OF CALIFORNIA, BERKELEY, 2009, 210 pages; 3382857

Abstract:

Because of the large size of industrial designs, modern sequential logic synthesis and formal verification techniques cannot afford to accurately characterize the state space of a design. This limits the ability to both optimize designs and to formally prove the designs behave as required.

Invariants are properties that hold in all reachable states. They can be generated in an automated manner, and the set of generated invariants provides a characterization of the design's state space. This characterization can be utilized sequential logic synthesis and formal verification.

In total, this thesis provides (1) a framework to efficiently generate invariants, (2) extensions to sequential logic synthesis to make it more capable of reducing the size of complex designs, and (3) extensions to formal verification to increase its scalability on complex industrial designs.

 
AdviserRobert Brayton
SchoolUNIVERSITY OF CALIFORNIA, BERKELEY
SourceDAI/B 70-10, p. , Dec 2009
Source TypeDissertation
SubjectsElectrical engineering
Publication Number3382857
Adobe PDF Access the complete dissertation:
 

» Find an electronic copy at your library.
  Use the link below to access a full citation record of this graduate work:
  http://gateway.proquest.com/openurl%3furl_ver=Z39.88-2004%26res_dat=xri:pqdiss%26rft_val_fmt=info:ofi/fmt:kev:mtx:dissertation%26rft_dat=xri:pqdiss:3382857
  If your library subscribes to the ProQuest Dissertations & Theses (PQDT) database, you may be entitled to a free electronic version of this graduate work. If not, you will have the option to purchase one, and access a 24 page preview for free (if available).

About ProQuest Dissertations & Theses
With over 2.3 million records, the ProQuest Dissertations & Theses (PQDT) database is the most comprehensive collection of dissertations and theses in the world. It is the database of record for graduate research.

The database includes citations of graduate works ranging from the first U.S. dissertation, accepted in 1861, to those accepted as recently as last semester. Of the 2.3 million graduate works included in the database, ProQuest offers more than 1.9 million in full text formats. Of those, over 860,000 are available in PDF format. More than 60,000 dissertations and theses are added to the database each year.

If you have questions, please feel free to visit the ProQuest Web site - http://www.proquest.com - or call ProQuest Hotline Customer Support at 1-800-521-3042.