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

RTL Satisfiability Solving and Property Checking Based on Linear Programming

采用线性规划作为基本工具开发一个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.