基于线性规划的RTL可满足性求解和性质检验

摘要：

采用线性规划作为基本工具开发一个RTL可满足性求解器,并将其应用于解决RTL性质检验问题.深入研究了使用线性规划约束对RTL电路元器件的建模方法,得到了一种对RTL电路建模的通用方法.通过将RTL性质转化为虚拟RTL电路,找到了一种验证RTL性质的方法.通过实验,并与采用zchaff布尔可满足性求解器的模型检验工具NuSMV进行比较,证明了基于RTL可满足性求解器的性质验证方法在内存和时间消耗上具有相当大的优势.

关键词：线性规划、寄存器传输级、可满足性、性质检验、形式验证

所属期刊栏目：18

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

资助基金：中国科学院资助项目60273011,60236020;国家科技攻关项目2003AA115110

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

页数：共7页

页码：538-544