ACM Portal
  Subscribe (Full Service)    Register (Limited Service, Free)    Login
  Search:   The ACM Digital Library   The Guide
  
ACM Home Page
Please provide us with feedback. Feedback
Word level model checking—avoiding the Pentium FDIV error
Full text PdfPdf (365 KB)
Source Annual ACM IEEE Design Automation Conference archive
Proceedings of the 33rd annual Design Automation Conference table of contents
Las Vegas, Nevada, United States
Pages: 645 - 648  
Year of Publication: 1996
ISBN:0-89791-779-0
Authors
E. M. Clarke  School of Computer Science, Carnegie Mellon University, Pittsburgh, PA
M. Khaira  Intel Development Labs., Intel Corporation, 5200 NE Elam Young Pkwy, Hillsboro, OR
X. Zhao  School of Computer Science, Carnegie Mellon University, Pittsburgh, PA and Intel Development Labs., Intel Corporation, 5200 NE Elam Young Pkwy, Hillsboro, OR
Sponsors
IEEE-CAS : Circuits & Systems
SIGDA: ACM Special Interest Group on Design Automation
EDAC : Electronic Design Automation Consortium
Publisher
ACM  New York, NY, USA
Bibliometrics
Downloads (6 Weeks): 4,   Downloads (12 Months): 22,   Citation Count: 9
Additional Information:

references   cited by   index terms   collaborative colleagues  

Tools and Actions: Request Permissions Request Permissions    Review this Article  
DOI Bookmark: Use this link to bookmark this Article: http://doi.acm.org/10.1145/240518.240640
What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

1
Randal E. Bryant , Yirng-An Chen, Verification of arithmetic circuits with binary moment diagrams, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.535-541, June 12-16, 1995, San Francisco, California, United States  [doi>10.1145/217474.217583]
 
2
J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992  [doi>10.1016/0890-5401(92)90017-A]
 
3
Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
4
E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986  [doi>10.1145/5397.5399]
 
5
E. M. Clarke , M. Fujita , X. Zhao, Hybrid decision diagrams, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.159-163, November 05-09, 1995, San Jose, California, United States
 
6
E. M. Clarke and X. Zhao. Analytica: A theorem prover for Mathematica. The Journal of Mathematica, 3(1), 1993.
 
7
Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
 
8
G. S. Taylor. Compatible hardware for division and square root. In Proceedings of the Fifth IEEE Symposium on Computer Arithmetic, 1993.

CITED BY  9
Yirng-An Chen , Randal E. Bryant, ACV: an arithmetic circuit verifier, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.361-365, November 10-14, 1996, San Jose, California, United States
Yirng-An Chen , Randal E. Bryant, PHDD: an efficient graph representation for floating point circuit verification, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.2-7, November 09-13, 1997, San Jose, California, United States
Kathi Fisler , Moshe Y. Vardi, Bisimulation Minimization and Symbolic Model Checking, Formal Methods in System Design, v.21 n.1, p.39-78, July 2002
Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
Harald Ruess , Natarajan Shankar , Mandayam K. Srivas, Modular Verification of SRT Division, Formal Methods in System Design, v.14 n.1, p.45-73, January 1999
David Déharbe, A tutorial introduction to symbolic model checking, Logic for concurrency and synchronisation, Kluwer Academic Publishers, Norwell, MA, 2003
Edmund M. Clarke , Steven M. German , Xudong Zhao, Verifying the SRT Division Algorithm Using Theorem Proving Techniques, Formal Methods in System Design, v.14 n.1, p.7-44, January 1999
William Chan , Richard J. Anderson , Paul Beame , Steve Burns , Francesmary Modugno , David Notkin , Jon D. Reese, Model Checking Large Software Specifications, IEEE Transactions on Software Engineering, v.24 n.7, p.498-520, July 1998
Per Bjesse, Word-level sequential memory abstraction for model checking, Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-9, November 17-20, 2008, Portland, Oregon

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Verification


General Terms:
Design, Theory

Collaborative Colleagues:
E. M. Clarke: colleagues
M. Khaira: colleagues
X. Zhao: colleagues

The ACM Portal is published by the Association for Computing Machinery. Copyright © 2009 ACM, Inc.
Terms of Usage   Privacy Policy   Code of Ethics   Contact Us

Useful downloads: Adobe Acrobat    QuickTime    Windows Media Player    Real Player