一种基于SAT的运算电路查错方法

作者：陈云霁; **; 沈海华; 胡伟武

来源：计算机学报, 2007, (12): 2082-2089.

• 形式验证
• 模型检验
• SAT
• E-CNF
• 标志子句 Formal verification
• SAT
• E-CNF
• Tag clause

基于SAT的运算电路查错方法将被验证系统中系统规范成立与否的问题转换为布尔公式和数学公式的混合形式E-CNF,通过采用了标志子句技术的E-SAT求解器进行求解.实验表明该方法自动化程度高,能处理大规模的运算电路,有较强的查找错误能力.

• 单位
  计算机科学国家重点实验室; 中国科学院计算技术研究所; 中国科学院软件研究所