vc_formal_dpv

介绍VC Formal DPV。

简介

VC Formal DPV工具是Synopsys公司VC Formal中的一个子工具，DPV是Datapath Validation。

它与FPV不同的是，FPV是基于property verification，采用断言的方式进行formal，主要用于控制流的formal。而DPV专注于数据流的formal，它非常适用于CPU/GPU/DSP/AI中的ADD/SUB/MULT/DIV/SQRT等运算单元的验证。

对于数据流的formal，其挑战是巨大的数据空间，如果简单的遍历，是不可能完成的任务，像图中说的64bit的乘法可能需要3.5*10^21年。

三类等价性验证：

• Transactional Equivalence：其一般是c/c++与RTL对比，而c/c++是没有时间概念的，RTL是有时序的。DPV属于这种。
• Sequential Equivalence：每一个时钟cycle都能对比上，一般是RTL和RTL对比。
• Combinational Equivalence：输入和输出能完全对上，RTL和Gate对比。

VC Formal DPV有如下特点：

• 能支持c/c++和c/c++的对比；能支持c/c++和RTL对比；能支持RTL/RTL对比。
• 不需要testbench就能完成signoff

DPV流程

以下是DPV的流程：

• compile SPEC
  • 编译spec，也就是reference，一般是c/c++
• compile IMPL
  • 编译implementation，一般是RTL
• compose
  • 将SPEC和IMPL结合在一起
• solveNB
  • 证明其等价性
• simcex
  • debug fail outputs

Quick Start

以下用一个最简单的例子，来展示如何使用DPV。

Prepare environment

设置环境变量。

export VC_STATIC_HOME=/tools/synopsys/vc_static/P-2019.06
export PATH=${VC_STATIC_HOME}:$PATH
export SNPSLMD_LICENSE_FILE=27000@etx-soc
export LM_LICENSE_FILE=27000@etx-soc

Create Folders

创建如下目录 及文件：

• rtl
  • add.sv
  • file_a
• c
  • add.cc
• tcl
  • command_stript_add.tcl
• run
  • 运行目录

RTL

编写add.sv如下，里面特意构造了一个错误。

c

编写add.cc如下。

command_script_add.tcl

编写tcl脚本如下：

运行

执行以下命令：

$ cd run
$ vcf -verdi -f ../tcl/command_script_add.tcl -fmode DPV

将打开如下界面

在tcl shell中执行以下命令，就开始证明了。

vcf> make
vcf> run_main

很快可以看到，status变成失败。

双击status的x，可以打开波形进行debug。

将RTL修改正确之后，重新运行，可以看到状态变为正确。