{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:19:17Z","timestamp":1759637957853,"version":"3.32.0"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2005,9,1]],"date-time":"2005-09-01T00:00:00Z","timestamp":1125532800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2005,9]]},"DOI":"10.1007\/s10703-005-2250-1","type":"journal-article","created":{"date-parts":[[2005,9,13]],"date-time":"2005-09-13T06:50:30Z","timestamp":1126594230000},"page":"67-112","source":"Crossref","is-referenced-by-count":5,"title":["A Formal Framework for Verification of Embedded Custom Memories of the Motorola MPC7450 Microprocessor"],"prefix":"10.1007","volume":"27","author":[{"given":"Jayanta","family":"Bhadra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew K.","family":"Martin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacob A.","family":"Abraham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"2250_CR1","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1145\/356914.356916","volume":"15","author":"M. Abadir","year":"1993","unstructured":"M. Abadir and J. Reghbati, \u201cFunctional testing of semiconductor random access memories,\u201d ACM Computing Surveys, Vol. 15, No. 3, pp. 175\u2013198, 1993.","journal-title":"ACM Computing Surveys"},{"key":"2250_CR2","doi-asserted-by":"crossref","unstructured":"D.L. Beatty and R.E. Bryant, \u201cFormally verifying a microprocessor using a symbolic methodology,\u201d in Proceedings of Design Automation Conference, 1994, pp. 596\u2013602.","DOI":"10.1145\/196244.196575"},{"key":"2250_CR3","doi-asserted-by":"crossref","unstructured":"J. Bhadra and N. Krishnamurthy, \u201cAutomatic generation of design constraints in verifying high performance embedded dynamic circuits,\u201d in Proceedings of The International Test Conference, 2002, pp. 213\u2013222.","DOI":"10.1109\/TEST.2002.1041763"},{"key":"2250_CR4","unstructured":"J. Bhadra, A. Martin, J. Abraham, and M. Abadir, \u201cUsing abstract specifications to verify PowerPCTM custom memories by symbolic trajectory evaluation,\u201d in Proceedings of the Advanced Research Working Conference on Correct Hardware Design and Verification Methods, LNCS Vol. 2144, Springer-Verlag 2001, pp. 386\u2013402."},{"key":"2250_CR5","doi-asserted-by":"crossref","unstructured":"J. Bhadra, A. Martin, J. Abraham, and M. Abadir, \u201cA language formalism for verification of PowerPCTM custom memories using compositions of abstract specifications,\u201d in Proceedings of The IEEE High Level Design Validation and Test Workshop, 2001, pp. 134\u2013141.","DOI":"10.1109\/HLDVT.2001.972820"},{"key":"2250_CR6","doi-asserted-by":"crossref","unstructured":"M. Bruer and A. Friedman, Diagnosis and Reliable Design of Digital Systems, Computer Science, Woodland Hills, CA, 1976.","DOI":"10.1007\/978-3-642-95424-5"},{"issue":"8","key":"2250_CR7","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, \u201cGraph-based algorithms for Boolean function manipulation,\u201d IEEE Transactions on Computers, Vol. 35, No. 8, pp. 677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"issue":"4","key":"2250_CR8","doi-asserted-by":"crossref","first-page":"618","DOI":"10.1109\/TCAD.1987.1270309","volume":"6","author":"R.E. Bryant","year":"1987","unstructured":"R.E. Bryant, \u201cAlgorithmic aspects of symbolic switch network analysis,\u201d IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 6, No. 4, pp. 618\u2013633, 1987.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"issue":"4","key":"2250_CR9","doi-asserted-by":"crossref","first-page":"634","DOI":"10.1109\/TCAD.1987.1270310","volume":"6","author":"R.E. Bryant","year":"1987","unstructured":"R.E. Bryant, \u201cBoolean analysis of MOS circuits,\u201d IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 6, No. 4, pp. 634\u2013649, 1987.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"2250_CR10","doi-asserted-by":"crossref","unstructured":"R.E. Bryant, \u201cVerification of synchronous circuits by symbolic logic simulation,\u201d in Hardware Specification, Verification, and Synthesis: Mathematical Aspects, Springer-Verlag, 1990, pp. 14\u201324.","DOI":"10.1007\/0-387-97226-9_21"},{"key":"2250_CR11","doi-asserted-by":"crossref","unstructured":"R.E. Bryant and C.-J.H. Seger, \u201cFormal verification of digital circuits using symbolic ternary system models,\u201d in Proceedings of Computer Aided Verification, American Mathematical Society, 1991, pp. 121\u2013146.","DOI":"10.1090\/dimacs\/003\/11"},{"key":"2250_CR12","doi-asserted-by":"crossref","unstructured":"R.E. Bryant and M.N. Velev, \u201cVerification of pipelined microprocessors by comparing memory execution sequences in symbolic simulation,\u201d in Proceedings of Asian Computer Science Conference, ASIAN, LNCS 1345, Springer-Verlag, 1997, pp 18\u201331.","DOI":"10.1007\/3-540-63875-X_40"},{"key":"2250_CR13","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1109\/43.55188","volume":"9","author":"R. Dekker","year":"1990","unstructured":"R. Dekker, F. Beenker, and L. Thijssen, \u201cA realistic fault model and test algorithms for static random access memories,\u201d IEEE Transactions on Computers, Vol. 9, pp. 567\u2013572, 1990.","journal-title":"IEEE Transactions on Computers"},{"key":"2250_CR14","doi-asserted-by":"crossref","unstructured":"N. Ganguly, M.S. Abadir, and M. Pandey, \u201cPowerPC array verification methodology using formal techniques,\u201d in Proceedings of International Test Conference, 1996, pp. 857\u2013864.","DOI":"10.1109\/TEST.1996.557147"},{"key":"2250_CR15","unstructured":"H. Gericke, Lattice Theory, Frederick Ungar Publishing Company, New York, NY, 1966."},{"key":"2250_CR16","unstructured":"J. E. Hopcroft and J.D. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley Publishing Company, Reading, MA, 1979."},{"issue":"1","key":"2250_CR17","doi-asserted-by":"crossref","first-page":"1141","DOI":"10.1109\/TC.1977.1674761","volume":"C-26","author":"J. Knaizuk","year":"1977","unstructured":"J. Knaizuk and C. Hartman, \u201cAn optimal algorithm for testing stuck-at faults in random access memories,\u201d IEEE Transactions on Computers, Vol. C-26, pp. 1141\u20131144, 1977.","journal-title":"IEEE Transactions on Computers"},{"issue":"4","key":"2250_CR18","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1109\/54.895007","volume":"17","author":"N. Krishnamurthy","year":"2000","unstructured":"N. Krishnamurthy, A. Martin, M. Abadir, and J. Abraham, \u201cValidating PowerPCTM microprocessor custom memories,\u201d IEEE Design and Test of Computers, Vol. 17, No. 4, pp. 61\u201376, 2000.","journal-title":"IEEE Design and Test of Computers"},{"key":"2250_CR19","doi-asserted-by":"crossref","unstructured":"C.B. McDonald and R.E. Bryant, \u201cSymbolic timing simulation using cluster scheduling,\u201d in Proceedings of Design Automation Conference, 2000, pp. 254\u2013259.","DOI":"10.1145\/337292.337411"},{"issue":"3","key":"2250_CR20","doi-asserted-by":"crossref","first-page":"458","DOI":"10.1109\/43.913762","volume":"20","author":"C.B. McDonald","year":"2001","unstructured":"C.B. McDonald and R.E. Bryant, \u201cCMOS circuit verification with symbolic switch-level timing simulation,\u201d IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 20, No. 3, pp. 458\u2013474, 2001.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"issue":"3","key":"2250_CR21","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1109\/TC.1979.1675331","volume":"C-28","author":"R. Nair","year":"1979","unstructured":"R. Nair, \u201cAn optimal algorithm for testing stuck-at faults in random access memories,\u201d IEEE Transactions on Computers, Vol. C-28, No. 3, pp. 258\u2013261, 1979.","journal-title":"IEEE Transactions on Computers"},{"key":"2250_CR22","doi-asserted-by":"crossref","unstructured":"H. Oberle and P. Muhmenthaler, \u201cTest pattern development and evaluation for DRAMS with fault simulator RAMISM,\u201d in Proceedings of the International Test Conference, 1991, pp. 548\u2013555.","DOI":"10.1109\/TEST.1991.519717"},{"issue":"7","key":"2250_CR23","doi-asserted-by":"crossref","first-page":"918","DOI":"10.1109\/43.771176","volume":"18","author":"M. Pandey","year":"1999","unstructured":"M. Pandey and R.E. Bryant, \u201cExploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation,\u201d IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 18, No. 7, pp. 918\u2013935, 1999.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"2250_CR24","doi-asserted-by":"crossref","unstructured":"M. Pandey, R. Raimi, D.L. Beatty, and R.E. Bryant, \u201cFormal verification of PowerPC arrays using symbolic trajectory evaluation,\u201d in Proceedings of Design Automation Conference, 1996, pp. 649\u2013654.","DOI":"10.1145\/240518.240641"},{"key":"2250_CR25","doi-asserted-by":"crossref","unstructured":"M. Pandey, R. Raimi, R.E. Bryant, and M.S. Abadir, \u201cFormal verification of content addressable memories using symbolic trajectory evaluation,\u201d in Proceedings of Design Automation Conference, 1997, pp. 167\u2013172.","DOI":"10.1109\/DAC.1997.597138"},{"key":"2250_CR26","unstructured":"C.-J.H. Seger, \u201cVoss\u2014a formal hardware verification system: User\u2019s Guide,\u201d Technical Report 93-45, Department of Computer Science, University of British Columbia, 1993."},{"issue":"2","key":"2250_CR27","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J.H. Seger","year":"1995","unstructured":"C.-J.H. Seger and R.E. Bryant, \u201cFormal verification by symbolic evaluation of partially-ordered trajectories,\u201d Formal Methods in System Design, Vol. 6, No. 2, pp. 147\u2013189, 1995.","journal-title":"Formal Methods in System Design"},{"key":"2250_CR28","unstructured":"A. van de Goor, Testing Semiconductor Memories: Theory and Practice, John Wiley and Sons, 1991."},{"key":"2250_CR29","doi-asserted-by":"crossref","unstructured":"M.N. Velev and R.E. Bryant, \u201cEfficient modeling of memory arrays in symbolic ternary simulation,\u201d in Proceedings of The International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS Vol. 1384, Springer-Verlag, 1998, pp. 136\u2013150.","DOI":"10.1007\/BFb0054169"},{"key":"2250_CR30","unstructured":"M.N. Velev, R.E. Bryant, and A. Jain, \u201cEfficient modeling of memory arrays in symbolic simulation,\u201d in Proceedings of Computer-Aided Verification, LNCS Vol. 1254, Springer-Verlag, 1997, pp. 388\u2013399."},{"key":"2250_CR31","doi-asserted-by":"crossref","unstructured":"L.-C. Wang, M.S. Abadir, and N. Krishnamurthy, \u201cAutomatic generation of assertions for formal verification of PowerPCTM microprocessor arrays using symbolic trajectory evaluation,\u201d in Proceedings of The Design Automation Conference, 1998, pp. 534\u2013537.","DOI":"10.1145\/277044.277188"},{"key":"2250_CR32","unstructured":"N.H.E. Weste and K. Eshraghian, Principles of CMOS VLSI Design: A Systems Perspective, Addison-Wesley Publishing Company, Reading, MA, 1993."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-005-2250-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-005-2250-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-005-2250-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T02:12:18Z","timestamp":1735956738000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-005-2250-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,9]]},"references-count":32,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2005,9]]}},"alternative-id":["2250"],"URL":"https:\/\/doi.org\/10.1007\/s10703-005-2250-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2005,9]]}}}