期刊文献+

一种改进的有界模型检验子句规则 被引量:1

Modified Clause Form for Bounded Model Checking
下载PDF
导出
摘要 为有界模型检验提出了改进的子句规则。在节点分类的基础上,首先对精简布尔电路表示进行逻辑化简,去掉功能冗余节点;然后识别、记录和处理多元运算的操作数,把多元运算作为单个节点直接生成子句;最后合并相邻节点,根据合并后的逻辑关系生成变量和子句。实验结果表明,改进的子句规则普遍减少了可满足性问题的变量、子句数目和运行时间。 A new Clause Form for Bounded Model Checking is proposed. First, RBCs nodes are divided into two classes, Second, logic simplifying is performed to remove node with functional redundancy. Then muhi-operands operation is considered to be a single node to produce CNF clauses directly. In the end, the method of merging adjacent logical nodes is used to produce minimal CNF variables and clauses. The efficiency of the proposed approach is shown through its application on benchmark circuits.
出处 《微电子学与计算机》 CSCD 北大核心 2007年第11期103-106,109,共5页 Microelectronics & Computer
基金 国家自然科学基金项目(90207002) 国家"863"高技术研究发展计划(2003AA1Z1120 2004AA1Z1050)
关键词 可满足性问题 有界模型检验 子句规则 精简布尔电路 satisilability(SAT) bounded model checking clause form reduced Boolean circuits
  • 引文网络
  • 相关文献

参考文献4

  • 1Biere A,Cimatti A,Clarke E.M,et al.Symbolic model checking using SAT procedures instead of BDDs[C].Proceedings of the 36th ACM/IEEE conference on Design Automation Conference,New Orleans,Louisiana:ACM,1999:317-320
  • 2Abdullah P A,Bjesse P,Eén N.Symbolic reachability analysis based on SAT-solvers[C].Proceedings of 6th Internationai Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berli:TACAS,2000:411-425
  • 3David A,Plaisted,Steven Greenbaum.A structure-preserving clause form translation[J].Journal of Symbolic Computation,1986,2(3):293-304
  • 4Velev M N.Efficient translation of Boolean formulas to CNF in formal verification of microprocessors[C].Asia and South Pacific Design Automation Conference (ASPDAC'04),Yokohama,Japan:ACM,2004:310-315

同被引文献6

引证文献1

;
使用帮助 返回顶部