Article

Free access

Counterexample-guided choice of projections in approximate symbolic model checking

Authors:

Shankar G. Govindaraju,

David L. DillAuthors Info & Claims

ICCAD '00: Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design

Pages 115 - 119

Published: 05 November 2000 Publication History

PDF eReader

Abstract

BDD-based symbolic techniques of approximate reachability analysis based on decomposing the circuit into a collection of overlapping sub-machines (also referred to as overlapping projections) have been recently proposed. Computing a superset of the reachable states in this fashion is susceptible to false negatives. Searching for real counterexamples in such an approximate space is liable to failure. In this paper, the "hybridization effect" induced by the choice of projections is identified as the cause for the failure. A heuristic based on Hamming Distance is proposed to improve the choice of projections, that reduces the hybridization effect and facilitates either a genuine counterexample or proof of the property. The ideas are evaluated on a real large design example from the PCI Interface unit in the MAGIC chip of the Stanford FLASH Multiprocessor.

References

[1]

Balarin, F. and Sangiovanni-Vincentelli, A. L., "An iterative approach to language containment," CAV, pp. 29-40, 1993.

Digital Library

Google Scholar

[2]

Bryant, R. E., "Graph-based algorithms for Boolean function manipulation," IEEE Transactions on Computers, Vol. C-35, No. 8, pp. 677-691, August 1986.

Digital Library

Google Scholar

[3]

Burch, J. R. et al., "Symbolic model checking: 1020 states and beyond," LICS, pp. 428-439, 1990.

Google Scholar

[4]

Cho, H. et al., "Automatic state space decomposition for approximate FSM traversal based on circuit analysis," IEEE-TCAD, Vol. 15, No. 12, pp. 1451-1464, December 1996.

Digital Library

Google Scholar

[5]

Clarke, E. et al., "Counterexample-guided abstraction refinement," CAV, pp. 154-169, July 2000.

Digital Library

Google Scholar

[6]

Govindaraju, G. S., Dill, D. L., Hu, A. J, and Horowitz, M. A., "Approximate reachability with BDDs using over-lapping projections," DAC, pp. 451-456, 1998.

Digital Library

Google Scholar

[7]

Govindaraju, G. S. and Dill, D. L., "Verification by approximate forward and backward reachability," ICCAD, pp. 366-370, 1998.

Digital Library

Google Scholar

[8]

Kurshan, R. P., "Timing verification by successive approximation," US Patent US05483470.

Google Scholar

[9]

Kuskin, J., et al., "The Stanford FLASH multiprocessor," ISCA, pp. 301-313, April 1994.

Digital Library

Google Scholar

[10]

Shimizu, K., Dill, D., and Hu, A. J., "Monitor based formal specification of PCI," (To appear).

Google Scholar

[11]

Yang, C. H., and Dill, D., "Validation with guided search of the state space," DAC, pp. 599-604, 1998.

Digital Library

Google Scholar

Cited By

View all

Tian CDuan ZNotkin DCheng BPohl K(2013)Detecting spurious counterexamples efficiently in abstract model checkingProceedings of the 2013 International Conference on Software Engineering10.5555/2486788.2486816(202-211)Online publication date: 18-May-2013
https://dl.acm.org/doi/10.5555/2486788.2486816
Tian CDuan Z(2011)Making abstraction-refinement efficient in model checkingProceedings of the 17th annual international conference on Computing and combinatorics10.5555/2033094.2033130(402-413)Online publication date: 14-Aug-2011
https://dl.acm.org/doi/10.5555/2033094.2033130
Banerjee ADasgupta PChakrabarti P(2008)Auxiliary state machines + context-triggered properties in verificationACM Transactions on Design Automation of Electronic Systems10.1145/1391962.139197013:4(1-31)Online publication date: 3-Oct-2008
https://dl.acm.org/doi/10.1145/1391962.1391970
Show More Cited By

Recommendations

Counterexample-guided abstraction refinement for symbolic model checking

The state explosion problem remains a major hurdle in applying symbolic model checking to large hardware designs. State space abstraction, having been essential for verifying designs of industrial complexity, is typically a manual process, requiring ...
Approximate symbolic model checking using overlapping projections
SAT-based counterexample-guided abstraction refinement

