Equivalence Checking of High-Level Designs Based on Symbolic Simulation

摘要：

In this paper, we present a formal equivalence checking method for source-to-source refinements in C-based high-level hardware design descriptions. The method is based on word-level symbolic simulation, where variables and operators in designs are treated as uninterpreted symbols. In addition, we introduce a more efficient method utilizing the difference between two designs under verification. It can verify the equivalence faster when the similarity between the designs is large. We also show case studies of equivalence checking that were carried out with our verification framework FLEC.

作者: Takeshi Matsumoto Tasuku Nishihara Yoshihisa Kojima Masahiro Fujita

作者单位: VLSI Design and Education Center, The University of Tokyo Department of Electronics Engineering, The University of Tokyo

会议类型: 国际会议

会议名称: 2009国际通信电路与系统学术会议(ICCCAS 2009)(2009 International Conference on Communications，Circuits and Systems)

会议地点: 成都

会议语种:英文

页码: 1129-1133

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