论文部分内容阅读
传统模拟验证方法和形武化验证方法在面临复杂大规模设计时，性能和处理能力的缺陷日益突出。为了融合二者的优点，避免各自不足，本文改进并实现了一种半形式化的验证方法。首先，提出了控制状态变量和一般控制变量的概念，以及从代码中识别和提取这两类变量的方法。利用此方法能够从目标设计中较为精细的抽象出部分核心电路逻辑，获得抽象距离信息。然后通过一种抽象信息引导的激励生成算法，对获得的抽象信息的有效性进行了检验。实验结果表明，这种方法仅需花费较小的计算代价，获得了较为精确的抽象信息，能够高效的引导验证覆盖到难达的状态。并且与设计规模相关性较小，具有较为广泛的适用性。