采用二元CSP引擎求解RTL数据通路的可满足性

摘要：

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

关键词：寄存器传输级、数据通路、可满足性、约束满足问题、模型检验

所属期刊栏目：21

分类号：TP391.7(计算技术、计算机技术)

资助基金：国家自然科学基金60673034;北京交通大学科技基金2007XM011, 2008RC002

在线出版日期：2009-05-22（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：442-447