一种改进的有界模型检验子句规则  

Modified Clause Form for Bounded Model Checking

作　　者：尹文波[1] 荆明娥[1] 周电[1] 周晓方[1] 

机构地区：[1]复旦大学专用集成电路与系统国家重点实验室,上海201203

出　　处：《微电子学与计算机》2007年第11期103-106,109,共5页Microelectronics & Computer

基　　金：国家自然科学基金项目(90207002);国家"863"高技术研究发展计划(2003AA1Z1120;2004AA1Z1050)

摘　　要：为有界模型检验提出了改进的子句规则。在节点分类的基础上,首先对精简布尔电路表示进行逻辑化简,去掉功能冗余节点;然后识别、记录和处理多元运算的操作数,把多元运算作为单个节点直接生成子句;最后合并相邻节点,根据合并后的逻辑关系生成变量和子句。实验结果表明,改进的子句规则普遍减少了可满足性问题的变量、子句数目和运行时间。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.

关 键 词：可满足性问题 有界模型检验 子句规则 精简布尔电路 

分 类 号：TN47[电子电信—微电子学与固体电子学]