Hardware/Software Co-design and Verification Methodology from System Level Based on System Dependence Graph

Shunsuke Sasaki (University of Tokyo, Japan)

Tasuku Nishihara (University of Tokyo, Japan)

Daisuke Ando (University of Tokyo, Japan)

Masahiro Fujita (University of Tokyo, Japan)

Abstract: System Dependence Graph (SDG) is a graph representation which shows dependencies among statements / expressions in a design. In this paper, we propose a new HW/SW co-design methodology based on SDG. In our method, any combination of C / C++ / SpecC descriptions is acceptable as input designs so that design functions can be specified flexibly. First, the input descriptions are analyzed and verified with static but partially dynamic program checking methods by traversing SDG. With those methods, large descriptions can be processed. Next, those designs are divided into HW and SW parts. In this step, SDGs are fully utilized to insert parallelism into the designs, and it enables flexible HW/SW partitioning. The HW parts are further optimized and then converted into RTL descriptions by existing behavioral synthesis tools. Finally, the generated RTL descriptions together with the SW parts are compared to the original descriptions in order to make sure that they are logically equivalent. Also, designerspecified properties may be model checked with these final design descriptions. Such formal verifications can be realized by translating those descriptions into Finite State Machine (FSM) type representations and existing formal verifiers. We show two case studies with practical examples to demonstrate the usefulness of our approach.

Keywords: hardware software co-design, hardware software coverification, program slicing

Categories: B.7.2, D.2.2, D.2.4