caa a22 4500 475797442 CHVBK 20180406123728.0 cr unu---uuuuu 170329e20000101xx s 000 0 eng 10.1023/A:1008777509016 doi (NATIONALLICENCE)springer-10.1023/A:1008777509016 Automated Correctness Condition Generation for Formal Verification of Synthesized RTL Designs [Elektronische Daten] [Nazanin Mansouri, Ranga Vemuri] High-level synthesis tools generate register-transfer level designs from algorithmic behavioral specifications. The high-level synthesis process typically consists of dependency graph scheduling, functional unit allocation, register allocation, interconnect allocation and controller generation tasks. Widely used algorithms for these tasks retain the overall control flow structure of the behavioral specification allowing code motion only within basic blocks. Further, high-level synthesis algorithms are oblivious to the mathematical properties of arithmetic and logic operators. Selecting and sharing of RTL library modules are solely based on matching uninterpreted function symbols and constants. Many researchers have noted that these features of high-level synthesis algorithms can be exploited to develop efficient verification strategies for synthesized designs. This paper reports a verification technique that effectively exploits these features to achieve efficient and fully automated verification of synthesized designs and its incorporation in a high-level synthesis tool. In our technique, a correctness condition generator is tightly integrated with a high-level synthesis tool to automatically generate (1) formal specifications of the behavior and the RTL design including the data path and the controller, (2) the correctness lemmas establishing equivalence between the synthesized RTL design and its behavioral specification, and (3) their proof scripts that can be submitted to a higher-order logic proof checker without further human interaction. This approach is based on the identification, by the synthesis tool during the synthesis process, of the binding between critical specification variables and critical registers in the RTL design, and between the critical states in the behavior and the corresponding states in the RTL design. We have implemented our verification technique in conjunction with a relatively mature high-level synthesis tool. We report experimental results indicating the effectiveness of the proposed technique and summarize our ongoing work to further strengthen it. Kluwer Academic Publishers, 2000 correctness conditions nationallicence high-level synthesis nationallicence RT-level verification nationallicence formal synthesis nationallicence theorem proving nationallicence Mansouri Nazanin Digital Design Environments Laboratory, ECECS Department, University of Cincinnati, 45221-0030, Cincinnati, Ohio, USA aut Vemuri Ranga Digital Design Environments Laboratory, ECECS Department, University of Cincinnati, 45221-0030, Cincinnati, Ohio, USA aut Formal Methods in System Design Kluwer Academic Publishers 16/1(2000-01-01), 59-91 0925-9856 16:1<59 2000 16 10703 https://doi.org/10.1023/A:1008777509016 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1023/A:1008777509016 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Mansouri Nazanin Digital Design Environments Laboratory, ECECS Department, University of Cincinnati, 45221-0030, Cincinnati, Ohio, USA aut NATIONALLICENCE 700 1- Vemuri Ranga Digital Design Environments Laboratory, ECECS Department, University of Cincinnati, 45221-0030, Cincinnati, Ohio, USA aut NATIONALLICENCE 773 0- Formal Methods in System Design Kluwer Academic Publishers 16/1(2000-01-01), 59-91 0925-9856 16:1<59 2000 16 10703 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer