[Colloquium] Zijiang Yang talk - Friday, May 23rd

[Meridel Trimble]

--------------------------------------------------------------------------------

TOYOTA TECHNOLOGICAL INSTITUTE 
--------------------------------------------------------------------------------

Date: Friday May 23rd, 2003

Time: 2:30 p.m.

Place: Ryerson Hall 251 

Speaker: Zijiang Yang 
University of Pennsylvania

Title:  Reducing the Computational Requirements of Symbolic Model Checking

Abstract: 
As the complexity of hardware/software designs continues to grow, formal 
verification becomes the trend in industry. Verification techniques using 
symbolic state space traversal rely on efficient algorithms based on Binary 
Decision Diagram(BDD) for reachability computation. Unfortunately, BDD size is 
very sensitive to the number of variables, variable ordering, and the nature of 
the logic expressions being represented. In spite of a large body of work, the 
current purely BDD-based approach has been unreliable for designs of realistic 
size and functionality. 

Instead of using pure symbolic method, we combine BDD-based and Boolean 
Satisfiability (SAT)-based techniques in a single integrated framework.  In our 
approach to reachability computation, we use BDDs to represent state sets, and 
a Conjunction Normal Form(CNF) formula to represent the transition relation. 
All the solutions are enumerated using a backtracking search algorithm for SAT 
that exhaustively visits the entire space. However, rather than using SAT to 
enumerate each solution all the way down to a leaf, we invoke BDD-based 
algorithm at intermediate points within the SAT decision procedure, which 
effectively obtains all solutions below that point in the search tree. This 
patented technology, together with inactive clause removal and dynamic decision 
partitioning, have been implemented in commercial verification system and shown 
ability of verifying industrial designs.

*Refreshments will be served after the talk in Ryerson 255* 

If you wish to meet with the speaker, please send e-mail to Meridel Trimble 
mtrimble at uchicago.edu 


Toyota Technological Institute at Chicago