EHSAT Modeling from Algorithm Description for RTL Model Checking
This paper presents a new method to translate Verilog HDL into RTL Model combining algorithm description for high level verification. The model could be used in the enhanced version of a state-of-the-art finite- domain satisfiability (SAT) solver EHSAT to check the verified properties. The enhanced version of EHSAT provides an efficient algorithm to solve the SA T problem for higher level abstraction RTL designs using a hybrid branch-and-bound strategy with conflict-driven learning. This modeling program analyses the control flow of Verilog source codes and generates corresponding statements for the enhanced version EHSAT. This method could largely reduce the scale of model checking and simplify the devices used in EHSAT. Experimental results show that this method can reduce verification problem sizes considerably while comparing with lower level methods.
Xiaoqing Yang Jinian Bian Shujun Deng Yanni Zhao
Department of Computer Science and Technology, Tsinghua University, Beijing, China
国际会议
The 16th Asian Test Symposium(第十六届亚洲测试学术会议)
北京
英文
178-183
2007-10-08（万方平台首次上网日期，不代表论文的发表时间）