A Symbolic Methodology for Formal Verification of High-level Data-Flow Synthesis

摘要：

This paper presents a new symbolic methodology for the formal verification of high-level data-flow synthesis process. In the approach,high-level specification of a data-flow design is modeled with Kleene algebra with tests (KAT) as a relational expression. By analyzing this relational expression,assertions that establish properties of the high-level specification are obtained. Then,the problem of high-level data-flow synthesis verification is reduced to the task of checking whether the architectural implementation generated by the synthesis procedure satisfies these asserted properties. A Wus method based property checking approach is integrated into the verification framework to solve this problem. The experimental results on some benchmark and practical designs demonstrate the efficiency of the approach.

作者: Zhi Yang Chao Lv Guangsheng Ma Jingbo Shao

作者单位: College of Computer Science & Technology,Harbin Engineering University,Harbin 150001,P.R.China Harbin High Financial College,Harbin 150030,P.R.China

会议类型: 国际会议

会议名称: 9th International Conference on Solid-State and Integrated-Circuit Technology(第9届固态和集成电路国际会议)

会议地点: 北京

会议语种:英文

页码: 2353-2356

在线出版日期: 2008-10-20（万方平台首次上网日期，不代表论文的发表时间）