基于逻辑锥和SAT的带黑盒电路等价性验证方法

发布时间：2021-12-23 09:24

　　随着信息产业的发展，超大规模集成电路和数字系统几乎占据了我们生活的所有领域。而且，由于芯片设计复杂性与日俱增，新产品的功能验证难度也逐渐加大。由于这些原因，在设计阶段早期发现错误显得十分必要。因此，开发形式化验证技术来处理那些或许会引起功能不正确的设计阶段是非常重要的。等价性验证是形式化验证方法之一，它主要解决验证两个电路是否功能等价的问题。现在电路设计经常包含某些功能未知的模块，这些模块被称作黑盒。为了在早期阶段发现设计错误，我们对带黑盒的实现电路进行等价性验证。本文主要研究了集成电路的等价性验证理论及其在带黑盒电路上的应用，进而提出一种基于逻辑锥分割和SAT的带黑盒电路的等价性验证方法。主要包括以下三方面的内容：1．等价性验证：等价性验证技术证明两个被给定电路具有相同的功能。例如，一个优化的设计与其早期版本是功能等价的。在验证过程中，验证方法被分为两类：（1）符号方法，（2）增量方法。符号方法是指依赖于使用BDD符号技术的那些方法；增量方法是指在验证中，开发两个电路的结构相似性。2．带黑盒的等价性验证：在假设规范电路和带黑盒的实现电路具有组合性质的基础上，提出带黑盒的等价性验证方法... 

【文章来源】：兰州大学甘肃省 211工程院校 985工程院校 教育部直属院校

【文章页数】：65 页

【学位级别】：硕士

【部分图文】：

EDA验证需求

验证工作占用的时间最多，特别是进入深亚微米领域，几乎80%的时间都花费在验证方面(如图2.1所示)。造成这种局面的原因有二:一方面，设计的规模正如摩尔定律所指出的呈指数增长(如图2.2所示)。如果使用设计中的状态数目来衡量功能复杂度的话，则设计的功能复杂度随着设计规模又呈指数增长。如此惊人的速度，对验证技术的处理能力提出了巨大挑战。另一方面，历史上对设计流程中的其它环节，如逻辑综合、布局布线和测试产生等问题关注颇多，而对验证重视不够，造成验证成为目前集成电路设计的瓶颈，如果没有重大突破，验证将成为未来集成电路设计工业【19}流程中的重大障碍。传统的模拟仿真等验证技术，己经越来越不能适应日益复杂的设计要求。

功能属性有效或无效，因此能够对所有可能的运行状态进行完全彻底的探查。一般来说，功能验证方法主要有模拟(simulation)、硬件仿真(HardwareEmulation)、形式化方法 (FormalMethod)(如图2.4所示)。其中形式化验证方法大致可以分为等价性检验 (EqulvaleneeCbeeking){3，20}、定理证明(TheoremProving)和模型检测 (ModelCheeking)。等价性检验是目前在工业实践中广泛使用的一种形式化验证方法，而且已经被应用于验证大型复杂系统的设计。等价性检验的基本思想是对照设计的形式化规范来验证它的实现的功能正确性。等价性检验使验证工程师节省了大量的时间，因为它使用形式化方法而不需要产生测试向量，此外，这种方法对于检测设计错误也很有效。等价性检验可以用来验证两个相同或者不同抽象级别设计的等价性，如


本文编号：3548224