Computer-aided design and analysis of circuits and semiconductor – Integrated circuit design processing – Logic design processing
Reexamination Certificate
2011-08-16
2011-08-16
Levin, Naum (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Integrated circuit design processing
Logic design processing
C716S106000, C703S014000
Reexamination Certificate
active
08001498
ABSTRACT:
A computer implemented representation of a circuit design including memory is abstracted to a smaller netlist, which can be analyzed by standard verification tools and by other tools that operate on netlists. The correctness of such systems can require reasoning about a much smaller number of memory entries than exist in the circuit design, and by abstracting such memories to a smaller number of entries, the computational complexity of the verification problem is substantially reduced.
REFERENCES:
patent: 6044211 (2000-03-01), Jain
patent: 6163876 (2000-12-01), Ashar et al.
patent: 6345379 (2002-02-01), Khouja et al.
patent: 6415420 (2002-07-01), Cheng et al.
patent: 6574787 (2003-06-01), Anderson
patent: 6625797 (2003-09-01), Edwards et al.
patent: 6651228 (2003-11-01), Narain et al.
patent: 6691078 (2004-02-01), Beer et al.
patent: 6823486 (2004-11-01), Ghosh
patent: 7020856 (2006-03-01), Singhal et al.
patent: 7149987 (2006-12-01), Zhu et al.
patent: 7284218 (2007-10-01), Roy et al.
patent: 7322017 (2008-01-01), Baumgartner et al.
patent: 7373618 (2008-05-01), Khoo et al.
patent: 7386818 (2008-06-01), Ganai et al.
patent: 7742907 (2010-06-01), Gupta et al.
patent: 7752588 (2010-07-01), Bose
patent: 2002/0138812 (2002-09-01), Johannsen
patent: 2003/0105617 (2003-06-01), Cadambi et al.
patent: 2003/0208730 (2003-11-01), Singhal et al.
patent: 2005/0050484 (2005-03-01), Keller et al.
patent: 2006/0085774 (2006-04-01), Moorby
patent: 2008/0126066 (2008-05-01), Zhu et al.
patent: 2009/0007038 (2009-01-01), Wang et al.
patent: 2010/0077366 (2010-03-01), Bjesse
patent: 2008033404 (2008-02-01), None
Search Report Mailed Mar. 31, 2010 in PCT/US2009/05530 10 pages.
Search Report Mailed Apr. 1, 2010 in PCT/US2009/05537 12 pages.
Jain, Himanshu, et al., “Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 27, No. 2, Feb. 2008, 14 pages.
Adams, Sara, et al., “Automatic Abstraction in Symbolic Trajectory Evaluation,” Proc. of the Formal Methods in CAD conf. 2007, 23 pages.
Armando, Alessandro, et al., “Abstraction Refinement of Linear Programs with Arrays,” Proc. International Conference on Tools and Algorithms for the Construction and Analysis of Systems LNCS 4424 pp. 373-388, 2007.
Bjesse, Per, “A Practical Approach to Word Level Model Checking of Industrial Netlists,” 20th Int'l Conf. on Computer Aided Design, Jul. 2008, 13 pages.
Bryant, Randal E., et al., “Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions,” Lecture Notes in Computer Science; vol. 2404 archive, Proceedings of the 14th International Conference on Computer Aided Verification pp. 78-92 Year of Publication: 2002.
Burch, Jerry R., et al., “Automatic verification of Pipelined Microprocessor Control,” In Proceedings of the 6th international Conference on Computer Aided Verification (Jun. 21-23, 1994). D. L. Dill, Ed. Lecture Notes in Computer Science, vol. 818. Springer-Verlag, London, 68-80.
Clarke, E. M., et al, “Word level model checking-avoiding the Pentium FDIV error.,” In Proceedings of the 33rd Annual Conference on Design Automation (Las Vegas, Nevada, United States, Jun. 3-7, 1996). DAC '96. ACM, New York, NY, 645-648.
Clarke, Edmund, “Counterexample-Guided Abstraction Refinement,” Proc. of the computer aided verification conf. 2000, 2 pages.
Galler, Bernard A., et al., “An Improved Equivalence Algorithm,” Communications of the ACM archive, vol. 7 , Issue 5 (May 1964) pp. 301-303.
Ganai, Malay K., et al., “Efficient Modeling of Embedded Memories in Bounded Model Checking,” in Proceedings of Computer Aided Verification (CAV), 2004 13 pages.
Ganai, Malay K., et al., “Verification of embedded memory systems using efficient memory modeling,” Design, Automation and Test in Europe, 2005. Proceedings 2005 pp. 1096-1101 vol. 2.
Glokler, Tilman, et al., “Enabling Large-Scale Pervasive Logic Verification through Multi-Algorithmic Formal Reasoning,” Formal Methods in Computer Aided Design, 2006. FMCAD '06, Nov. 2006 pp. 3-10.
Hojati, R. and Brayton, R. K. 1995. Automatic Datapath Abstraction in Hardware Systems. In Proceedings of the 7th international Conference on Computer Aided Verification (Jul. 3-5, 1995). P. Wolper, Ed. Lecture Notes in Computer Science, vol. 939. Springer-Verlag, London, 98-113.
Ip, C. Norris, et al., “Better Verfication Through Symmetry,” Formal Methods in System Design 9, 41-75, 1996.
Johannsen, Peer, Dissertation, “Speeding Up Hardware Verification by Automated Data Path Scaling,” Aug. 2002, 201 pages.
Manolios, Panagiotis, et al., “BAT: The Bit-Level Analysis Tool,” Proceedings of Computer Aided Verification (CAV) 2007, LNCS 4590, pp. 303-306, 2007.
McMillan, K.L., “Verfication of an implementation of Tomasulo's algorithm by compositional model checking,” In A. Hu and M. Vardi (editors) Proc. 10th International Conference on Computer Aided Verification (CAV'98), vol. 1427 of LNCS, pp. 110-121, Springer.1998.
Peh, Li-Shiuan, et al., “A Delay Model and Speculative Architecture for Pipelined Routers,” Proc. 7th Int'l Symp on High-Performance Computer Architecture, Jan. 22-24, 2001, Monterrey, Mexico, pp. 255-266.
Pugh, William, “Skip Lists: A Probabilistic Alternative to Balanced Trees,” Communications of the ACM, vol. 33, No. 6, Jun. 1990, 9 pages.
Ranise, Silvio et al, “Satisfiability Modulo Theories,” p. 77-79, IEEE Nov./Dec. 2006, Trends & Controversies, Intelligent Systems and Formal Methods in Software Engineering.
Seger, Carl-Johan H., et al., “Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories,” Technical Report. UMI Order Number: TR-93-08., University of British Columbia, Jul. 1, 1999, 41 pages.
Sheeran, Mary, et al., “Checking Safety Properties Using Induction and a SAT-Solver, ” In Proceedings of the Third international Conference on Formal Methods in Computer-Aided Design (Nov. 1-3, 2000). W. A. Hunt and S. D. Johnson, Eds. Lecture Notes in Computer Science, vol. 1954. Springer-Verlag, London, 108-125.
Haynes Beffel & Wolfeld LLP
Levin Naum
Synopsys Inc.
LandOfFree
Method and apparatus for memory abstraction and verification... 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 apparatus for memory abstraction and verification..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and apparatus for memory abstraction and verification... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2738195