skip to main content
10.1145/1228784.1228885acmconferencesArticle/Chapter ViewAbstractPublication PagesglsvlsiConference Proceedingsconference-collections
Article

Hand-in-hand verification of high-level synthesis

Published: 11 March 2007 Publication History

Abstract

This paper describes a formal verification methodology of high-level synthesis (HLS) process. The abstraction level of the input to HLS is so high compared to thatof the output that the verification has to proceed hand-in-hand with the synthesis process. The HLS verificationis performed in three phases in this work. The verification method is based on equivalence checking of two finite state machines with data-paths(FSMDs). Unlike most reported works that targets the individual phases independently, the proposed method applies to all these three phases. The method is strong enoughto accommodate control structure modification of the original behaviour, application of several code motion techniques during scheduling and register optimization during register allocation. It can also verify the correctness of the controller. A hand-in-hand synthesis and verification tool SAST has been developed and tested for effectiveness on several HLS benchmark circuits.

References

[1]
P. Ashar, S. Bhattacharya, A. Raghunathan, and A. Mukaiyama. Verification of rtl generated from scheduled behavior in a high-level synthesis flow. In Proceedings of the IEEE/ACM ICCAD, pages 517--524, 1998.
[2]
R. Camposano. Path-based scheduling for synthesis. IEEE transactions on computer-Aided Design of Integrated Circuits and Systems, Vol 10 No 1:85--93, Jan. 1991.
[3]
H. Eveking, H. Hinrichsen, and G. Ritter. Automatic verification of scheduling results in high-level synthesis. In Proc. Conf. DATE, pages 59--64, March 1999.
[4]
R. W. Floyd. Assigning meaning to programs. In Proceedings the 19 th Symposium on Applied Mathematics, pages 19--32. American Mathematical Society, 1967. Mathematical Aspects of Computer Science.
[5]
D. Gajski and L. Ramachandran. Introduction to high-level synthesis. IEEE transactions on Design and Test of Computers, pages 44--54, 1994.
[6]
S. Gupta, N. Dutt, R. Gupta, and A. Nicolau. Using global code motions to improve the quality of results for high-level synthesis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 23(2):302--312, Feb 2004.
[7]
C. A. R. Hoare. An axiomatic basis of computer programming. Commun. ACM, pages 576--580, 1969.
[8]
C. Karfa, C. Mandal, D. Sarkar, S. Pentakota, and C. Reade. A formal verification method of scheduling in high-level synthesis. In Proc. ISQED'06, pages 71--78, March 2006.
[9]
Y. Kim, S. Kopuri, and N. Mansouri. Automated formal verification of scheduling process using finite state machine with datapath (FSMD). In Proc. Conf.ISQED 2004), pages 110--115, March 2004.
[10]
C. Mandal and R. M. Zimmer. A genetic algorithm for the synthesis of structured data paths. In 13th International Conference on VLSI Design, pages 206--211, 2000.
[11]
N. Mansouri and R. Vemuri. A methodology for automated verification of synthesized rtl designs and its integration with a high-level synthesis tool. In In Proceedings of FMCAD, pages 204--221, 1998.
[12]
D. Sarkar and S. De Sarkar. Some inference rules for integer arithmetic for verification of flowchart programs on integers. IEEE Trans Software. Engg., 15(1):1--9, 1989.

Cited By

View all
  • (2022)BLAST: Belling the Black-Hat High-Level Synthesis ToolIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2022.320051341:11(3661-3672)Online publication date: Nov-2022
  • (2022)FastSim: A Fast Simulation Framework for High-Level SynthesisIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2021.309033941:5(1371-1385)Online publication date: May-2022
  • (2022)DEEQ: Data-driven End-to-End EQuivalence Checking of High-level Synthesis2022 23rd International Symposium on Quality Electronic Design (ISQED)10.1109/ISQED54688.2022.9806218(64-70)Online publication date: 6-Apr-2022
  • Show More Cited By

Index Terms

  1. Hand-in-hand verification of high-level synthesis

    Recommendations

    Comments

    Information & Contributors

    Information

    Published In

    cover image ACM Conferences
    GLSVLSI '07: Proceedings of the 17th ACM Great Lakes symposium on VLSI
    March 2007
    626 pages
    ISBN:9781595936059
    DOI:10.1145/1228784
    Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

    Sponsors

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Publication History

    Published: 11 March 2007

    Permissions

    Request permissions for this article.

    Check for updates

    Author Tags

    1. FSMD model
    2. equivalence checking
    3. formal verification
    4. high-level synthesis

    Qualifiers

    • Article

    Conference

    GLSVLSI07
    Sponsor:
    GLSVLSI07: Great Lakes Symposium on VLSI 2007
    March 11 - 13, 2007
    Stresa-Lago Maggiore, Italy

    Acceptance Rates

    Overall Acceptance Rate 312 of 1,156 submissions, 27%

    Upcoming Conference

    GLSVLSI '25
    Great Lakes Symposium on VLSI 2025
    June 30 - July 2, 2025
    New Orleans , LA , USA

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)4
    • Downloads (Last 6 weeks)1
    Reflects downloads up to 27 Jan 2025

    Other Metrics

    Citations

    Cited By

    View all
    • (2022)BLAST: Belling the Black-Hat High-Level Synthesis ToolIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2022.320051341:11(3661-3672)Online publication date: Nov-2022
    • (2022)FastSim: A Fast Simulation Framework for High-Level SynthesisIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2021.309033941:5(1371-1385)Online publication date: May-2022
    • (2022)DEEQ: Data-driven End-to-End EQuivalence Checking of High-level Synthesis2022 23rd International Symposium on Quality Electronic Design (ISQED)10.1109/ISQED54688.2022.9806218(64-70)Online publication date: 6-Apr-2022
    • (2021)HOST: HLS Obfuscations against SMT ATtack2021 Design, Automation & Test in Europe Conference & Exhibition (DATE)10.23919/DATE51398.2021.9473927(32-37)Online publication date: 1-Feb-2021
    • (2017)PRESGenProceedings of the 2017 Workshop on Software Engineering Methods for Parallel and High Performance Applications10.1145/3085158.3086158(13-20)Online publication date: 26-Jun-2017
    • (2012)Translation validation for PRES+ models of parallel behaviours via an FSMD equivalence checkerProceedings of the 16th international conference on Progress in VLSI Design and Test10.1007/978-3-642-31494-0_9(69-78)Online publication date: 1-Jul-2012
    • (2008)Automated formal verification of scheduling with speculative code motionsProceedings of the 18th ACM Great Lakes symposium on VLSI10.1145/1366110.1366134(95-100)Online publication date: 4-May-2008
    • (2008)An Equivalence-Checking Method for Scheduling Verification in High-Level SynthesisIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2007.91339027:3(556-569)Online publication date: 1-Mar-2008

    View Options

    Login options

    View options

    PDF

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader

    Figures

    Tables

    Media

    Share

    Share

    Share this Publication link

    Share on social media