High Level Formal Verification for Polynomial Datapath

摘要：

Taylor Expansion Diagram (TED) is a compact, canonical, world level graph-based representation, and it can effectively express multi-variate polynomial. In this paper, variable replacement algorithm and variable mergence algorithm for TED are presented. Based on variable replacement algorithm, variable ordering algorithm and variable merging algorithm, an algorithm of backward-construction TED is proposed, which is used to verify the equivalence between the behaviors specification and register transfer level (RTL) implementation of polynomial datapath. Experimental results show that the proposed method is effective.

作者: Donghai LI Haitao YU Guangsheng MA Guangshun LI

作者单位: Harbin Engineering University, China

会议类型: 国际会议

会议名称: 2nd IEEE Conference on Industrial Electronics and Applications(ICIEA 2007)(第二届IEEE工业电子与应用国际会议)

会议地点: 哈尔滨

会议语种:英文

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