中文摘要：

针对寄存器传输级（RTL）验证和测试过程中非常重要的数据通路可满足性求解问题,提出一种基于二元约束满足问题（CSP）的求解方法,包括数据通路提取、二元CSP建模和搜索求解3个步骤.数据通路提取通过对接口布尔变量和某些字变量赋值,为各个数据通路器件建立环境;二元CSP建模则根据该环境和各个数据通路器件的功能,将数据通路的可满足性问题转化为二元CSP描述;该二元CSP问题的描述被送入到二元CSP引擎,并采用冲突引导的回跳搜索策略进行求解,获得有解的例证或无解的判定.实验结果表明,即使在没有采取很多优化策略的条件下,该方法仍有较好的性能,并优于基于线性规划（LP）的求解方法.

英文摘要：

We propose a binary constraint satisfaction problem （CSP） based approach to the satisfiability problem of register-transfer level （RTL） datapaths, which is a critical issue in RTL verification and testing. The approach consists of three steps： datapath extraction, binary CSP modeling, and solution searching. In datapath extraction, we build the environments for all datapath units by making assignments to the Boolean interface variables and some word variables. Binary CSP modeling then translates the RTL datapath satisfiability problem to a binary CSP description, which in turn will be sent to a binary CSP engine and solved by conflict-directed backjumping search strategy. The answer will be either a witness of satisfiable instance or a unsatisfiable decision. Experimental results show that even without many optimization strategies exerted, the binary CSP based method still works fairly well, with better performance than LP-based method.