Mike Case

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2009-46

April 2, 2009

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-46.pdf

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 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.

Advisors: Robert K. Brayton

---

BibTeX citation:

@phdthesis{Case:EECS-2009-46,
    Author= {Case, Mike},
    Title= {On Invariants to Characterize the State Space for Sequential Logic Synthesis and Formal Verification},
    School= {EECS Department, University of California, Berkeley},
    Year= {2009},
    Month= {Apr},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-46.html},
    Number= {UCB/EECS-2009-46},
    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 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.},
}

EndNote citation:

%0 Thesis
%A Case, Mike 
%T On Invariants to Characterize the State Space for Sequential Logic Synthesis and Formal Verification
%I EECS Department, University of California, Berkeley
%D 2009
%8 April 2
%@ UCB/EECS-2009-46
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-46.html
%F Case:EECS-2009-46