从1965年4月摩尔在《电子学》杂志上的一篇文章中提出摩尔定律的半个多世纪以来,半导体发展迅速。集成电路已经应用到各个领域,无处不在,手机、电脑等数字产品深入每个人的生活,成为人们生活不可或缺的产品。因此集成电路的安全性越来越受到重视。随着集成电路技术的不断发展,为了适应市场,降低电路的设计成本和研发周期,SoC开发已经成为集成电路的设计主流。IP库是SoC设计的重要组成部分,在使用第三方IP库的时候安全性也成为了一个突出的问题。集成电路的设计和制造分离,工厂迁往劳动力成本低的地区,不少设计也外包给了其他设计公司,在集成电路的设计过程中会使用到各种不同公司提供的电子设计自动化软件,因此现在的半导体芯片在设计过程中变得比以前更容易受到恶意篡改。针对这个问题本文采用Coq来进行电路的安全性证明(等价安全性)。Coq是一种定理证明软件,适合于定理的正确性验证。本文先用Coq构建随机数发生器后处理算法的RTL代码的模型,然后将电路的RTL代码用这个模型转换成Coq语言。为了验证RTL代码是否包含硬件木马或者被人为的恶意篡改,采用Coq来验证RTL代码是否与设计时一致,以此来确定芯片的安全性。随着集成电路的发展,现在密码领域的很多算法都在SoC系统中实现。Coq不仅可以用于RTL代码级的等价安全性证明,同样也可以用于密码SoC架构的等价安全性证明；结合随机预言模型,本文为另一种电路的安全性证明(计算安全性)做了理论阐述,为下一步的工作打下了一个理论基础。