模块级验证是当代微处理器功能验证的重要环节.模块级验证针对各类不同模块的特点,选取合适的验证策略,或者将绝大部分bug在模块级发现出来,或者证明模块的正确性.模块级验证是全系统级验证的前提,它减轻全系统级验证的负担,使之专注于互联、交互响应、接口和comer case等.但当模块复杂度达到一定规模后,传统仿真验证方法无法覆盖整个状态空间,因而无法确保模块的正确性.因此形式化和半形式化的模块级验证方法的研究,对于微处理器设计验证有着重要的意义. 本文结合龙芯2号微处理器的模块级验证工作,系统研究了微处理器中两类主要模块的验证方法:针对控制模块,提出了基于SAT的面向覆盖率的验证方法;针对运算模块,对基于SAT的运算电路查错方法进行了优化,使得它能真正实用于工业级设计.其中部分技术在龙芯2号验证中取得了实际效果. 以下是本文的主要贡献与创新点:1.提出了面向覆盖率的SAT引擎.覆盖率是仿真验证的评估依据,也是进一步仿真验证的指导.面向覆盖率的策略令仿真验证有着很好的健壮性和可扩展性.但是仿真验证效率比较低.模型检验方法单位时间能处理的状态要比仿真多得多,验证效率远高于仿真验证.但它受限于指数级的复杂度,因此可处理的电路规模仍然有限.面向覆盖率的SAT引擎通过回溯的方法来遍历整个搜索空间来搜索bug,同时给出覆盖率信息.它结合了仿真验证和形式验证的优势,既有仿真验证的健壮性和可扩展性,又有形式验证的高效率.它适合控制模块的验证,即使在处理电路规模太大无法完全证明时,也能以形式化方法的验证效率来完成仿真验证的任务.2.提出了SAT求解过程中的覆盖率制导方法.在基于SAT的硬件验证中, SAT求解器的搜索过程陷入局部性子树会导致某部分需验证的电路无法被覆盖到,在覆盖率上则体现为覆盖率增长速度变缓.SAT求解过程中的覆盖率制导方法利用覆盖率变化速度来估计Pareto-Lévy分布的α值,以此来判断当前搜索是否陷入局部性子树,并在在口值较低时重启搜索.通过这种方法,求解器能较准确地估计是否已经陷入局部性子树,避免无意义的深度遍历,因此能更快地提高覆盖率.3.提出了E-CNF求解的标志子句技术.在基于SAT的运算电路查错方法中,只有在数学子句所包含布尔变量都已被赋值的情况下才能判断它的真假.实际上部分布尔变量被赋值就可能已经使得对应的数学子句有确定的值,但求解器还必需做无谓的深度遍历.标志子句技术使得E-CNF的求解器E-SAT能提前判断数学子句的值,避免无谓的深度遍历,令基于SAT的运算电路查错技术能真正实用于工业级设计.