Chinese Journal of Computers   Full Text
Title	A SAT-Based Arithmetic Circuit Bug-Hunting Method
Authors	CHEN Yun-Ji1) ZHANG Jian2) SHEN Hai-Hua1) HU Wei-Wu1)
Address	1)(Key Laboratory of Computer Architecture, Institute of Computing Technology, Chinese Academy of Sciences, Beijing 100080) 2)(State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100080)
Year	2007
Issue	No.12(2082—2089)
Abstract &   Background	Abstract E-CNF is hybrid of Boolean formula and mathematic formula. SAT-based arithmetic circuit bug-hunting method translates the verification problem into E-CNF, and solves E-CNF through E-SAT solver. E-SAT solver is an extension of complete SAT solver, with tag clause technique. Experiments show that SAT-based arithmetic bug-hunting method is powerful in finding bugs in arithmetic circuits. keywords Formal verification； SAT； E-CNF； Tag clause background This Research is supported by the National Basic Research Program of China (973 Program), under grant No.2005CB321600, by the National Natural Foundation of China for Distinguished Young Scholars, under grant No.60325205, by the Basic Research Foundation of the Institute of Computing Technology, Chinese Academy of Sciences, under grant No.20056020, by the National High-Tech Research and Development Plan of China, under grant Nos.2002AA110010, 2005AA110010 and 2005AA119020, and by the Knowledge Innovation Program of the Institute of Computing Technology, Chinese Academy of Sciences, under grant No.20056240. The authors mainly focus on design and verification of microprocessor Godson2. Conventional simulation method cannot cover the total state space of many module of modern microprocessor, so they dedicated on combination of formal verification and conventional verification methods. Till now, they have fully verified all function units of a modern microprocessor.