计算机架构的安全性主要涉及软件安全和硬件安全两个方面。面向软件的漏洞分析一直是安全分析领域的主要内容,产生了许多有效的研究方法,使得软件部分的安全性不断提高。而硬件漏洞一方面由于其隐蔽性、抽象性以及复杂性等诸多因素的制约,多年来一直没有引起足够的重视,另一方面进展较为缓慢,没有形成系统性的研究方法,取得的研究成果也较为有限。因此,硬件漏洞分析技术已经成为制约计算机安全性提升的主要因素。针对这种情况,本文在分析比较传统硬件漏洞分析方法优缺点的基础上,提出了基于软硬件协同形式验证的计算机硬件漏洞分析方法,同时详细阐述了该方法的研究思想和工作流程,提高了计算机硬件漏洞分析方法的通用性和有效性。之后描述了软硬件协同形式验证库的架构和构建方法,针对建模过程中常见的状态空间爆炸问题,在改进现有方法的基础上提出了基于变量约束的谓词抽象方法,减少了系统模型中的状态数量,提高了系统模型的建模和检测速度。最后针对已知漏洞进行了建模分析和验证,证明了该方法的有效性。同时以计算机启动过程中的未知漏洞分析为例,使用该方法对其进行了分析,发现了模型中的未知漏洞并通过实验进行了证明,验证了使用该方法分析未知漏洞的有效性。