{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T05:40:46Z","timestamp":1737006046191,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425410"},{"type":"electronic","value":"9783540447986"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44798-9_30","type":"book-chapter","created":{"date-parts":[[2007,5,3]],"date-time":"2007-05-03T17:16:15Z","timestamp":1178212575000},"page":"386-402","source":"Crossref","is-referenced-by-count":3,"title":["Using Abstract Specifications to Verify PowerPC\u2122 Custom Memories by Symbolic Trajectory Evaluation"],"prefix":"10.1007","author":[{"given":"Jayanta","family":"Bhadra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Martin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacob","family":"Abraham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Magdy","family":"Abadir","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"30_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1007\/3-540-63166-6_38","volume-title":"CAV, 1997, Proceedings","author":"M. N. Velev","year":"1997","unstructured":"M. N. Velev, R. E. Bryant, A. Jain. Efficient \u201cModeling of Memory Arrays in Symbolic Simulation\u201d. CAV, 1997, Proceedings. LNCS, Vol. 1254, Springer, 1997, pp. 388\u2013399."},{"doi-asserted-by":"crossref","unstructured":"M. N. Velev, R. E. Bryant. \u201cEfficient Modeling of Memory Arrays in Symbolic Ternary Simulation\u201d. TACAS, 1998.","key":"30_CR2","DOI":"10.1007\/BFb0054169"},{"issue":"4","key":"30_CR3","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/54.895007","volume":"17","author":"N. Krishnamurthy","year":"2000","unstructured":"N. Krishnamurthy, A. K. Martin, M. S. Abadir, J. A. Abraham. \u201cValidating PowerPC Microprocessor Custom Memories\u201d IEEE Design and Test of Computers, Vol. 17, No. 4, Oct-Dec 2000, pp. 61\u201376.","journal-title":"IEEE Design and Test of Computers"},{"doi-asserted-by":"crossref","unstructured":"L.-C. Wang, M. S. Abadir, N. Krishnamurthy. \u201cAutomatic Generation of Assertions for Formal Verification of PowerPC Microprocessor Arrays Using Symbolic Trajectory Evaluation\u201d. 35th ACM\/IEEE DAC, June, 1998.","key":"30_CR4","DOI":"10.1145\/277044.277188"},{"doi-asserted-by":"crossref","unstructured":"R. E. Bryant. \u201cAlgorithmic Aspects of Symbolic Switch Network Analysis\u201d. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 6(4), July 1987.","key":"30_CR5","DOI":"10.1109\/TCAD.1987.1270309"},{"issue":"2","key":"30_CR6","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, 6(2):147\u2013189, March, 1995.","journal-title":"Formal Methods in System Design"},{"unstructured":"J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Publishing Company, 1979, pp. 1\u201345.","key":"30_CR7"},{"doi-asserted-by":"crossref","unstructured":"R. E. Bryant. \u201cGraph-Based Algorithms for Boolean Function Manipulation\u201d. IEEE Transactions on Computers, 35(8), August 1986.","key":"30_CR8","DOI":"10.1109\/TC.1986.1676819"},{"doi-asserted-by":"crossref","unstructured":"R. E. Bryant. \u201cVerifying a Static RAM Design by Logic Simulation\u201d, Fifth MIT Conference on Advanced Research in VLSI, 1988, pp. 335\u2013349.","key":"30_CR9","DOI":"10.7551\/mitpress\/1102.003.0027"},{"doi-asserted-by":"crossref","unstructured":"N. Ganguly, M. S. Abadir, M. Pandey. \u201cPowerPC array verification methodology using formal techniques\u201d. International Test Conference 1996, pp. 857\u2013864.","key":"30_CR10","DOI":"10.1109\/TEST.1996.557147"},{"doi-asserted-by":"crossref","unstructured":"M. Pandey, R. Raimi, D. L. Beatty, R. E. Bryant. \u201cFormal Verification of PowerPC arrays using Symbolic Trajectory Evaluation\u201d. 33rd ACM \/IEEE DAC, June 1996, pp. 649\u2013654.","key":"30_CR11","DOI":"10.1145\/240518.240641"},{"doi-asserted-by":"crossref","unstructured":"M. Pandey, R. Raimi, R. E. Bryant, M. S. Abadir. \u201cFormal Verification of Content Addressable Memories using Symbolic Trajectory Evaluation\u201d. 34th ACM\/IEEE DAC, June 1997.","key":"30_CR12","DOI":"10.1145\/266021.266056"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44798-9_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T00:57:11Z","timestamp":1736989031000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44798-9_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425410","9783540447986"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-44798-9_30","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}