一种基于混合SAT求解器的RTL验证方法

作者：葛海通; 翁延玲; 严晓浪

来源：浙江大学学报(工学版), 2010, (02): 289-293.

• 集成电路设计
• 逻辑综合
• 等价性验证
• 混合SAT求解器 integrate circuit design
• logic synthesis
• equivalence checking
• hybrid SAT engine

为了提高集成电路验证系统的性能,提出一种面向Verilog描述的寄存器传输级(RTL)电路验证方法.该方法将验证问题转化为RTL可满足性问题,并采用基于混合布尔可满足性问题(SAT)的求解器.与传统方法相比,其综合引擎取消了算术电路逻辑的实现,保留了电路特性及其优化信息.因为所需的待验证模型的抽象层次较高,综合系统所花的综合时间较少,尤其是验证引擎不需要处理较低级别的验证细节,由此大大提升了系统性能.不同规模的加法器实验结果表明,基于混合SAT引擎的RTL验证流程较传统流程有明显优势,对复杂电路的验证时间甚至可减少99%.

• 单位
  浙江大学