Validating GCSE in the scheduling of high-level synthesis

High-level synthesis (HLS) compiles a algorithmic description (C or C++) into a digital hardware implementation (VHDL or Verilog) through a sequence of transformations. However, the complex compiling process may introduce an error in the produced register-transfer level (RTL) implementation. Global...

Full description

Saved in:
Bibliographic Details
Main Authors: Hu, Jian, Hu, Yongyang, Yu, Long, Yang, Haitao, Kang, Yun, Cheng, Jie
Format: Conference Proceeding
Language:English
Subjects:
Automata
Computational modeling
Convergence
Equivalence Checking
FSMD
Global Common Subexpression Elimination
High-level Synthesis
Merging
Processor scheduling
Resource management
Scheduling
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:High-level synthesis (HLS) compiles a algorithmic description (C or C++) into a digital hardware implementation (VHDL or Verilog) through a sequence of transformations. However, the complex compiling process may introduce an error in the produced register-transfer level (RTL) implementation. Global common subexpression elimination (GCSE) as a commonly used code motion technique in the scheduling of HLS is an error-prone and complex process that need to be validated. In this paper, we propose an equivalence checking method to validate GCSE with non-common variables used in the rest code in the scheduling of HLS by enhancing the path equivalence criteria. The source and target programs are modeled using Finite State Machine with Datapath (FSMD) that is essentially a Control and Data Flow Graph (CDFG). The experimental results show that our method can indeed validate the GCSE with non-common variables used in the rest code in HLS which has not been solved in the existing papers.
ISSN:2377-5386
DOI:10.1109/ATS49688.2020.9301546