We describe new techniques for model checking in the counterexample-guided abstraction-refinement framework. The abstraction phase "hides" the logic of various variables, hence considering them as inputs. This type of abstraction may lead to "spurious" ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ICCAD '00: Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design

November 2000

558 pages

ISBN:0780364481

Conference Chair:
Ellen M. Sentovich
Cadence Berkley Labs., Berkley, California

Publisher

IEEE Press

Publication History

Published: 05 November 2000

Check for updates

Qualifiers

Article

Conference

ICCAD '00

Sponsor:

SIGDA

ICCAD '00: International Conference on Computer Aided Design

November 5 - 9, 2000

California, San Jose

Acceptance Rates

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
126
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)1

Reflects downloads up to 31 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Tian CDuan ZNotkin DCheng BPohl K(2013)Detecting spurious counterexamples efficiently in abstract model checkingProceedings of the 2013 International Conference on Software Engineering10.5555/2486788.2486816(202-211)Online publication date: 18-May-2013
https://dl.acm.org/doi/10.5555/2486788.2486816
Tian CDuan Z(2011)Making abstraction-refinement efficient in model checkingProceedings of the 17th annual international conference on Computing and combinatorics10.5555/2033094.2033130(402-413)Online publication date: 14-Aug-2011
https://dl.acm.org/doi/10.5555/2033094.2033130
Banerjee ADasgupta PChakrabarti P(2008)Auxiliary state machines + context-triggered properties in verificationACM Transactions on Design Automation of Electronic Systems10.1145/1391962.139197013:4(1-31)Online publication date: 3-Oct-2008
https://dl.acm.org/doi/10.1145/1391962.1391970
He FSong XGu MSun JZhou HMacii EYan ZMassoud Y(2007)Effective heuristics for counterexample-guided abstraction refinementProceedings of the 17th ACM Great Lakes symposium on VLSI10.1145/1228784.1228878(393-398)Online publication date: 11-Mar-2007
https://dl.acm.org/doi/10.1145/1228784.1228878
He FSong XGu MSun J(2006)A probabilistic learning approach for counterexample guided abstraction refinementProceedings of the 4th international conference on Automated Technology for Verification and Analysis10.1007/11901914_6(39-50)Online publication date: 23-Oct-2006
https://dl.acm.org/doi/10.1007/11901914_6
Glusman MKamhi GMador-Haim SFraer RVardi M(2003)Multiple-counterexample guided iterative abstraction refinementProceedings of the 9th international conference on Tools and algorithms for the construction and analysis of systems10.5555/1765871.1765889(176-191)Online publication date: 7-Apr-2003
https://dl.acm.org/doi/10.5555/1765871.1765889
McMillan KAmla N(2003)Automatic abstraction without counterexamplesProceedings of the 9th international conference on Tools and algorithms for the construction and analysis of systems10.5555/1765871.1765875(2-17)Online publication date: 7-Apr-2003
https://dl.acm.org/doi/10.5555/1765871.1765875
Mitchell ITomlin C(2003)Overapproximating Reachable Sets by Hamilton-Jacobi ProjectionsJournal of Scientific Computing10.1023/A:102536422756319:1-3(323-346)Online publication date: 1-Dec-2003
https://dl.acm.org/doi/10.1023/A%3A1025364227563
Shimizu KDill DAckland B(2002)Deriving a simulation input generator and a coverage metric from a formal specificationProceedings of the 39th annual Design Automation Conference10.1145/513918.514118(801-806)Online publication date: 10-Jun-2002
https://dl.acm.org/doi/10.1145/513918.514118
Wang DJiang PKukula JZhu YMa TDamiano RRabaey J(2001)Formal property verification by abstraction refinement with formal, simulation and hybrid enginesProceedings of the 38th annual Design Automation Conference10.1145/378239.378260(35-40)Online publication date: 22-Jun-2001
https://dl.acm.org/doi/10.1145/378239.378260

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Recommendations

Counterexample-guided abstraction refinement for symbolic model checking

Approximate symbolic model checking using overlapping projections

SAT-based counterexample-guided abstraction refinement