Verilog Transformation for an RTL SAT Solver in Formal Verification

摘要：

This paper presents a new method automatically translating the Verilog model to an RTL circuit model which can be used in a state-of-the-art finite-domain satisfiability solver EHSAT to check the verified properties. Different methods are used in the transformations of different data types and expressions of Verilog model. Effective backfilling technology is applied in the processes of if…else and case blocks. Experiment al results show that this method can make the transformation effective.

作者: Xiaoqing Yang Jinian Bian Shujun Deng Yanni Zhao

作者单位: Department of Computer Science and Technology Tsinghua University Beijing, China

会议类型: 国际会议

会议名称: 2007年通信、电路与系统国际会议(2007 International Conference on Communications,Circuits and Systems Proceedings)

会议地点: 日本福冈

会议语种:英文

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