每日一题1013

icboy

形式验证
转自维基百科
形式验证
维基百科，自由的百科全书

在计算机硬件和软件系统中，形式验证的含义是根据某个或某些形式规范或属性，使用数学的方法证明其正确性或非正确性。
[编辑]
解释

软件测试无法证明系统不存在缺陷，也不能证明它符合一定的属性。只有形式化验证过程可以证明一个系统不存在某个缺陷或符合某个或某些属性。系统无法被证明或测试为无缺陷，这是因为不可能形式的规定什么是“没有缺陷”。所有可以做的，就是证明一个系统没有任何可以想到的缺陷，并且满足所有的使系统符合功能要求的和有用的属性。

在IC设计中，形式验证是一种IC设计的验证方法，它的主要思想是通过使用形式证明的方式来验证一个设计的功能是否正确。形式验证可以分为三大类：等价性检查（Equivalence Checking）、形式模型检查（Formal Model Checking）（也被称作特性检查）和定理证明(Theory Prover) 。


等价性检查的验证用于验证RTL设计与门级网表、门级网表与门级网表是否一致。在进行扫描链重排、时钟树综合等过程中，都可以用等价性检查保证网表的一致性。等价性检查已经融入IC标准设计流程中。等价性检查在检查ECO时非常有用。例如，设计者在修改门级网表时，由于手误，错将一个或门写成或非门，等价性检查工具通过比较RTL设计与门级网表，可以很容易地发现这种错误。

模型检查用时态逻辑来描述规范，通过有效的搜索方法来检查给定的系统是否满足规范。模型检查是目前研究的热点，但其验证的电路规模受限制这一问题还没有得到很好的解决。

定理证明把系统与规范都表示成数学逻辑公式，从公理出发寻求描述。定理证明验证的电路模型不受限制，但需要使用者的人工干预和较多的背景知识。

icboy

在百度找的

　　可测性设计(Design for Test)DFT
　　随着电子电路集成度的提高，电路愈加复杂，要完成一个电路的测试所需要的人力和时间也变得非常巨大。为了节省测试时间，除了采用先进的测试方法外，另外一个方法就是提高设计本身的可测试性。其中，可测试性包括两个方面：一个是可控制性，即为了能够检测出目的故障（fault）或缺陷（defect），可否方便的施加测试向量；另外一个是可观测性，指的是对电路系统的测试结果是否容易被观测到。
    在集成电路（Integrated Circuit，简称IC）进入超大规模集成电路时代，可测试性设计（Design for Test,简称DFT）是电路和芯片设计的重要环节，它通过在芯片原始设计中插入各种用于提高芯片可测试性（包括可控制性和可观测性）的硬件逻辑，从而使芯片变得容易测试，大幅度节省芯片测试的成本。
　　编辑本段
　　三种常见的可测性技术
　　扫描路径设计(Scan Design)
　　扫描路径法是一种针对时序电路芯片的DFT方案.其基本原理是时序电路可以模型化为一个组合电路网络和带触发器（Flip-Flop，简称FF）的时序电路网络的反馈。
　　内建自测试
　　内建自测试（BIST）设计技术通过在芯片的设计中加入一些额外的自测试电路，测试时只需要从外部施加必要的控制信号，通过运行内建的自测试硬件和软件，检查被测电路的缺陷或故障。和扫描设计不同的是，内建自测试的测试向量一般是内部生成的，而不是外部输入的。内建自测试可以简化测试步骤，而且无需昂贵的测试仪器和设备（如ATE设备），但它增加了芯片设计的复杂性。
　　边界扫描测试
　　为了对电路板级的逻辑和连接进行测试，工业界和学术界提出了一种边界扫描的设计，边界扫描主要是指对芯片管脚与核心逻辑之间的连接进行扫描。

icboy

　　SDRAM:Synchronous Dynamic Random Access Memory，同步动态随机存储器，同步是指 Memory工作需要同步时钟，内部的命令的发送与数据的传输都以它为基准；动态是指存储阵列需要不断的刷新来保证数据不丢失；随机是指数据不是线性依次存储，而是自由指定地址进行数据读写。
　　SDRAM从发展到现在已经经历了四代，分别是：第一代SDR SDRAM，第二代DDR SDRAM，第三代DDR2 SDRAM，第四代DDR3 SDRAM.(显卡上的DDR已经发展到DDR5)
　　　　第一代SDRAM采用单端（Single-Ended）时钟信号,第二代、第三代与第四代由于工作频率比较快，所以采用可降低干扰的差分时钟信号作为同步时钟。
　　　　SDR SDRAM的时钟频率就是数据存储的频率，第一代内存用时钟频率命名，如pc100，pc133则表明时钟信号为100或133MHz，数据读写速率也为100或133MHz。
　　　　之后的第二，三，四代DDR（Double Data Rate）内存则采用数据读写速率作为命名标准，并且在前面加上表示其DDR代数的符号，PC-即DDR，PC2=DDR2，PC3=DDR3。如PC2700是DDR333，其工作频率是333/2=166MHz，2700表示带宽为2.7G。
　　　　DDR的读写频率从DDR200到DDR400，DDR2从DDR2-400到DDR2-800，DDR3从DDR3-800到DDR3-1600。