loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formal Methods in Computer Aided Design (FMCAD'06)
Symmetry Reduction for STE Model Checking
San Jose, California, USA
November 12-November 16
ISBN: 0-7695-2707-8
Ashish Darbari, Oxford University Computing Lab, UK
In spite of the tremendous success of STE model checking one cannot verify circuits with arbitrary large number of state holding elements. In this paper we present a methodology of symmetry reduction for STE model checking, using a novel set of STE inference rules. For symmetric circuit models these rules provide a very effective reduction strategy. When used as tactics, rules help decompose a given STE property to a set containing several classes of equivalent STE properties. A representative from each equivalence class is picked and verified using an STE simulator, and the correctness of the entire class of assertions is deduced, using a theorem that we provide. Finally inference rules are used in the forward direction to deduce the overall statement of correctness. Our experiments on verifying arbitrarily large CAMs and circuits with multiple CAMs, show that these can be verified using a fixed, small number of BDD variables.
Citation:
Ashish Darbari, "Symmetry Reduction for STE Model Checking," fmcad, pp.97-105, Formal Methods in Computer Aided Design (FMCAD'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.