验证包含黑盒的电路设计的有效方法

作者：李光辉; 邵明; 李晓维

来源：计算机学报, 2004, (06): 796-802.

• 布尔可满足性
• 功能验证
• 黑盒
• 布尔比较
• 逻辑模拟 Boolean satisfiability
• function verification
• black box
• Boolean comparison
• logic simulation

在超大规模集成电路设计中 ,为了进行早期的设计错误检测与调试或层次化验证 ,常常需要使用含黑盒的设计验证方法 .该文提出了一种结合逻辑模拟和布尔可满足性的黑盒验证方法 ,用于验证设计中黑盒外部的功能正确性 .该方法使用量化的合取范式 (CNF)来表示电路中出现的未知约束 ,并且不需要修改电路结构 ,有效地节省了计算资源 .此外 ,通过使用随机并行模拟增强了可满足性算法的错误检测能力 .通过对ISCAS’85电路的实验表明了该方法不仅比以往同类算法速度快 ,而且具有较好的错误检测能力 .

• 单位
  中国科学院计算技术研究所; 浙江林学院; 中国科学院研究生院