【作者】 陈闽川； 吴为民； 边计年；

【Author】 Chen Min Chuan, Wu Weimin, Bian Jinian

【机构】 清华大学计算机科学与技术系；

【摘要】 本文通过可满足性求解进行时序电路的性质检验。其基本思想是将时序电路展开若干个时序,并将性质转化为这些时序范围内的电路变量的可满足性问题。通过在iscas89标准测试电路上进行的一系列实验,证明了本文方法的有效性。更多还原

【Abstract】 In this paper, property checking is performed on sequential circuit via satisfiability solving. The main idea is to unfold the circuit by some time frames and translate the property checking into a satisfiability problem which includes variables acrossing these time frames. By a series of experi on iscas89 benchmark circuit, we demonstrate the effectiveness of the method更多还原