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

作者：郑伟伟; 吴为民; 边计年线性规划寄存器传输级可满足性性质检验形式验证

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

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社