{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:58:21Z","timestamp":1759147101017,"version":"3.43.0"},"reference-count":56,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2000,1]]},"DOI":"10.1023\/a:1008777509016","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"59-91","source":"Crossref","is-referenced-by-count":7,"title":["Automated Correctness Condition Generation for Formal Verification of Synthesized RTL Designs"],"prefix":"10.1007","volume":"16","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","reference":[{"key":"243847_CR1","unstructured":"M. Aagaard and M. Leeser, \u201cA formally verified system for logic synthesis,\u201d Proceedings of 1991 IEEE International Conference on Computer Design, 1991."},{"key":"243847_CR2","doi-asserted-by":"crossref","unstructured":"M. Aagaard, M. Leeser, and P. Windley, \u201cTowards a super duper hardware tactic,\u201d HOL Theorem Proving System and its Applications, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57826-9_151"},{"key":"243847_CR3","unstructured":"S. Basse, Computer Algorithms, Addison-Wesley, 1978."},{"key":"243847_CR4","doi-asserted-by":"crossref","unstructured":"R.A. Bergamaschi and S. Rajel, \u201cObservable time windows: verifying the results of high-level synthesis,\u201d IEEE Design & Test of Computers, 1997.","DOI":"10.1109\/54.587740"},{"key":"243847_CR5","unstructured":"R.E. Bryant, \u201cSymbolic boolean manipulation with ordered binary decision diagrams,\u201d Technical Report CMU-CS-92-160, School of Computer Science, Carnegie Mellon University, 1992."},{"key":"243847_CR6","unstructured":"R.E. Bryant, \u201cBinary decision diagrams and beyond: enabling technologies for formal verification,\u201d Embedded Tutorial at International Conference on Computer-Aided Design, 1995."},{"key":"243847_CR7","doi-asserted-by":"crossref","unstructured":"J.R. Burch and D.L. Dill, \u201cAutomatic verification of pipelined microprocessor control,\u201d Proceedings of Computer-Aided Verification, 1994.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"243847_CR8","doi-asserted-by":"crossref","unstructured":"R. Camposano and W. Wolf, High-Level VLSI Synthesis, Kluwer Academic Publishers, 1991.","DOI":"10.1007\/978-1-4615-3966-7"},{"key":"243847_CR9","unstructured":"L. Claesen, M. Genoe, E. Verlind, F. Proesmans, and H.D. Man, \u201cSFG-tracing: a methodology of design for verifiability,\u201d Proceedings of Advanced Workshop on Correct Hardware Design Methodologies, 1991."},{"key":"243847_CR10","unstructured":"L. Claesen, F. Proesmans, E. Verlind, and H.D. Man, \u201cSFG-tracing: a methodology for the automatic veri-fication of MOS transistor level implementations from high-level behavioral specifications,\u201d Proceedings of International Workshop on Formal Methods in VLSI Design, 1991."},{"key":"243847_CR11","doi-asserted-by":"crossref","unstructured":"E. Clarke, E. Emerson, and A. Sistla, \u201cAutomatic verification of finite-state concurrent systems using temporal logic specifications,\u201d ACM Transactions on Prog. Lang. Syst., 1986.","DOI":"10.1145\/5397.5399"},{"key":"243847_CR12","unstructured":"F. Corella, \u201cAutomated verification of behavioral equivalence for microprocessors,\u201d Research Report, IBM Research division, T.J. Watson Research Center, 1992."},{"key":"243847_CR13","doi-asserted-by":"crossref","unstructured":"F. Corella, \u201cAutomated high-level verification against clocked algorithmic specifications,\u201d Proceedings of Computer Hardware Description Languages and Their Applications, 1993.","DOI":"10.1016\/B978-0-444-81641-2.50017-4"},{"key":"243847_CR14","doi-asserted-by":"crossref","unstructured":"F. Corella, R. Camposano, R. Bergamaschi, and M. Payer, \u201cVerification of synchronous sequential circuits obtained from algorithmic specifications,\u201d Proceedings of International Workshop on Formal Methods in VLSI Design, 1991.","DOI":"10.1016\/B978-0-444-89208-9.50019-3"},{"key":"243847_CR15","unstructured":"G. De-Micheli, Synthesis and Optimization of Digital Circuits, McGraw-Hill, 1994."},{"key":"243847_CR16","unstructured":"R. Dutta, J. Roy, and R. Vemuri, \u201cDistributed design space exploration for high-level synthesis systems,\u201d 29th Design Automation Conference, 1992."},{"key":"243847_CR17","doi-asserted-by":"crossref","unstructured":"D. Eisnbiegler and R. Kumar, \u201cFormally embedding existing high level synthesis algorithms,\u201d Correct Hardware Design and Verification Methods, Springer, 1995.","DOI":"10.1007\/3-540-60385-9_5"},{"key":"243847_CR18","unstructured":"F. Feldbusch and R. Kumar, \u201cVerification of synthesized circuits at register transfer level with flow graphs,\u201d Proceedings of IEEE European Design Automation Conference, 1991."},{"key":"243847_CR19","doi-asserted-by":"crossref","unstructured":"D. Gajski, N. Dutt, A. Wu, and S. Lin, High-Level Synthesis, Introduction to Chip and System Design, Kluwer Academic Publishers, 1992.","DOI":"10.1007\/978-1-4615-3636-9"},{"key":"243847_CR20","unstructured":"S. Govindarajan and R. Vemuri, \u201cCone-based clustering heuristic for list scheduling algorithms,\u201d Proceedings of the European Design and Test Conference, 1997."},{"key":"243847_CR21","unstructured":"S. Govindarajan and R. Vemuri, \u201cDynamic bounding of successor force computations in the force directed list scheduling algorithm,\u201d Proceedings of International Conference on Computer Design, 1997."},{"key":"243847_CR22","doi-asserted-by":"crossref","unstructured":"D. Greve, \u201cSymbolic simulation of the JEM1 microprocessor,\u201d Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design, 1998.","DOI":"10.1007\/3-540-49519-3_21"},{"key":"243847_CR23","doi-asserted-by":"crossref","unstructured":"W. Hunt, FM8501: A Verified Microprocessor, Springer-Verlag, 1994.","DOI":"10.1007\/3-540-57960-5"},{"key":"243847_CR24","unstructured":"S. Johnson, Synthesis of Digital Designs from Recursion Equations, MIT Press, 1984."},{"key":"243847_CR25","unstructured":"S. Katkoori, J. Roy, and R. Vemuri, \u201cA hierarchical register optimization algorithm for behavioral synthesis,\u201d Proceedings of International Conference on VLSI Design, 1996."},{"key":"243847_CR26","unstructured":"D.W. Knapp, Behavioral Synthesis: Digital System Design Using the Synopsys Behavioral Compiler, Prentice Hall, 1996."},{"key":"243847_CR27","doi-asserted-by":"crossref","unstructured":"T. Kropf, K. Schneider, and R. Kumar, \u201cA formal framework for high level synthesis,\u201d Theorem Provers in Circuit Design, Springer-Verlag, 1994.","DOI":"10.1007\/3-540-59047-1_51"},{"key":"243847_CR28","doi-asserted-by":"crossref","unstructured":"F. Kurdahi and A. Parker, \u201cREAL: A program for REgister ALlocation,\u201d 24th Design Automation Conference, 1987.","DOI":"10.1145\/37888.37920"},{"key":"243847_CR29","doi-asserted-by":"crossref","unstructured":"N. Mansouri and R. Vemuri, \u201cA methodology for completely automated verification of synthesized RTL designs and its integration with a high-level synthesis tool,\u201d Proceedings of International Conference on Formal Methods in Computer-Aided Design, 1998.","DOI":"10.1007\/3-540-49519-3_15"},{"key":"243847_CR30","doi-asserted-by":"crossref","unstructured":"M. McFarland, \u201cAn abstract model of behavior for hardware descriptions,\u201d IEEE Transactions on Computers, 1983.","DOI":"10.1109\/TC.1983.1676294"},{"key":"243847_CR31","unstructured":"K.L. McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem, Carnegie Mellon University, 1992."},{"key":"243847_CR32","unstructured":"J.S. Moore, \u201cSymbolic simulation: an ACL2 approach,\u201d Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design, 1998."},{"key":"243847_CR33","doi-asserted-by":"crossref","unstructured":"N. Narasimhan, E. Teica, R. Radhakrishnan, S. Govindarajan, and R. Vemuri, \u201cTheorem proving guided development of formal assertions in a resource-constrained scheduler for high-level synthesis,\u201d Proceedings of International Conference on Computer Design (ICCD'98), 1998, pp. 392\u2013399.","DOI":"10.1109\/ICCD.1998.727079"},{"key":"243847_CR34","doi-asserted-by":"crossref","unstructured":"N. Narasimhan and R. Vemuri, \u201cSpecification of control flow properties for verification of synthesized VHDL designs,\u201d Proceedings of International Conference in Formal Methods in Computer Aided Design, 1996.","DOI":"10.1007\/BFb0031819"},{"key":"243847_CR35","unstructured":"N. Narasimhan and R. Vemuri, \u201cSynchronous controller models for synthesis from communicating VHDL processes,\u201d Ninth International Conference on VLSI Design, 1996."},{"key":"243847_CR36","doi-asserted-by":"crossref","unstructured":"N. Narasimhan and R. Vemuri, \u201cOn the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a high-level synthesis system,\u201d Proceedings of 11th Conference on Theorem Proving in Higher Order Logics (TPHOL'98), 1998.","DOI":"10.1007\/BFb0055147"},{"key":"243847_CR37","unstructured":"S. Owre, N. Shankar, and J.M. Rushby, \u201cThe PVS specification language (beta release),\u201d 29th Design Automation Conference, 1992."},{"key":"243847_CR38","doi-asserted-by":"crossref","unstructured":"P. Pualin, J. Knight, and E. Girczyck, \u201cHAL: a multi-paradigm approach to automatic data path synthesis,\u201d 24th ACM\/IEEE Desgin Automation Conference, 1986.","DOI":"10.1109\/DAC.1986.1586099"},{"key":"243847_CR39","unstructured":"S. Rajan, \u201cCorrectness transformations in high level synthesis: formal verification,\u201d Proceedings of the International Conference on Computer Hardware Description Languages, 1995."},{"key":"243847_CR40","doi-asserted-by":"crossref","unstructured":"S. Rajan, J. Joyce, and C. Seger, \u201cFrom abstract data types to shift registers: a case study in formal specification and verification at differing levels of abstraction using theorem proving and symbolic simulation,\u201d 6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, 1993.","DOI":"10.1007\/3-540-57826-9_158"},{"key":"243847_CR41","doi-asserted-by":"crossref","unstructured":"J. Roy, N. Kumar, R. Dutta, and R. Vemuri, \u201cDSS: a distributed high-level synthesis system,\u201d IEEE Design and Test of Computers, 1992.","DOI":"10.1109\/54.143143"},{"key":"243847_CR42","doi-asserted-by":"crossref","unstructured":"S. Devadas, T. Ma, and R. Newton, \u201cOn verification of sequential machines at differing levels of abstraction,\u201d IEEE Transactions on Computer-Aided Design, 1988.","DOI":"10.1109\/43.3210"},{"key":"243847_CR43","unstructured":"N. Shankar, S. Owre, and J.M. Rushby, The PVS Proof Checker: A Reference Manual (Beta Release), 1993."},{"key":"243847_CR44","unstructured":"M.K. Srivas and S.P. Miller, \u201cFormal verification of the AAMP5 microprocessor,\u201d Applications of Formal Methods, Prentice Hall International, 1995."},{"key":"243847_CR45","unstructured":"L. Stok and R.V.D. Born, \u201cEasy: multiprocessor architecture optimiztion,\u201d Proceedings of International Workshop on Logic and Architecture Synthesis for Silicon Compilers, 1998."},{"key":"243847_CR46","unstructured":"A. Takach and W. Wolf, Scheduling Constraint Generation for Communicating Processes, Princeton University, 1993."},{"key":"243847_CR47","doi-asserted-by":"crossref","unstructured":"D. Thomas, C.Y. H. III, T. Kowalski, J. Rajan, and A. Walker, \u201cAutomatic data path synthesis,\u201d IEEE Transactions on Computers, 1983.","DOI":"10.1109\/MC.1983.1654268"},{"key":"243847_CR48","doi-asserted-by":"crossref","unstructured":"D. Thomas, E. Lagnese, R. Walker, J. Nestor, J. Rajan, and R. Blackburn, Algorithmic and Register Transfer Level Synthesis: The System Architect's Workbench, Kluwer Academic Publishers, 1990.","DOI":"10.1007\/978-1-4613-1519-3"},{"key":"243847_CR49","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 Transactions on Computer Aided Design, 1987.","DOI":"10.1109\/TCAD.1987.1270252"},{"key":"243847_CR50","unstructured":"C. Tseng and D.P. Siewiorek, \u201cFacet: a procedure for the automated synthesis of digital systems,\u201d 20th ACM\/IEEE Design Automation Conference, 1983."},{"key":"243847_CR51","unstructured":"R. Vemuri, \u201cOn the notion of normal form register-level structures and its applications in design-space exploration,\u201d Proceedings of IEEE European Design Automation Conference, 1990."},{"key":"243847_CR52","doi-asserted-by":"crossref","unstructured":"R. Vemuri, P. Mamtora, P. Sinha, N. Kumar, and J.R.R. Vutukuru, \u201cExperiences in functional validation of a high level synthesis system,\u201d Proceedings of 30th ACM\/IEEE Design Automation Conference, 1993.","DOI":"10.1145\/157485.164667"},{"key":"243847_CR53","doi-asserted-by":"crossref","unstructured":"R. Walker and R. Camposano, A Survey of High-Level Synthesis Systems, Kluwer Academic Publishers, 1990.","DOI":"10.1007\/978-1-4615-3968-1"},{"key":"243847_CR54","unstructured":"P. Windley, The Practical Verification of Microprocessor Designs, Compcon, 1991."},{"key":"243847_CR55","unstructured":"P.J. Windley, \u201cVerifying pipelined microprocessors,\u201d Proceedings of the International Conference on Computer Hardware Description Languages, 1995."},{"key":"243847_CR56","doi-asserted-by":"crossref","unstructured":"N. Woo, \u201cA global, dymanic register allocation and binding for data path synthesis system,\u201d 27th Design Automation Conference, 1990.","DOI":"10.1145\/123186.123384"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008777509016.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008777509016\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008777509016.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:25:10Z","timestamp":1754367910000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008777509016"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,1]]},"references-count":56,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2000,1]]}},"alternative-id":["243847"],"URL":"https:\/\/doi.org\/10.1023\/a:1008777509016","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2000,1]]}}}