Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
2005-05-06
2008-08-26
Siek, Vuthe (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000
Reexamination Certificate
active
07418680
ABSTRACT:
A method to check correspondence between different representations of a circuit may include abstracting a first computer language representation of the circuit to form a first abstract model of the circuit and abstracting a second computer language representation of the circuit to form a second abstract model of the circuit. The method may also include forming a product machine using the first and second abstract models. The method may further include checking correspondence between the first and second abstract models using the product machine.
REFERENCES:
patent: 6131078 (2000-10-01), Plaisted
patent: 2003/0191615 (2003-10-01), Bailey et al.
Carl Pixley, Guest Editor's Introduction: Formal Verification of Commercial Integrated Circuits, IEEE Design & Test of Computers, 18(4):4-5, 2001.
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Yhu. Symbolic model checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems, pp. 193-207, 1999.
A. Biere, E. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a Power PC™ microprocessor using symbolic model checking without BDDs. In N. Halbwachs and D. Peled, editors, Proceedings of the 11thInternational Conference on Computer Aided Verification (CAB 99), Lecture Notes in Computer Science. Springer Verlag, 1999.
A. Biere, A.Cimatti, E.M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Design Automation Conference (DAC '99), 1999.
Joao P. Marques-Silva and Karem A. Sakallah. Grasp—A New Search Algorithm for Satisfiability. In Proceedings of IEEE/ACM International Conference on Computer-Aided Design, pp. 220-227, Nov. 1996.
Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38thDesign Automation Conference (DAC '01), Jun. 2001.
D. Kroening and O. Strichman. Efficient computation of recurrence diameters. In Proceedings of the Fourth International Conference on Verification, Model Checking and Abstract Interpretation. Springer, 2003. To appear.
O. Shtrichman. Tuning SAT checkers for bounded model checking. In E.A. Emerson and A.P. Sistla, editors, Proceedings of the 12thInternational Conference on Computer Aided Verification (CAV 2000), Lecture Notes in Computer Science. Springer Verlag, 2000.
Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia, Gila Kami, Armando Tacchella, and Moshe Y. Vardi. Benefits of bounded model checking at an industrial setting. In Gerard Berry, Hubert Comon, and Alain Finkel, editors, Proceedings of the 13thInternational Conference on Computer Aided Verification (CAV 2001), No. 2102 in Lecture Notes in Computer Science, pp. 436-453. Springer Verlag, 2001.
Per Bjesse, Tim Leonard, and Abdel Mokkedem. Finding bugs in an Alpha microprocessor using satisfiability solvers. In Gerard Berry , Hubert Comon, and Alain Finkel, editors, Proceedings of the 13thInternational Conference on Computer Aided Verification (CAV 2001), No. 2102 in Lecture Notes in Computer Science, pp. 454-464. Springer Verlad, 2001.
Luc Semeria, Andrew Seawright, Renu Mehra, Daniel Ng, Arjuna Ekanayake, and Barry Pangrle. RTL C-based methodology for designing and verifying a multi-threaded processor. In Proc. Of the 39thDesign Automation Conference ACM Press, 2002.
I. Page. Constructing Hardware-Software Systems from a Single Description. Journal of VLSI Signal Processing, 1291):87-107, 1996.
A. Pnueli, M. Siegel, and O. Shtrichman. The code validation tool (CVT)—automatic verification of a compilation process. Int. Journal of Software Tools for Technology Transfer (STTT), 2(2):192-201, 1998.
R. Cytron, J. Ferrante, B.K. Rosen, M.N. Wegman, and F.K. Zadeck. An efficient method of computing static single assignment form. In Proceedings of the 16thACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 25-35. ACM Press, 1989.
David W. Currie, Alan J. Hu, and Sreeranga Rajan. Automatic formal verification of dsp software. In Proceedings of the 37thDesign Automation Conference (DAC 2000), pp. 130-135. ACM Press, 2000.
Kiyoharu Hamaguchi. Symbolic simulation heuristics for high-level design descriptions with uninterpreted functions. In International Workshop on High-Level Design, Validation, and Test, pp. 25-30. IEEE, 2001.
C. Blank, H. Eveking, J. Levihn, and G. Ritter. Symbolic simulation—state of the art and applications. In International Workshop on High-Level Design, Validation, and Test, pp. 45-50. IEEE, 2001.
Apt., Krzysztof R. Logics and Models of Concurrent Systems, NATO ASI Series, Series F: Computer and System Sciences, vol. 13, no date.
T. Ball and S. Rajamani, Automatically Validating Temporal Safety Properties of Interfaces. In The 8thInternational SPIN Workshop on Model Checking of Software, vol. 2057 of LNCS, pp. 103-122. Springer, May 2001.
T. Ball and S. Rajamani, Boolean Programs: A Model and Process For Software Analysis. Technical Report 2000-14, Microsoft Research, Feb. 2000.
S.K. Lahiri, R.E. Byrant, and B. Cook. A symbolic approach to predicate abstraction. In W.A. Hunt and F. Somenzi, editors,Computer-Aided Verification(CAV), No. 2725 in LNCS, pp. 141-153. Springer-Verlag, Jul. 2003.
E. Clarke, D. Kroening and K. Yorav, Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking. In Proceedings of DAC 2003, pp. 368-371. ACM Press, 2003.
E. Clarke, D. Kroening, N. Sharygina and K. Yorav, Predicate Abstraction of ANSI-C Programs using SAT. In Proc. Of the Model Checking for Dependable Software-Intensive Systems Workshop, San Francisco, USA, 2003.
A. Gupta, Z. Yang, P. Ashar and A. Gupta, SAT-Based Image Computation with Application in Reachability Analysis. in Formal Methods in Computer-Aided Design (FMCAD), No. 1954 in LNCS, pp. 354-372, 2000.
S. Graf and H. Saidi, Construction of Abstract State Graphs With PVS. In O. Grumberg, editor, Proc. 9thInternational Conference on Computer Aided Verification (CAV '97), vol. 1254, pp. 72-83. Springer Vrlag, 1997.
D. Detlefs, G. Nelson and J. Saxe, Simplify: A Theorem Prover For Program Checking. Technical Report HPL-2003-148, HP Labs, Jul. 2003.
E. Clarke, O. Gumberg and D. Long, Model Checking and Abstraction. In Principles of Programming Lanuages, Jan. 1992.
E. Clarke, M. Talupur, and D. Wang. SAT based predicate abstraction for hardware Verification. InProceedingsof SAT '03, May 2003.
D. Plaisted, A. Biere and Y. Zhu, A SatisfiabilityTester for Quantified Boolean Formulae. Journal of Discrete Applied Mathematics (DAM), 2003.
J.E. Smith and A.R. Pleszkun. Implementing Precise Interrupts in Pipelined Processors. IEEE Transactions on Computers, 37(5):562-573, 1988.
R. Tomasulo. An Efficient Algorithm For Exploiting Multiple Arithmetic Units, IBM Journal of Research and Development, 11(1):25-33, 1967.
K. McMillan. Applying SAT Methods in Unbounded Symbolic Model Checking. In 14thConference on Computer Aided Verification, pp. 250-264, 2002.
Clarke, Edmund M. Jr., et al., Model Checking, (1999) United States.
Kurshan, Robert P., Computer-Aided Verification of Coordinating Processes, The Automata-Theorectic Approach (1994) Princeton University Press.
Matumoto, Takeshi, et al., Equivalence Checking in C-based Hardware Descriptions by Using Symbolic Simulation and Program Slicer, InInternational Workshop on Logic Synthesis(IWLS '03), 2003.
Clarke Edmund M.
Kroening Daniel
Carnegie Mellon University
Moore Charles L.
Moore & Van Allen PLLC
Siek Vuthe
LandOfFree
Method and system to check correspondence between different... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Method and system to check correspondence between different..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and system to check correspondence between different... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3994802