精华内容
下载资源
问答
  • 形式化方法一般可分为形式化规范说明Formal Specification,和形式化验证Formal Verification。 Formal Formal Specification 形式化规范说明 Formal Verification 形式化验证 Theorem Proving 定理检测/Deductive...

    【1】 概述

    硬件和软件系统在规模和功能上的增长增加了复杂性,也 增加了潜在错误的可能性,这些错误引起了金钱、时间上的损 失,甚至会危及人们的生命。形式方法是用于软件和硬件系统 的规范,开发和验证的特定类型的基于数学的技术,是改善和 确保系统质量的重要方法。形式化方法在软件和硬件领域中 的应用进展比较显著,引起了各个领域的注意[1]。形式化验证 方法是形式化方法的一个重要的研究内容,本文主要对形式化 验证方法进行探讨。

    形式化方法一般可分为形式化规范说明Formal Specification,和形式化验证Formal Verification。

    Formal

    • Formal Specification 形式化规范说明
    • Formal Verification 形式化验证
      • Theorem Proving 定理检测(证明)/Deductive Verification 演绎检测
      • Model Checking 模型检测
      • Automated Test Case Generation 自动测试用例生成

    在这里插入图片描述

    【2】基本概念

    【2.1】形式化规范说明

    硬件和软件系统在规模和功能上的增长增加了复杂性,也 增加了潜在错误的可能性,这些错误引起了金钱、时间上的损 失,甚至会危及人们的生命。形式方法是用于软件和硬件系统 的规范,开发和验证的特定类型的基于数学的技术,是改善和 确保系统质量的重要方法。形式化方法在软件和硬件领域中 的应用进展比较显著,引起了各个领域的注意[1]。形式化验证 方法是形式化方法的一个重要的研究内容,本文主要对形式化 验证方法进行探讨。

    【2.2】形式化验证

    【2.2.1】定理证明

    定理证明:先对系统及其性质进行抽取,表示成基于某种 逻辑的命题、谓词、定理,在验证者的引导下,不断地对公理、以 证明的定理施加推理规则,产生新的定理,直到推导出表达系 统性质的公式,从而证明设计的系统满足该性质。现在定理证 明器越来越多的应用在验证硬件和软件设计的安全临界性质 的验证[3]。 定理证明高度抽象,具有强大的逻辑表达能力,可以验证 几乎所有的系统行为特性,可以处理无限的状态空间。定理证 明器可以分为三种:自动定理证明器、交互式定理证明器及证 明检验器。现在大多数定理证明器是交互式的,需要人的引 导,对验证者的要求有良好的数学经验。 主要的定理证明工具有:STeP(Stanford)、TLV、AL2(UTAus⁃ tin/CLI)、Coq、HOL(Cambridge)、Isabelle(Cambridge)、Larch、Nu⁃ prl、PVS(SRI)等。

    【2.2.2】模型检测

    模型检测是一种通过对目标系统建立一个有限的模型,并在模型发生改变时,检测希望满足的性质,例如安全性和活性在该模型中是否成立、稳定的技术。

    目前有两种主要模型检测技术:

    • 一种是时态模型检测,这 种方法中规范说明用时态逻辑公式表示,系统用有限状态转换模型表示,用模型检测器检测模型是否满足规范说明公式。
    • 另外一种是等价性检测,这种方法中规范说明用一个自动机表示,系统用一个自动机表示,然后证明两个模型是否一致。

    自动化程度较高是模型检测的优点,并且当系统不满足给 定的性质时,可以给出反例,使设计人员方便找出设计错误。 模型检测应用于硬件和协议的验证,现在在对软件设计的验证 已成为研究的热点。状态空间爆炸问题是其主要的缺点。

    主要的模型检测工具有:

    • COSPAN/FORMALCHECK(Bell)、
    • MURPHY(Stanford)、SPIN(Bell)、
    • SMV(CMU)、
    • VIS(Berkeley)等。

    目前形式化验证方法成功应用于商业、航空业、通信业和 芯片制造业,INTEL,ARM和NIVIDA等大公司已经把形式化方法应用到芯片的制造和验证[5]。

    从本质上讲,模型检测技术就是穷尽对状态空间的搜索,并通过模型的有限性来保证该搜索过程一定会终止。最初的模型检测应用在硬件和协议验证领域,十分成功,后来在软件系统的验证上也得到了广泛应用。

    Reference:

    [形式化验证方法浅析] 陈波1,李夫明2 (1.山东理工大 学 计算机科学与技术学院,山东 淄博255000; 2.山东理工大学 数学与统计学院,山东 淄博255000)**

    后续待阅读资料

    线性时序逻辑 https://www.docin.com/p-506137477.html
    模型检测 https://wenku.baidu.com/view/800eade45a8102d277a22f3a.html?fr=search
    model checking overview and buchi automata and LTL https://www.docin.com/p-1003260979.html

    展开全文
  • 基于Spin的安全协议的形式化验证
  • 智能合约形式化验证

    千次阅读 2018-06-19 10:59:19
  • 摘要:IP验证传统上包括某种形式的受约束的随机验证方法,例如UVM,也可能包括对设计的一部分进行形式化验证。但是,在运行第一个随机测试之前,通常都有一个将所有验证基础架构汇总的提前期,并且覆盖率闭合也很...

     

    摘要:IP验证传统上包括某种形式的受约束的随机验证方法,例如UVM,也可能包括对设计的一部分进行形式化验证。但是,在运行第一个随机测试之前,通常都有一个将所有验证基础架构汇总的提前期,并且覆盖率闭合也很耗时。对设计的一部分进行形式化验证有助于减少UVM测试平台的覆盖空间,但仍需要完整的UVM测试平台基础结构,并且还需要用于形式化验证的其他资源。在本文中,我们将端到端(E2E)形式化方法作为仅使用形式化工具来验证IP的可行选择。我们使用交叉开关(XBar)和中断控制器(INTC)这两个IP来呈现关于我们方法论有效性的经验证据,并将其与使用标准UVM验证的其他IP进行对比。我们还介绍了在这两个模块上部署E2E形式化时遇到的一些挑战,并讨论了克服这些问题的策略。我们还为部署E2E形式化方法提供了一些建议,并得出结论,与基于UVM模拟的方法相比,我们的E2E形式化方法能够提供至少相同的验证质量,同时验证周期显着缩短

     

     

    引言

     

    在我们的E2E形式化验证方法中,使用基于IP规范的形式化属性来完整描述IP。使用IPXACT XML文件中自动生成的断言检查寄存器。标准接口使用形式化的特性证明套件而不是通过VIP进行检查。DVE编写新的断言时,将并行完善验证环境和IP,并调试断言的反例。通过与设计团队经常对IP规范进行审查,来检查这些断言的质量和完整性。一旦所有形式化属性均被设计人员批准,并且所有断言和证明工具包均已通过验证,则该IP被视为经过充分验证。

     

    我们之所以选择这种方法,主要是因为我们预测它可以用更少的精力达到与UVM相同或更高的验证质量。E2E形式化验证不承担编写UVM测试平台所带来的开销,例如编写自定义代理,序列库和记分板。还可以在交付RTL之前获得IP规范,从而使DVE可以在开发验证环境方面抢先一步。我们在E2E形式化验证方面的经验表明,与基于模拟的测试平台相比,它还有其他优势,这些将在本文档的后面部分进行深入讨论。

     

    选择用于形式验证的IP时,仔细评估与该方法的兼容性至关重要。通常,IP必须较小且相对简单。我们选择使用我们的方法来验证中断控制器(INTC)和交叉开关(XBar)。

     

    中断控制器

    图1 中断控制器结构图

     

    中断控制器负责将设备和软件中断路由到动态位置。它接受不同级别的中断输入,并将它们路由到中断标志寄存器和路由配置寄存器中指定的位,然后在该位置设置中断标志寄存器的位。每个中断标志寄存器都映射到唯一的输出中断,只要将中断标志寄存器设置为非零值,就会产生一个中断。输入和输出中断都可以在配置寄存器中单独屏蔽。可以随时操纵配置寄存器和中断标志寄存器,从而允许软件控制的中断,动态路由和中断屏蔽。

     

    交叉开关

    标题图2 交叉开关结构图

     

    交叉开关是一个仲裁程序,它控制三个不同请求者对共享内存空间的访问。它支持轮询、固定优先级和LFSR优先级方案。它允许单个请求者锁定对bank的独占访问。每个bank模块都负责仲裁逻辑,并且包含了大多数交叉开关的复杂性。

     

     

    挑战

     

    通常,由于仅使用形式化的验证难以被接受用以取代受约束的随机验证流程。因此,从技术和报告的角度来看,我们在部署E2E形式化方法时都遇到了许多挑战。其中一些描述如下:

    1. 质量:对于E2E形式化方法,我们必须确保我们通过编写的所有断言涵盖了设计的所有功能/方面。那时,EDA工具没有很好的覆盖率报告(后文详细讨论),与传统的模拟测试平台相比,我们不得不花额外的时间来检查断言。但是,这并不是工作的重要部分。

    2. 验证IP:我们计划为所有标准接口(例如APB,OCP等)和配置寄存器(configuration registes,即CSR)编写断言。开发这些断言需要投入大量的精力。幸运的是,大多数工具供应商都有一些我们可以利用的“证明工具包”(Proof-kits)。这些工具包类似于模拟测试平台中的VIP。但是,并非所有工具供应商都具有相同功能的形式证明工具。在某些情况下,还需要其它胶合逻辑来整合成证明套件和/或其他配置选项。

    3. 收敛:对于INTC,由于微体系结构的对称性,我们选择将断言的生成模板化。这导致为E2E形式化验证生成了420K大小的断言,并且我们很快遇到了几个工具上的问题。这些问题不限于任何特定的EDA供应商。存在两个主要的基本问题:

      1. 编译时间:甚至在开始证明之前,都需要花费难以接受的大量时间来编译断言。将420K的断言拆分为多个较小的10K-40K文件块后仍需要近几个小时的编译时间。我们必须与客服紧密合作来调试问题,最终通过工具的R&D更新/补丁将编译时间减少到合理的数量。

      2. 证明时间:解决了编译时间问题后,我们很快遇到了非线性运行时增长与断言数量之间的关系。考虑到有限的许可证和计算资源,到目前为止,我们仅能并行处理INTC证明。为了进一步解决验证时间,我们必须部署后续讨论的策略。

    4. 报告:在开发时,可用的形式化工具并未提供与模拟覆盖率指标(例如代码覆盖率)进行轻易比较的覆盖率指标。这需要额外的精力来开发脚本,把我们拥有的指标重新格式化,使其成为更传统的格式,使工程师、程序和高管者更容易理解。由于没有一种格式可以与仿真报告进行对等的比较,我们在验证质量和进度方面不断的面临挑战,并且不得不经常深入研究E2E形式验证结果的细节。在许多情况下,我们必须与工具供应商紧密合作,以设计出对形式化验证报告进行后期处理的方法。

     

     

    策略

     

    分而治之

    某些IP(例如中断控制器)特别容易受到有关断言个数导致的非线性运行时间增长的影响。通过限制每次执行的断言数量,有效地将断言的总集合分成较小的组,从而减轻了这种过多的运行时间。即使在按顺序执行这些划分后的断言主体时,总的运行时仍显示出接近线性模式的增长模式,这与玩增证明中看到的非线性增长相反。对于中断控制器,此差异使运行时间减少了25%,并且断言的数量越多,差距就越大。

    标题图3 划分断言和完整断言的运行时间

     

    分层策略

    IP通常会将同一子模块用相同的参数实例化多次。在这种情况下,高效的方法是将子模块验证一次,并在顶层验证多个实例的集成。这减少了验证IP所需的断言数量,大大减少了运行时间,但保持了相同水平的验证质量。

    例如,交叉开关中的每个存储库都包含其自己的特定子模块的实例,该子模块负责优先级逻辑和选择标准。检查此功能对于交叉开关的验证至关重要,但是没有必要在相同实例中都对优先级逻辑部分执行相同的检查。这些子模块集的集成测试是在顶层进行连接并检查的。

     

    通过允许DVE在子模块级别上开发,诊断和调试测试平台,该方法降低了断言复杂度并加快了调试时间。与UVM相比,它还具有优势,因为与基于仿真的方法相比,使用E2E形式化方法实现子模块级验证所需的工作量更少。在UVM中,如果不为子模块开发单独的测试平台,则很难进行子模块级别的验证。然而,在E2E形式化方法中,只需为子模块编写断言即可执行类似的检查,这些断言可以在测试平台的顶层轻松导入。

     

    抽象化

    抽象化是识别IP或测试平台中的模式,并通过更高级别的抽象以更简单的术语描述模式的过程。从细粒度到较宽粒度的这种转变可以减少所需的断言数量,从而带来性能优势。

    事实证明,抽象化对于减少中断控制器中的证明时间非常有用。该IP接受由上升沿触发的中断线程。验证这种边缘检测功能的简单方法是为每条中断线程写一个断言。但是,由于$ rose()这类的系统功能只能在单个比特位上运行,因此只能在比特位级别的粒度下才可以不应用抽象化。相反,在一个断言中将所有中断线程都视为一个比特位向量的情况下,在所有中断线程上测试相同的功能将更加简单。这是通过将边缘检测器逻辑引入到胶合逻辑中,然后在重写断言边缘检测检查时利用这些结构来实现的,从而使它们以字粒度级别进行测试。这种粒度上的变化使中断控制器的边沿中断检查的断言计数减少了32倍。

    此方法提供的优点是,它可以显着减少断言计数,而不必丢失任何功能验证。如果存在不需要验证的功能(例如馈入多路复用器的数据位的各种可能值),则可以减少更多。但是,与分层策略和黑匣子一样,必须格外小心,以确保不排除未经验证的功能。

     

    常规方法

    我们的方法中还利用了一些传统的形式化验证策略。尽管在E2E形式化验证中进行详尽测试非常重要,但经过仔细考虑,如果不更改IP的功能,则可以安全地排除或限制组件。例如,在仅测试总线连接性的情况下,无需测试总线的所有可能的数据或地址值。可以将这些信号约束为不随机化以减少运行时间。其他传统方法,例如利用并行性和执行工具特定的优化,也被用来减少运行时间。

     

     

    结果

     

    我们比较了基于传统仿真(UVM)的环境与E2E形式化验证之间的各种指标,以分析E2E形式化验证方法的质量和投资回报率(Return on Investment,ROI)。为了规范通过不同方法验证的各种IP的复杂性,我们将门数视为比较分析的一个很好的一阶近似值。然后,我们根据资源、时间表、测试台代码行(lines-of-code,LOC)和逃避这些IP测试台的错误来考虑验证每个门所需的工作,以评估每个测试台的相对效率和质量。最后,我们比较了模拟验证和E2E形式化验证测试平台之间的效率。

     

    下表突出展现了各种测试平台的一些关键指标。所有数据均来自最近已流片的项目。

    • 选择了多个IP,其中包括图像处理,信号处理和通用控制密集块;

    • 门数不包括任何内存,但代表IP中的组合+顺序逻辑总数;

    • 持续时间仅是工作日(即星期一至星期五);

    • DV(Design Verfication)代码行在测试平台中不包括空白或注释代码,但包括所有UVM组件,序列,断言,测试用例,覆盖结构等。其中不包括第三方VIP代码;

    • 逃脱Bug是在IP的RTL代码冻结后逃脱IP验证并在更高级别的测试台上捕获的RTL Bug的数量;

    • Bug密度是每一千行DV代码行发现的RTL Bug总数;

    • 假定许可权和计算资源可用,不作为比较的因素。

    • UVM DV资源是具有丰富的经验组合,范围从1-10年的从事受约束的随机验证到1-7年的UVM / OVM方法学。E2E形式化的DV资源具有SVA和大约1年的形式化验证经验。

     

    关于数据的其他注释如下:

    1. 每个LOC每个工作日验证的平均门数约为0.09,IP1 由于IP1是一个异常,因此不考虑入内。由于IP的微体系结构占用了大量寄存器文件。如果考虑IP1,则平均值为0.16;

    2. 对于INTC,总LOC-DV还包括使用模板生成声明所需的代码/脚本;

    3. IP9有较多的逃逸错误主要由于所有权的流失,在整个IP开发过程中,该模块归几位不同的设计师所有。

     

    我们选择了三个指标来比较UVM和形式化的E2E方法之间的质量和ROI:

    1. 每天每个LOC-DV验证的门数(即DV效率)

    2. 每个一千个LOC-DV的错误密度(即DV质量)

    3. 从IP测试平台逃逸的Bug

     

    基于上述标准,我们得出以下推论:

    1. 与模拟或UVM的测试平台相比,使用形式化的E2E可以达到相同甚至更高的效率

    2. 在错误密度方面,形式化的E2E在每个LOC-DV中可以比UVM测试平台发现更多的错误,这主要是由于我们只需要声明和形式化测试平台所需的最小胶合逻辑(如果有)。我们也不需要开发任何UVM / VIP组件。

    3. 就错误逃逸而言,E2E形式化测试平台可以达到与UVM测试平台相同的IP验证质量

    4. 即使我们花了额外的时间来审查E2E形式化方法中的断言,也可以通过以下方式来节省时间:

      1. 测试平台编码:与UVM测试平台相比,所需的代码更少,并且测试平台在RTL交付的第一天就可以使用了。最早的RTL错误可以在第一个RTL版本发布后立即发现;

      2. 覆盖率闭合:证明是详尽无遗的,因此没有覆盖率闭合的步骤;

      3. 回归:由于详尽无遗的证明,因此不需要随机测试和夜间回归;

      4. 错误重现:这很简单,调试可以立即开始,而无需等待仿真重新运行失败的测试。

    5. 我们发现重复的模式,对称性和可重复使用的子块使我们能够使用前面描述的策略简化测试平台,从而节省了时间运行时而不必牺牲验证质量

     

    总体而言,我们发现E2E形式验证相对于UVM具有令人信服的成本优势,同时实现了与模拟/ UVM测试平台相比至少相同,甚至更好的验证质量

     

     

    未来的工作

     

    我们在E2E正式验证方面的经验揭示了我们认为仍有改进空间的几个方面。它们如下:

    • 覆盖率报告:在中断控制器和交叉开关的DV周期中,可用的覆盖率报告解决方案功能有限,并且与基于模拟验证的覆盖率报告不能很好地比较。具有易于与基于模拟验证的覆盖率报告进行比较的覆盖率报告,将使E2E形式化验证从管理角度更易于被接受。

    • 工具辅助的IP评估:可以使用工具(可报告有关E2E形式验证适用性的IP信息)来增强E2E形式验证候选对象的选择过程。访问关键数据点,例如最大逻辑锥深度,重复的子模块计数和门计数,使DVE可以更好地理解该模块的复杂性,并有助于引导他们对IP的适用性进行合理的判断。进行E2E形式化验证。

    • 集成的运行时间的减少:上述某些策略可以部分或全部自动化。下一代的形式化工具可以在“分而治之”方法中增加对对断言进行分组的支持,并可以确定何时某个模块将特别适合于“分层”策略。将这些功能预先集成到现有的形式化工具中,并利用我们的方法减轻DVE的工作量,从而加快流片进度。

    • 证明工具:证明工具通过分担验证标准接口的工作来加快流片进程,这与基于模拟验证中的VIP十分相似。随着更多可用的证明工具,更多IP可以使用E2E形式化验证。

     

     

    部署E2E形式化验证的建议

     

    • IP选择:并非所有IP都非常适合E2E形式验证。在考虑此方法时,至关重要的是仔细选择与该方法兼容的IP。通常,我们推荐在SVA中可以完全指定的IP,这些都是E2E验证的优先选项。更具体地说,此方法的理想候选者应具有较浅的逻辑锥度,较低的门数和较低的复杂度。

    • 增强断言质量:在我们进行研究时,现有的形式化工具并未提供类似于基于模拟指标的覆盖率跟踪解决方案。如果没有覆盖率解决方案,则必须在DE和DVE之间进行广泛的审查,以增强测试台的质量。评审应检查所有功能均具有显式检查;在未指定行为的情况下检查应失败;在任何定义的行为之前没有明确定义的触发器,并且所有约束不排除与IP的任何合法且有意义的交互,否则失败。但是,当有形式化的验证覆盖解决方案可用时,我们强烈建议将覆盖率跟踪与测试台审查配对。

    • 上述策略:我们还建议在部署适用于这些策略的IP上的E2E形式验证时,采用上述策略。使用这些策略可以减少断言计数和运行时间,而不会影响验证的质量。

     

     

    结论

     

    我们发现端到端形式验证非常适合某些类型的高度对称且控制路径密集的设计。与传统的基于UVM的方法相比,我们的方法能够节省验证投入和资源,并且能够达到与传统UVM测试平台至少相同的验证质量。

     

    原文来自:DVCon2017_USA, 点击阅读原文去路科官网下载DVCon2017论文合集,还有更多资料等你来哦!

     

     

    扫描上图二维码可直达课程页面,马上试听

    往期精彩:

    获取验证通关密语,就在本周日开班的验证V2课程

    30w+还送股送房?60+IC企业2019薪资全面攀升!

    UVM RAL模型:用法和应用

    我们准备做第二期线下培训,依旧认真且严肃

    如果你突然被裁员了,你的Plan B是什么?

    [彩虹糖带你入门UVM]

    理解UVM-1.2到IEEE1800.2的变化,掌握这3点就够

    展开全文
  • 认识形式化验证

    2019-04-03 16:37:00
    形式化验证是用逻辑来验证程序的可靠性,就是把一段程序用逻辑的方法证明一遍,证明它能得到预期的结果,没有bug。一般这类研究主要应用于昂贵的航天器材的操作系统、危险的医疗设备的程序之中。因为航天器材、医疗...

      软件开发中一般使用“测试”来找bug,这种方法只能找到bug,不能证明程序没有bug。
    形式化验证是用逻辑来验证程序的可靠性,就是把一段程序用逻辑的方法证明一遍,证明它能得到预期的结果,没有bug。一般这类研究主要应用于昂贵的航天器材的操作系统、危险的医疗设备的程序之中。因为航天器材、医疗设备牵扯到人的生命,如果操作系统出现错误,那么很危险,又不能用测试一遍一遍的测,所以用形式化验证来做。比如美国航天局NASA就会雇佣大批形式化验证的专家来验证他们操作系统的正确性
    学习这个方向,最好有比较好的逻辑知识(数理逻辑、拉姆达验算),最好比较了解程序(比如操作系统的设计、编译器的设计等)。
    这个方向是比较犀利的研究方向,但不大容易出论文,需要长时间积累才能发一篇好论文。

    这个方向只是科研方向,不适合找工作,如果你读完硕士打算找工作而不做研究,这个方向不适合。因为企业没人用形式化验证来验证程序。

     

    Formal Verification(形式验证)

      在计算机硬件(特别是集成电路)和软件系统的设计过程中,形式验证的含义是根据某个或某些形式规范或属性,使用数学的方法证明其正确性或非正确性。

    形式验证是一个系统性的过程,将使用数学推理来验证设计意图(指标)在实现(RTL)中是否得以贯彻。形式验证可以克服所有3种仿真挑战,由于形式验证能够从算法上穷尽检查所有随时间可能变化的输进值。

    形式验证

    形式验证的出现

      由于仿真对于超大规模设计来说太耗费时间,形式验证就出现了。当确认设计的功能仿真是正确的以后,设计实现的每一个步骤的结果都可以与上个步骤的结果做形式比较,也就是等价检查,如果一致就说明设计合理,不必进行仿真了。

    形式验证主要是进行逻辑形式和功能的一致性比较,是靠工具自己来完成,无需开发测试向量。而且由于实现的每个步骤之间逻辑结构变化都不是很大,所有逻辑的形式比较会非常快。这比仿真的时间要少很多。一般要做形式验证的步骤有:RTL和RTL。

    IC设计验证方法

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

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

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

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

    软件设计验证方法

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

    形式验证工具:

    Synopsys的Formality

    Cadence LEC(Logic Equivalence Check)

    形式验证的优点

    1. 由于形式验证技术是借用数学上的方法将待验证电路和功能描述或参考设计直接进行比较,因此测试者不必考虑如何获得测试向量。

    2. 形式验证是对指定描述的所有可能的情况进行验证,而不是仅仅对其中的一个子集进行多次试验,因此有效地克服了模拟验证的不足。

    3. 形式验证可以进行从系统级到门级的验证,而且验证时间短,有利于尽早、尽快地发现和改正电路设计中的错误,有可能缩短设计周期。

    ​区别

    验证实现工作包括将多种输进条件定义为测试计划的一部分、创建功能覆盖模型、开发测试平台、创建输进激励发生器、编写指导性测试以及执行测试、分析覆盖率指标、调整激励发生器以面向未验证的设计部分,然后反复这一过程。

    形式验证补充了模拟验证的不足,二者各有优势,互为补充,缺一不可。

    仿真是一种基于经验的模拟验证方法,通过反复试验试图查明缺陷,这要花相当多的时间尝试所有可能的组合,因此永远不会完整。另外,由于工程师必须定义和产生大量输进条件,他们的工作重点将是如何在非设计目标基础上分解设计。

    形式验证是穷尽式数学技术,使工程师仅关注设计意图。纯形式验证技术与仿真验证相反,专注于证实模块的端到端、直接对应微架构规范的高层要求,帮助用户戏极大进步项目的设计和验证产能,同时确保正确性。

     

    转载于:https://www.cnblogs.com/zhouwenfan-home/p/10649837.html

    展开全文
  • 基于梯形逻辑的联锁系统形式化验证方法
  • PAR平台中若干软件构件形式化验证技术研究
  • OSDI,SOSP这俩是计算机系统顶会,形式化验证最近在计算机系统、网络安全、内核等领域大放异彩,多次拿下顶会的Best Paper。本资源根据顶级大佬Wang Xi教授给出的论文列表进行整理,找出了最有价值的这几篇论文带你...
  • 形式化验证技术

    千次阅读 2014-10-13 21:46:50
    形式化验证就是基于已建立的形式化规格,对所规格系统的相关特性进行分析和验证,以评判系统是否满足期望的特性。形式化验证并不能完全确保系统的性能正确无误,但是可以最大限度地理解和分析系统,并尽可能地发现...
  • 形式化验证调研报告

    千次阅读 2018-10-17 14:56:24
    形式化验证调研报告 王立敏 中国科学院信息工程研究所 第五实验室 北京 中国100093 摘要2018年初,Spectre和Meltdown漏洞的发现,使得芯片安全备受重视。然而传统的基于仿真的芯片验证方法由于测试样例覆盖不完全...
  • 关于软件形式化验证

    万次阅读 2018-05-29 09:37:01
    形式化验证是用逻辑来验证程序的可靠性,就是把一段程序用逻辑的方法证明一遍,证明它能得到预期的结果,没有bug。一般这类研究主要应用于昂贵的航天器材的操作系统、危险的医疗设备的程序之中。因为航天器材、医疗...
  • web服务形式化验证

    2013-07-20 23:17:54
    web服务形式化验证,将Web服务组合建模为多智能体系统,采用时态知识逻辑模型检测工具MCTK刻画贷款协议Web服务实例,并验证相关的时态知识规范。在同一实验环境下,采用另一种时态知识逻辑模型检测工具MCMAS进行建模...
  • 针对处理器浮点运算单元,采用Cadence公司JasperGold工具对一些关键模块进行了形式化验证,对流水控制中的纠错码(Error Correcting Code,ECC)、软件结构寄存器(Software Architected Register,SAR)和计算单元中的...
  • 基于PRISM的分布式实时操作系统任务调度的形式化验证
  • 201806 智能合约安全之形式化验证研究报告.pdf
  • 为提高下一代列车运行控制(简称列控)系统安全计算机的系统兼容性,首先对其结构进行简要分析,并对管理机制进行设计,建立了管理单元状态转移模型,同时以形式化验证工具对模型的正确性进行了验证。在此基础上对...
  • 形式化验证 Gasper 共识机制 Gasper 是一个由信标链协议(即将到来的以太坊 2.0 网络的底层协议)实现的抽象的权益证明协议层。Gasper 的关键部分就是一套终局性机制(finality mechanism),用于保证交易的持存性...
  • 基于ATL(交替时态逻辑)对电子商务协议中的公平交换协议(Fair Exchange Protocols)进行形式化分析与验证,并选取了其中的一个电子合同签署协议进行形式化验证。用ATL语言来形式化描述公平交换协议,并使用ATS...
  • 从模型到可执行程序的形式化验证 可信编译器l2c 康烁 浙江迪捷软件 *本报告内容大部分来自王生原老师的l2c的相关材料 什么是形式化 什么是形式化 用非形式化的方式描述就是一个可辨认的字符集 外加一套既定的规则和...
  • Web服务组合验证是确保组合服务正常执行的...利用模糊推理Petri网算法进行可信度验证、计算服务组合的可信度及可达性,对于Web服务组合是一种可以推理的形式化验证方法。实验结果表明这种方法是一种很好的验证方法。
  • 形式化验证,英文是formal verification,是验证软硬件逻辑很重要的一种方法。特别是对于芯片开发、高安全性的系统开发来说,是非常必要。这主要是因为系统失败的代价很高,传统的测试也无法验证整个系统的安全性和...
  • 针对目前没有直接对事件图模型进行形式化验证的方法,提出了一种基于行为时态逻辑(temporal logic of action,TLA)的事件图模型形式化验证方法。该方法利用TLA语言能够同时表达模型行为与逻辑规则的特点及其与事件...
  • 总共包括synopsys若干讲芯片相关知识。... 芯片验证方法学近十年的发展极大的帮助到了验证工作效率和质量的提升,但是基于传统激励机制的...近几年越来越多的工程师把眼光投向了形式化验证,对比探讨两种方法学的异同。
  • 嵌入式实时系统对时间约束性、安全性和可靠性具有非常高的要求,但是传统的建模和形式化验证方法难以满足对系统的实时性和安全性的模拟和验证需求。通过对有色Petri网的时间属性进行扩展,提出了实时有色Petri网模型...
  • 操作系统形式化验证实践教程(7) - C代码的自动验证 上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作。 那么能不能让这个模式化的工作自动化起来,...
  • DAO、Parity、BEC 等著名项目的市值几乎一夜归零,都是由于智能合约漏洞引起,智能...形式化验证如何保障合约安全? VaaS 平台的作用及优势? 实际案例展示。 关键词:智能合约,形式化验证,VaaS 平台,安全漏洞。...
  • 提取系统功能和性能规范约束,利用消息顺序图对TSRS与外部系统之间的信息交互行为建模,并将系统MSC模型转化为UPPAAL中的时间自动机仿真模型,对系统的功能和性能要求进行形式化验证。验证结果确认了系统的安全性和受限...
  • 操作系统形式化验证实践教程(11) - 结构化证明语言Isar 结构化证明语言Isar基本语法 apply方法和by方法虽然可以完成功能,但是看起来更像是命令式语言。使用Isar语言,还可以写得更加形式化一点。 Isar的格式看起来...
  • 在智能合约的形式化验证过程中,需要专业的编程人员对不同模板的智能合约进行特征分析、模型建立和模型验证。现在市场上出现了一些一键式的智能合约形式化验证工具,据说可以最大程度的减少验证程序、发现bug,提高...

空空如也

空空如也

1 2 3 4 5 ... 20
收藏数 2,661
精华内容 1,064
关键字:

形式化验证