Formal Verification of GCSE in the Scheduling of High-level Synthesis: Work-in-Progress

被引:4
作者
Hu, Jian [1 ]
Hu, Yongyang [1 ]
Yu, Long [1 ]
Wang, Wentao [2 ]
Yang, Haitao [1 ]
Kang, Yun [1 ]
Cheng, Jie [1 ]
机构
[1] Natl Univ Def Technol, Res Inst 63, Nanjing, Peoples R China
[2] Natl Univ Def Technol, Coll Comp Sci & Technol, Changsha, Peoples R China
来源
PROCEEDINGS OF THE 2020 INTERNATIONAL CONFERENCE ON HARDWARE/SOFTWARE CODESIGN AND SYSTEM SYNTHESIS (CODES+ISSS) | 2019年
基金
中国国家自然科学基金;
关键词
Equivalence Checking; High-level Synthesis; FSMD; Global Common Subexpression Elimination;
D O I
10.1109/codesisss51650.2020.9244039
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
High-level synthesis entails application of a sequence of transformations to compile a high-level description of a hardware design (e.g., in C/C++/SystemC) into a register-transfer level (RTL) implementation. However, an error may exist in the RTL implementation from the compiler in the high-level synthesis due to the complex and error prone compiling process. Global common subexpression elimination (GCSE) is a commonly used code motion technique in the scheduling of high-level synthesis. In this paper, we present an equivalence checking method to verify GCSE in the scheduling of high-level synthesis by enhancing the path equivalence criteria. The initial experimental results demonstrate our method can indeed verify the GCSE which has not been properly addressed in the past.
引用
收藏
页码:1 / 2
页数:2
相关论文
共 8 条
  • [1] Verification of Code Motion Techniques Using Value Propagation
    Banerjee, Kunal
    Karfa, Chandan
    Sarkar, Dipankar
    Mandal, Chittaranjan
    [J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2014, 33 (08) : 1180 - 1193
  • [2] Chi-Hui Lee, 2011, 2011 16th Asia and South Pacific Design Automation Conference, ASP-DAC 2011, P497, DOI 10.1109/ASPDAC.2011.5722241
  • [3] Translation Validation of Loop Invariant Code Optimizations Involving False Computations
    Chouksey, Ramanuj
    Karfa, Chandan
    Bhaduri, Purandar
    [J]. VLSI DESIGN AND TEST, 2017, 711 : 767 - 778
  • [4] SPARK: A high-level synthesis framework for applying parallelizing compiler transformations
    Gupta, S
    Dutt, N
    Gupta, R
    Nicolau, A
    [J]. 16TH INTERNATIONAL CONFERENCE ON VLSI DESIGN, PROCEEDINGS, 2003, : 461 - 466
  • [5] An equivalence-checking method for scheduling verification in high-level synthesis
    Karfa, Chandan
    Sarkar, Dipankar
    Mandal, Chittaranjan
    Kumar, Pramod
    [J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2008, 27 (03) : 556 - 569
  • [6] Panda P. R., 1995, Proceedings of the Eighth International Symposium on System Synthesis (IEEE Cat. No.95TH8050), P170, DOI 10.1109/ISSS.1995.520630
  • [7] GLOBAL SCHEDULING WITH CODE-MOTIONS FOR HIGH-LEVEL SYNTHESIS APPLICATIONS
    RIM, M
    FANN, Y
    JAIN, R
    [J]. IEEE TRANSACTIONS ON VERY LARGE SCALE INTEGRATION (VLSI) SYSTEMS, 1995, 3 (03) : 379 - 392
  • [8] US