随着半导体工艺突飞猛进的发展,集成电路(integrated circuit, IC)设计的复杂度呈指数增长,对IC设计起决定性作用的电子设计自动化(electronic design automation, EDA)技术的发展相对落后,特别是验证已经成为整个IC设计流程的瓶颈。基于BDD的形式化验证方法是一种自动化的方法,但只适用于中、小规模的电路,对大规模的电路则会出现状态空间爆炸问题。近几年来,对可满足性(satisfiability, SAT)问题研究的进步使得EDA中的一些问题可以转化为SAT问题进行解决。但是,通用SAT求解器对求解特定领域的问题并不是最有效的。本文对基于SAT的数字电路的形式验证方法和FPGA工艺映射方法进行深入研究,利用电路结构和问题的特有信息,对SAT求解算法进行改进,取得了如下创新性成果：1)针对基于SAT的等价验证中,已有SAT求解算法zChaff*对电路可观无关性信息不能有效利用的问题,提出了一种改进的可满足性求解算法zChaff+。首先,根据逻辑门的输入与输出之间的关系,引入控制唯一性概念；其次,以带可观无关条件的CNF理论为基础,先通过在可观无关条件计算时不使用变量排序的方法,减少可观无关条件丢失,再通过不对只出现在可观无关条件中的变量赋值的方法,来保证电路的控制唯一性。理论分析和实验结果表明,改进的可满足性求解算法zChaff+在解决等价验证问题时,搜索空间大大减小,求解速度明显提高。2)针对基于SAT的无界模型检验中的前像计算问题,提出改进的所有解可满足性求解算法All-SAT+。首先,选用zChaff+作为标准求解器,并采用出现在无关条件中次数多的变量优先赋值的变量决策策略对其进行改进,生成尽量大的解立方体或者小的冲突子句,降低阻塞子句或冲突学习存储空间需求,并减少算法所需的总枚举步数；其次,采用只对状态变量进行lifting检查的改进算法,对每个枚举步求得的解立方体进一步扩展,使每个枚举步获得的解立方体捕捉到更多的解；再次,用ZBDD进行解合并压缩和存储；最后,利用无关状态学习约束以避免对不必要状态空间的搜索,并采用增量式技术通过学习子句共享提高算法效率。实验结果表明,改进算法All-SAT+有效地降低了解的个数和前像计算的时间,比文献中的lifting算法、Lipi算法在求解速度上都有显著的提高。3)针对由随机搜索算法和DPLL算法组成的混合SAT算法在求解电路相关问题时存在的过度满足问题,提出了改进的混合SAT算法HBISAT+。利用电路可观性对混合算法进行改进,局部算法采用改进算法WalkSAT+, DPLL算法则采用文献中的算法zChaff*;采用改进的启发式策略选择填充子句,协调两种算法,减少算法的迭代次数,提高整个算法的效率。实验结果说明,混合算法比只使用DPLL算法在求解速度上有很大提高,而改进算法HBISAT+的速度比原算法平均提高27%,证明利用电路可观性改进的混合求解算法,可以更有效的求解难解电路的等价验证问题。4)针对基于SAT的FPGA工艺映射算法中输入置换带来的计算量大的问题,提出改进的工艺映射算法。利用PLB结构和布尔函数中的对称信息,将输入置换问题转化为分配问题,直接生成必要的置换,只针对必要的置换进行映射可满足性检查。实验结果表明,改进算法比文献算法SAT-BM-I的求解速度平均提高了32%,说明改进算法大大减少了问题可满足性求解的规模,提高了布尔函数到PLB结构映射的效率。