硬核产品 “芯天成”形式验证平台EsseFormal系列

引言

模型检查也称作属性检查，是一种基于设计属性的形式验证方法：通过在设计中使用 SVA（SystemVerilog Assertion）描述待验证的属性，并验证设计是否满足规范。属性验证工具一般涉及三种形式的属性：

1、断言属性Assertion：用于检查设计的行为是否符合规范

2、约束属性Assumption：用于约束设计行为

3、覆盖率属性Cover：用于监视预期事件是否发生

本期我们将了解芯天成EsseFormal形式验证平台的EsseFPV工具，包括其主要功能、优势及应用。

产品简介

芯天成EsseFPV 工具使用形式化技术验证 RTL 是否符合设计规范，为用户提供快速的错误检测以及预期设计行为的端到端的验证。

EsseFPV不需要搭建测试平台，可在仿真之前就能实现验证，适合设计早期的 bug 追踪。同时，EsseFPV支持断言属性、约束属性、覆盖率属性的验证，可在设计中更快地发现bug并提供反例。此外，EsseFPV通过端到端的验证可确保设计功能的高正确率。

产品优势

1、可定制化的属性验证服务

2、支持多种验证引擎

3、支持在TCL脚本中对属性是否执行、是否禁用进行控制

4、支持在TCL 脚本中为 RTL 设计添加属性：可添加断言属性、约束属性或覆盖率属性

5、支持通过命令行控制验证属性开始执行的时间，并支持跨越周期跳跃执行属性验证

6、可快速定位设计bug

7、支持使用波形调试结果

产品应用

交通灯案例——检查设计行为的断言

交通灯设计作为数字系统设计的入门案例，其包含时序信息和逻辑信息，该案例有助于我们更好地理解EsseFPV的基本原理，理解 EsseFPV 工具的使用方式。

一个基本的交通灯设计主要包含以下要求:

红绿黄三种灯色的出现需要满足规定的顺序，

即绿灯后为黄灯，黄灯后为红灯，

红灯后为绿灯。

三种灯色之间需要间隔一定的时间。

按照以上要求，工程师将设计出RTL代码：

部分交通灯RTL代码

我们可以看到设计工程师将RTL 设计的断言内容（蓝色标注）采用直接嵌入的方式放置在设计当中，该断言用于检测灯色的顺序，即要求黄灯倒计时结束后，需要亮红灯。由于该断言采取的是 A |=>B 的形式，即包含先行算子，因此我们需要开启EsseFPV的空成功检查功能（check vacuous），排除设计假性通过的可能。

验证断言的结果

验证结果为vacuous(空成功)，表示先行算子状态始终为假（0），即当灯为黄灯时，剩余时间不可能为 0 或者时当剩余时间为 0 时，灯不可能为黄灯，这明显出现了时序性错误。此时工程师需要在原有RTL代码上进行对剩余时间Counter项的修改，然后再次使用EsseFPV进行验证：

第二次验证断言的结果

第二次结果为 falsified，说明RTL设计功能跟预期不符。EsseFPV工具在遇到 falsified 时，会将反例写入生成的 testbench 文件，并生成对应的 vcd 文件和波形图（如下），便于工程师调试设计代码。

除了检查设计行为的断言，EsseFPV还可以约束形式化验证环境的假设以及监视预期事件的覆盖属性。

目前我们已经详细介绍了芯天成EsseFormal平台的三款工具，分别是EsseFCET、EsseFCEC、EsseFPV。最近，芯天成形式验证平台又结硕果，国微芯研发团队推出了EsseCC等工具，可用于信号的连通性检查和特定功能的验证。让我们期待新工具的正式发布。