摘要
采用线性规划作为基本工具开发一个RTL可满足性求解器,并将其应用于解决RTL性质检验问题·深入研究了使用线性规划约束对RTL电路元器件的建模方法,得到了一种对RTL电路建模的通用方法·通过将RTL性质转化为虚拟RTL电路,找到了一种验证RTL性质的方法·通过实验,并与采用zchaff布尔可满足性求解器的模型检验工具NuSMV进行比较,证明了基于RTL可满足性求解器的性质验证方法在内存和时间消耗上具有相当大的优势·
A RTL SAT solver is built which uses linear programming (LP) as the basic tool, and is applied to the property checking of RTL circuits. After researching further the method to model RTL elements in LP constrain to virtual RTL circuits, ts, th a general method to model RTL circuits is got. By transforming RTL properties e RTL property verification can be realized. By conducting experiments and comparing the results with that produced by NuSMV, a model checking tool which uses zchaff Boolean solver, it demonstrate superiority in memory and time consumption of RTL solver based property checking approach.
出处
《计算机辅助设计与图形学学报》
EI
CSCD
北大核心
2006年第4期538-544,共7页
Journal of Computer-Aided Design & Computer Graphics
基金
国家自然科学基金(60273011
60236020)
国家"八六三"高技术研究发展计划(2003AA115110)
关键词
线性规划
寄存器传输级
可满足性
性质检验
形式验证
linear programming
register transfer level
satisfiability
property checking
formal verification