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