模型检验在芯片工业界已经成为一种广泛认可的自动化的数字系统形式化验证工具，它可以明确地证明所设计的数字系统是否满足设计规范要求。尽管近年来模型检验获得了长足的发展，但是在处理容量方面还存在着进一步推广应用的巨大障碍——受困于状态爆炸问题，目前已有的模型检验工具还不能直接验证大部分的工业级数字系统设计。抽象精炼是一种通过迭代计算获得简化的抽象模型来帮助验证原始模型的算法，是目前解决模型检验处理容量问题最好的办法。BDD能够简洁有效地表示数字系统模型和时态逻辑公式，可以从化简抽象模型结构表示的角度来降低模型的复杂度，减小抽象模型BDD的规模是另外一种减轻模型检验状态爆炸问题的解决手段。本文针对模型检验所面临的状态爆炸问题提出了一种新的精细抽象方法以及基于此方法的二阶抽象精炼算法，用来获得最优或者近似最优的抽象模型，提高模型检验算法的处理容量和效率。此外，本文还提出了一种新的基于遗传禁忌混合策略的BDD优化算法，用来有效地降低抽象模型的BDD规模。　　 精细抽象方法是通过采用比其它抽象方法更小的抽象粒度，在抽象过程中仅仅将那些特性验证必需的电路元素——状态变量和中间组合变量添加到抽象模型中去，而不是将状态变量连同它所有的扇入组合逻辑一同添加到抽象模型中去。这种抽象方法在验证具有复杂组合逻辑的系统具有优势。基于精细抽象方法，本文提出的二阶抽象精炼算法可以利用K.可控性计算和K-协作性计算分别搜索用于模型精炼的状态和状态转移关系，迭代地依次分别对状态变量和中间组合变量进行抽象精炼。同其它已有的抽象精炼算法相比，这种算法可以提供给出更简洁的抽象模型用于特性模型检验，而消耗的运行时间却更少。在二阶抽象精炼算法中采用了最小固定点MBM机制来约束不可见变量的随意赋值，用来减少迭代过程中出现的伪反例的数量，以便提高计算效率。算法实验分析显示基于精细抽象方法的二阶抽象精炼算法同其它已有的抽象精炼算法相比能够获得较简的抽象模型，提高了模型检验工具处理大规模电路系统的能力。　　 基于遗传禁忌混合搜索策略的BDD优化算法将遗传算法的全局搜索能力同禁忌搜索的局部邻域搜索能力相结合来搜索最优的BDD状态排序，来获得最优的BDD结构。算法的架构分为两层，首先应用禁忌搜索给出所有最有希望的BDD变量候选排序，然后对这些候选排序进行遗传进化进而获得最优或者近似最优的BDD变量排序。算法中采用了相邻变量互换操作通过均匀分布随机地在解空间内生成邻域解，提高了邻域搜索的性能。算法实验分析显示这种混合了禁忌和遗传策略的BDD优化算法同其它已有的BDD优化算法相比能够取得规模更小的BDD表示，而且在运行时间上比单纯的基于遗传策略的BDD优化算法效率更高。针对此算法的未来工作将集中在如何提高算法的收敛速度上。