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

设置环境变量。

1
2
3
4
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脚本如下:

运行

执行以下命令:

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

将打开如下界面

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

1
2
vcf> make
vcf> run_main

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

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

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