{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T14:00:03Z","timestamp":1754488803927,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651918"},{"type":"electronic","value":"9783540495192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49519-3_15","type":"book-chapter","created":{"date-parts":[[2007,10,20]],"date-time":"2007-10-20T10:37:12Z","timestamp":1192876632000},"page":"204-221","source":"Crossref","is-referenced-by-count":6,"title":["A Methodology for Automated Verification of Synthesized RTL Designs and Its Integration with a High-Level Synthesis Tool"],"prefix":"10.1007","author":[{"given":"Nazanin","family":"Mansouri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ranga","family":"Vemuri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"15_CR1","unstructured":"G. De Micheli, \u201cSynthesis and Optimization of Digital Circuits\u201d, McGraw-Hill, 1994."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"D.E. Thomas et al., \u201cAlgorithmic and Register Transfer Level Synthesis: The System Architect\u2019s Workbench\u201d, Kluwer Academic Publishers, 1990.","DOI":"10.1007\/978-1-4613-1519-3"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Srinivas Devadas, Hi-Keung Tony Ma, Richard Newton, \u201cOn Verification of Sequential Machines at Differing Levels of Abstraction\u201d, IEEE Transactions on Computer-Aided Design, June 1988.","DOI":"10.1109\/43.3210"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Michael McFarland, \u201cAn Abstract Model of Behavior for Hardware Descriptions\u201d, IEEE Transactions on Computers, July 1983.","DOI":"10.1109\/TC.1983.1676294"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"F. Corella, R. Camposano, R. Bergamaschi, M. Payer, \u201cVerification of Synchronous Sequential Circuits Obtained from Algorithmic Specifications,\u201d Proc. Intl. Workshop on Formal Methods in VLSI Design, Miami, 1991.","DOI":"10.1016\/B978-0-444-89208-9.50019-3"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Reinaldo A. Bergamaschi, Salil Raje, \u201cObservable Time Windows: Verifying The Results of High-Level Synthesis\u201d, IEEE Design & Test of Computers\u201d, May 1997.","DOI":"10.1109\/54.587740"},{"key":"15_CR7","volume-title":"Synthesis of Digital Designs from Recursion Equations","author":"S. Johnson","year":"1984","unstructured":"Steven Johnson, \u201cSynthesis of Digital Designs from Recursion Equations\u201d, MIT Press, Cambridge, 1984."},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Ranga Vemuri, \u201cOn the Notion of Normal Form Register-Level Structures and Its Applications in Design-Space Exploration\u201d, European Design Automation Conference, March 1990.","DOI":"10.1109\/EDAC.1990.136618"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"F. Feldbusch, R. Kumar, \u201cVerification of Synthesized Circuits at Register Transfer Level with Flow Graphs,\u201d Proc. IEEE EDAC Conf., pp. 22\u201326, 1991.","DOI":"10.1109\/EDAC.1991.206351"},{"key":"15_CR10","unstructured":"Sreeranga Rajan, \u201cCorrectness Transformations in High Level Synthesis: Formal Verification\u201d, Proceedings of the International Conference on Computer Hardware Description Languages, Japan, August 1995."},{"key":"15_CR11","unstructured":"N. Shankar, S. Owre and J. M. Rushby, \u201cThe PVS Proof Checker: A Reference Manual (Beta Release)\u201d, March 1993."},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Dirk Eisnbiegler, Ramayya Kumar, \u201cFormally Embedding Existing High Level Synthesis Algorithms\u201d, \u201cCorrect Hardware Design and Verification Methods\u201d, Germany, October 1995.","DOI":"10.1007\/3-540-60385-9_5"},{"key":"15_CR13","unstructured":"Luc Claesen, Mark Genoe, Eric Verlind, Frank Proesmans, Hugo De Man, \u201cSFG-Tracing: A Methodology of Design for Verifiability\u201d, Proceedings of Advanced Workshop on Correct Hardware Design Methodologies, North-Holland, 1991."},{"key":"15_CR14","unstructured":"Luc Claesen, Frank Proesmans, Eric Verlind, Hugo De Man, \u201cSFG-Tracing: A Methodology for the Automatic Verification of MOS Transistor Level Implementations from High-Level Behavioral Specifications\u201d, Proc. Intl. Workshop on Formal Methods in VLSI Design, Miami, 1991."},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Francisco Corella, \u201cAutomated High-Level Verification Against Clocked Algorithmic Specifications,\u201d Proc. Computer Hardware Description Languages and Their Applications, April 1993.","DOI":"10.1016\/B978-0-444-81641-2.50017-4"},{"key":"15_CR16","unstructured":"Francisco Corella, \u201cAutomated Verification of Behavioral Equivalence for Microprocessors\u201d, Research Report, IBM Research division, T.J. Watson Research Center, 1992."},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Jerry R. Burch and David L. Dill, \u201cAutomatic Verification of Pipelined Microprocessor Control\u201d, Proceedings of Computer-Aided Verification, July 1994.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"M. K. Srivas and S. P. Miller, \u201cFormal Verification of the AAMP5 Microprocessor,\u201d Chapter 7 in Industrial Applications of Formal Verification.","DOI":"10.1109\/52.57892"},{"key":"15_CR19","unstructured":"A. Takach and W. Wolf, \u201cScheduling Constraint Generation for Communicating Processes\u201d, Princeton University, November 1993."},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"D. E. Thomas, R. L. Blackburn, and J. V. Rajan, \u201cLinking the Behavioral and Structural Domains of Representation for Digital System Design\u201d, IEEE Trans. CAD, vol. CAD-6, pp. 103\u2013110, January 1987.","DOI":"10.1109\/TCAD.1987.1270252"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"F. J. Kurdahi, A. C. Parker, \u201cREAL: A Program for REgister ALlocation\u201d, Proceedings of the 24th ACM\/IEEE Design Automation Conference, pp. 210\u2013215, 1987.","DOI":"10.1145\/37888.37920"},{"key":"15_CR22","unstructured":"S. Owre, N. Shankar, J. M. Rushby, \u201cThe PVS Specification Language (Beta Release)\u201d, June 1993."},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"J. Roy, N. Kumar, R. Dutta, R. Vemuri, \u201cDSS: A Distributed High-Level Synthesis System\u201d, IEEE Design and Test of Computers, June 1992.","DOI":"10.1109\/54.143143"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"R. Dutta, J. Roy, R. Vemuri, \u201cDistributed Design Space Exploration for High-Level Synthesis Systems\u201d, 29th Design Automation Conference, pp. 644\u2013650, 1992.","DOI":"10.1109\/DAC.1992.227806"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Sriram Govindarajan, Ranga Vemuri, \u201cDynamic Bounding of Successor Force Computations in the Force Directed List Scheduling Algorithm\u201d, International Conference on Computer Design (ICCD), October 1997.","DOI":"10.1109\/ICCD.1997.628949"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Sriram Govindarajan, Ranga Vemuri, Cone-Based Clustering Heuristic for List Scheduling Algorithms, Proceedings of the European Design and Test Conference, pp. 456\u2013462., (ED&TC), March 1997.","DOI":"10.1109\/EDTC.1997.582400"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Srinivas Katkoori, Jay Roy, Ranga Vemuri, \u201cA Hierarchical Register Optimization Algorithm for Behavioral Synthesis\u201d, Proceedings of International Conference on VLSI Design, pp. 126\u2013134, Banglore, India 1996.","DOI":"10.1109\/ICVD.1996.489471"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"R. Vemuri et al, \u201cExperiences in Functional Validation of a High Level Synthesis System\u201d, 30th ACM\/IEEE Design Automation Conference, 1993.","DOI":"10.1145\/157485.164667"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A. Emerson, A.P. Sistla, \u201cAutomatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications\u201d, ACM Trans. Prog. Lang. Syst., pp. 244\u2013263, 1986.","DOI":"10.1145\/5397.5399"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"N. Narasimhan, R. Vemuri, \u201cSpecification of Control Flow Properties for Verification of Synthesized VHDL Designs\u201d, \u201cProceedings of Formal Methods in CAD\u201d, pp. 327\u2013345, Springer-Verlag, November 1996.","DOI":"10.1007\/BFb0031819"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Kenneth L. McMillan, \u201cSymbolic Model Checking: An Approach to the State Explosion Problem\u201d Carnegie Mellon University, 1992.","DOI":"10.1007\/978-1-4615-3190-6_3"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49519-3_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T19:50:43Z","timestamp":1737489043000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49519-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651918","9783540495192"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-49519-3_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}