0
  • 聊天消息
  • 系统消息
  • 评论与回复
登录后你可以
  • 下载海量资料
  • 学习在线课程
  • 观看技术视频
  • 写文章/发帖/加入社区
会员中心
创作中心

完善资料让更多小伙伴认识你,还能领取20积分哦,立即完善>

3天内不再提示

Formal Verification (二) FPV、APPs介绍

rfdqdzdg 来源:IC Verification Club 2023-08-28 09:13 次阅读

SVA in Formal

FPV对不同的SVA Property,调用合适的算法engine进行建模,依据算法模型从初始状态Reset state对DUT所有的input自动施加激励,随着cycle的depth增加,逐渐穷尽状态空间。

71b3f62c-4537-11ee-a2ef-92fbcf53809c.png

The full space of all possible RTL state values: 最外层的紫方框为RTL的所有可能存在的状态空间(input + state element(dff,latch))。

The reset states:初始状态,一般从reset复位开始。

The reachable states:从reset state可以,自动对input施加激励,可以达到的状态。(所以紫方框以内绿椭圆以外的空间,是无法达到的空间,例如RTL中的dead code)Assumptions:使用SVA的assume对DUT进行约束;橙色椭圆型,约束缩小了状态空间。

Assertion: 使用SVA的assert对property进行断言;断言属性定义了模型的行为,例如assert property: ( @(posedge clk) clr |=> ((overfloat==0)&&(cnt==0)));断言了在clk上升沿采样时,若clr为高(先行算子anteceden成功),下一个clk上升沿采样到的overfloat和cnt都为0(后续算子consequent);而Formal工具要做的就是穷尽状态空间找出一个counter-exampleCEX反例,进行falsified证伪,例如overfloat和cnt都不为0或者只有一个为0;如果CEX出现,而assertion为golden,则就说明DUT不满足spec。

Asser1: pass,因为这个CEX不满足assumptions的约束,不是一个有效状态。

Assert2: pass,因为这个CEX本身不是可以达到的状态。

Assert3: fail,有效状态和约束内,出现了一个CEX。

Cover Points: 使用SVA的cover对property设置覆盖点;相当于设置一个观察点,Formal工具会穷尽状态空间,找到一个满足要求的状态;

Cover1: 该覆盖点被cover

Cover2: 该覆盖点在约束之外,unreachable

Cover3: 该覆盖点在有效空间之外,unreachable

VC Formal定义了Assertion和Cover Points的结果如下:

Assertion:proven: assertion pass,穷尽状态空间也找不到一个CEXfalsified:assertion fail,出现不满足断言的CEXinconclusive: Formal在N个cycle depth内,没有找到CEX,属于Bounded Proof,有界证明,这个"界“bounded (safe) depth就是N个cycle depth。vacuous:对于包含蕴含操作符|->|=>的property,如果antecedent一直未被触发,也一定不会出现CEX,此时为空成功vacuous success。vacuous在Simulation中经常出现,因为施加的有限激励,没有触发antecedent成功。但是在Formal中,需要引起注意。

Cover Points:Covered: 覆盖Uncovered: 未覆盖

the SVA differences

在Simaltion和Formal中,SVA的使用略有不同:

71cf6470-4537-11ee-a2ef-92fbcf53809c.png

Simulation中的assume和assertion作用相同,不起到约束的作用;而Formal中,assume实现约束的作用;对于Simulation的vacuous success,并不会报错引起用户注意,一般建议对property同时做assert和cover处理。

Sequential depth

Sequential depth:也就是上文提及到的Cycle depth;较大的Sequential depth,容易产生inconclusive的结果。

71fd7f5e-4537-11ee-a2ef-92fbcf53809c.png

Assertion Logic Contributes to State Space

COI

COI(CONES OF INFLUENCE):COI是Formal工具对property的逻辑电路映射,也被称作Logic Cones逻辑锥。COI包含property的所有input和state element,这些决定了不同的输出结果。

7212816a-4537-11ee-a2ef-92fbcf53809c.png

Formal工具对一个property解析生成的COI Schematic

72263d18-4537-11ee-a2ef-92fbcf53809c.png

从用户角度,我们不必关心一个property的COI具体是什么样子;用户创建的所有property的COI集合对DUT RTL的覆盖情况,类似于Simulation中的Code coverage,称为Property Density。

The suggestion of SVA for Formal

formal model从SVA中提取,所以SVA的书写方式,也会影响Formal的效率,推荐的SVA Coding Guidelines可以参考《VC_Formal_UGAppendix B。下面介绍一些常见的assertion”技巧“:

uniform format

assertion的书写,需要遵循同一的格式,每条assertion有相应的文档记录;每条property都有可读性的lable标注;可以采用一些宏定义,简化assertion的书写,参考:prim_assert.sv[4]当assertion的clock,reset都是同一个时,可以声明default clocking和default disable iff,简化书写。

Immediate VS Concurrent

虽然立即断言在一些情况下等效于并发断言,如下:

//ConcurrentAssertion
assert_overfloat_func:assertproperty(`clk_rst$rose(overfloat)|->$past(cnt==4'hF));

//ImmediateAssertion
always@(posedgeclk)
if($rose(overfloat)&&(rstn==1))
assert_overfloat_func_2:assert($past(cnt==4'hF));

但是建议使用并发断言,Formal工具对蕴含操作符的支持更好。

Try use implication

不建议直接对sequence进行断言,sequence会在每个cycle都被检查;推荐使用蕴含操作符的方式。

//BAD
propertysend_header_payload;
@(posedgeclk)disableiff(reset)
(enable##1header##1payload[*16]);
endproperty
//GOOD
propertysend_header_payload;
@(posedgeclk)disableiff(reset)
$rose(enable)|=>header##1payload[*16];
endproperty

SVA Modeling Layer Code

可以通过增加Auxiliary Code,简化property的书写难度;如下:

moduleassert_top(inputrstn,inputclk,inputA,
input,B,inputC,inputwr,inputrd);
//Requirement:inputsA,B,Caremutuallyexclusive
wire[2:0]my_bus={A,B,C};
a_abc_mutex:assertproperty(@(posedgeclk)$onehot0(my_bus));
//Requirement:Nomorethan5outstandingwr’s(withoutard)
//andnordbeforewr
reg[2:0]my_cnt;
always@(posedgeclkornegedgerstn)
if(!rstn)my_cnt<= 3’b000;
        else
            if ( wr && !rd) my_cnt <= my_cnt + 1;
            else if (!wr && rd) my_cnt <= my_cnt – 1;
            else my_cnt <= my_cnt;
a_wr_outstand_le5: assert property (@(posedge clk) my_cnt <= 3’d5 );
a_no_rd_wo_wr: assert property (@(posedge clk) !((my_cnt == 3’d0) && rd));
endmodule

use function

assertion中可以调用funciton。

//Computenextgrantforround-robinscheme
functionlogic[3:0]fv_rr_next(logic[3:0]req,logic[3:0]gnt);
fv_rr_next=0;
for(inti=1;(i<4); i++) begin
        if (req[(fv_which_bit(gnt)+i)%4]) begin
          fv_rr_next[(fv_which_bit(gnt)+i)%4] = 1;
          break;
        end
    end
endfunction

Page81_rr_next:  assert property (((opcode == NOP) && 
    (|gnt == 1) && (|req == 1) && (|(req&gnt)==4'b0)) |=>(gnt==fv_rr_next(req,gnt)))
else$error("Violationofroundrobingrantpolicy.");

as SIMPLE as possible

将一个大的assertion才分为多个小的assertion

$rose(START)|=>(ENABLE&&~START&&~STOP)[*7]
##1(ENABLE&&~START&&STOP)|=>
(~ENABLE&&~START&&~STOP);

$rose(START)|->~ENABLE##1ENABLE;
$rose(ENABLE)|->(~START&&~STOP)[*7];
$rose(STOP)|->ENABLE##1~ENABLE;
$fell(START)|=>##5$rose(STOP);

as SHORT as possible

尽量缩短Cycle Depth,使用[0:$]或者太大的时间delay不利于formal分析。

a5:assertproperty@(posedgeclk)a|->(##[0:$]b);
a6:assertproperty(@(posedgeclk)disableiff(~rst_n)A##1B|=>C##[1:100]D);

use Systemverilog

采用可综合的systemvrilog语法,如interface,struct等,使用更便捷;像s_eventually, 在sv09才支持。

Formal Property Verification

以一个counter做简单的演示:

modulecounter(
inputclk,
inputrstn,
inputen,
inputclr,
outputcnt,
outputoverfloat
);

reg[3:0]cnt;
regoverfloat;

always@(posedgeclk,negedgerstn)
begin
if(!rstn)
cnt<= 4'b0;
    else if (clr)
       cnt <= 0;
    else if (en & (cnt!=4'hF))
       cnt <= cnt + 1;
end


always@(posedge clk,negedge rstn)
begin
    if(!rstn)
       overfloat <= 1'b0;
    else if (clr)
       overfloat <= 1'b0;
    else if (cnt==15)
       overfloat <= 1'b1;
end

`ifdef FPV

`define clk_rst @(posedge clk) disable iff (!rstn)


//ASSUME
assume_en_clr_conflit: assume property (`clk_rst !(en && clr));

//COVER
cover_clr_overfloat: cover property (`clk_rst $fell(overfloat));
cover_cnt_value: cover property (`clk_rst (cnt==20));

//ASSERT
assert_clr_func: assert property(`clk_rst clr |=>((overfloat==0)&&(cnt==0)));


propertyp_en_func;
inttmp;
`clk_rst(en,tmp=cnt)|=>if(cnt!=4'hF)(tmp+1==cnt);
endproperty

assert_en_func:assertproperty(p_en_func);

assert_clr_overfloat:assertproperty(`clk_rst$fell(overfloat)|->$past(clr));
//PASS
assert_overfloat_func:assertproperty(`clk_rst$rose(overfloat)|->$past(cnt==4'hF));
//WRONGassertion
assert_overfloat_func_fail:assertproperty(`clk_rst(cnt==4'hF)|=>overfloat);

//ImmediateAssert
always@(posedgeclk)
if($rose(overfloat)&&(rstn==1))
assert_overfloat_func_2:assert($past(cnt==4'hF));

`endif
endmodule

Result:vacuity栏为property的先行算子成立的cycle depth。witness栏为property的后续算子成立的cycle depth。对于assert_overfloat_func这个property,witness早于vacuity1个cycle,是因为$past()是对过去的判断。

723756d4-4537-11ee-a2ef-92fbcf53809c.png

Initial State定义clk,rstn;从复位状态开始,Formal工具自动对input信号灌入激励。

#ClockDefinitions
create_clockclk-period100
#ResetDefinitions
create_resetrstn-senselow

#InitialisationCommands
sim_run-stable
sim_save_reset

ASSUME

增加了en和clr不可能同时为高的约束。

COVER

增加一些关心的cover point,工具可以快速地跑出对应波形:例如$fell(overfloat)的cover:

726468e0-4537-11ee-a2ef-92fbcf53809c.png

200ns:完成复位2000ns:cover point match(注意采样的上升沿前的数据)

对于(cnt==20))则是uncover,cnt最大值为15。

ASSERT

assert_overfloat_func_fail: assert property (`clk_rst (cnt==4'hF) |=> overfloat);这个propery断言失败,被工具找到了一个CEX: 当cnt==4'hF时,同时拉高clr,overfloat就不会为高了。

727dad64-4537-11ee-a2ef-92fbcf53809c.png在这里插入图片描述

assertion annotation:

72ad42ae-4537-11ee-a2ef-92fbcf53809c.png

**ENGINE** Type栏的e1,s6,t3为算法引擎的代号;工具会根据property的特性选择合适的算法,调用相应的引擎处理;VC Formal中的engines:

72c1d3cc-4537-11ee-a2ef-92fbcf53809c.png

常见算法为:

•Binary Decision Diagrams orBDD

•"SATisfiability" Proofs orSAT

•Bounded Model Checking orBMC

•Craig Interpolation, usually shortened to "Craig"

•Property Directed Reachability orPDR

一般使用工具默认分配的engine,当然用户也可以自己指定;VC Formal提供了多种引擎编排的recipes,适用FPV不同的使用场景。

JasperGold Result

72f24fca-4537-11ee-a2ef-92fbcf53809c.png

CEX wave:

7309adc8-4537-11ee-a2ef-92fbcf53809c.png

JasperGold中的engines:

7323d892-4537-11ee-a2ef-92fbcf53809c.png

FPV的使用场景

design exercise FPV

FPV不需要搭建平台和手动施加激励,适合快速的在一些新设计的RTL上跑一些基础功能;例如上一节$fell(overfloat))这个cover point,如果通过Simulatin,需要搭建testbench并详尽地施加每一拍的激励;而使用Formal,设计人员不需要关注整个过程,只关注最终结果,工具会自动施加相应的激励并达到你想要的结果。

所以当你有以下需求时,可以考虑使用design exercise FPV:

1.对于新设计的模块,想要跑一些基础功能进行确认

2.在验证人员的验证平台还没有准备好时,需要自己提前做一些简略地验证

3.接手遗留的RTL代码,可以跑一下FPV,结合波形加深对特定功能的理解

设计人员自己跑FPV,对RTL内部细节很了解;思路一般是:首先增加感兴趣的cover point;再添加一些assumption,可以过度约束;先跑出一些简单功能的波形;增加一些assertion,做检查;接着添加一些复杂功能的assertion和cover point,并逐渐放宽assumption;跑FPV并不是可以一次性把所有property都写完备,需要"wiggle"几轮,多次调试property;

有些公司对IP开发有额外的断言标准要求,例如property应该占RTL总代码行数的三分之一;这些property既可以用于formal,也可以用于simulation。《Assertion-Based Design》,《Creating Assertion-Based IP》书籍中介绍了相关经验。

Bug hunting FPV

当你有以下需求时,可以考虑使用Bug hunting FPV:

1.你所验证的模块有很多corner cases,需要额外的FPV验证保证完备性

2.Simulation回归random case时,陆续发现新的error,需要额外的FPV验证提高置信度

3.对于一个成熟的模块,加了一个新的feature,需要额外的FPV验证

Bug hunting FPV是Simulation的补充验证手段,采用更高层级的assertion,加入过约束,将注意力集中于某一个功能点;

full proof FPV

对一个设计只采用FPV进行验证,保证设计功能100%符合spec;这个从理论上是完全可行的,也是Formal Verification的初衷:只要property是完备的,正确的,相对于RTL,就可以建立一个golden model,遍历RTL的所有状态空间,保证100%正确。当你满足以下条件时,可以采用full proof FPV:

1.待测设计有一个详细的规格书或者一个包含所有功能点的表格

2.待测设计是一个标准接口,可以采用商业的AIP进行验证

对于full proof FPV,每种Formal工具都有推荐的sign-off流程,来保证验证的完备。

VC Formal的推荐流程如下:

73365602-4537-11ee-a2ef-92fbcf53809c.png

JasperGold的推荐流程如下:

734ee550-4537-11ee-a2ef-92fbcf53809c.png

通过收集覆盖率,保证property的完备,完成sign-off工作。具体后文介绍。

APPs

formal tool除了FPV,还提供了其他适用不同场景的APPs,如对于pinmux可以采用connectivity连通性检查,对于寄存器的访问采用register检查,对于一块mem,是否存在其他非法访问路劲,可以才用security检查;这一类app都是FPV的衍生,通过提供一文件或约束,工具自动产生property,调用最佳engine处理。相较于FPV,学习成本低。对于汽车产品,有额外的Functional Safety要求,工具会自动对rtl注错分析其影响结果。

VC Fomrla Apps:

7376437a-4537-11ee-a2ef-92fbcf53809c.png73a0b696-4537-11ee-a2ef-92fbcf53809c.png

对于以上Apps, 可能除了DPV, JasperGold都有对应的Apps.






审核编辑:刘清

声明:本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人,不代表电子发烧友网立场。文章及其配图仅供工程师学习之用,如有内容侵权或者其他违规问题,请联系本站处理。 举报投诉
  • 处理器
    +关注

    关注

    68

    文章

    19169

    浏览量

    229171
  • 逻辑电路
    +关注

    关注

    13

    文章

    494

    浏览量

    42581
  • SVA
    SVA
    +关注

    关注

    1

    文章

    19

    浏览量

    10119
  • DUT
    DUT
    +关注

    关注

    0

    文章

    189

    浏览量

    12344
  • FPV
    FPV
    +关注

    关注

    0

    文章

    16

    浏览量

    4476

原文标题:Formal Verification (二) FPV、APPs

文章出处:【微信号:数字芯片设计工程师,微信公众号:数字芯片设计工程师】欢迎添加关注!文章转载请注明出处。

收藏 人收藏

    评论

    相关推荐

    什么是FPV?怎样去搭建FPV验证环境呢?

    、顶层连接、状态机和门控等等。、搭建FPV验证环境(一)—编译设计为了更好地说明FPV的实际应用,本文首先基于一个密码锁的例子展示FPV验证的各个步骤。本文首先
    发表于 06-27 16:40

    搭建FPV验证环境之创建assert与执行FPV简析

    如果断言FAIL了,我们还需要进行2次定位以确定FAIL的根本原因。搭建FPV验证环境(四)—执行FPV现在所有FPV需要的元素已经在前面的文章依次介绍过了,我们可以开始真正执行
    发表于 06-27 17:15

    一、什么是FPV

    一、什么是FPVFPV是一种用来证明使用SVA或类似的语言描述的RTL属性的方法。上图说明了一个FPV工具执行的框图。FPV的输入:1、RTL模型2、要证明的一组属性:asserti
    发表于 06-28 14:35

    FPV设计的状态空间主要由什么因素决定的

    ;1} ,第个周期后到达状态{2} ,直到达到最终状态。FPV则会探索每个时钟周期中所有可能的状态,如图中不断增长的椭圆所示。如果FPV工具达到
    发表于 09-14 14:11

    A Roadmap for Formal Property

    What is formal property verification? A natural language such as English allowsus to interpret
    发表于 07-18 08:27 0次下载
    A Roadmap for <b class='flag-5'>Formal</b> Property

    路线图正式产权核查

    What is formal property verification? A natural language such as English allowsus to interpret
    发表于 07-18 08:28 0次下载
    路线图正式产权核查

    Advanced Formal Verification

    been observed that verification becomes the major bottleneck in design flows, i.e. up to 80% of the overall design
    发表于 07-21 09:10 0次下载
    Advanced <b class='flag-5'>Formal</b> <b class='flag-5'>Verification</b>

    Functional Verification Coverage Measurement and Analysis

    What is functional verification? I introduce a formal definition for functional verification
    发表于 07-25 14:48 0次下载
    Functional <b class='flag-5'>Verification</b> Coverage Measurement and Analysis

    功能验证覆盖测量与分析

    What is functional verification? I introduce a formal definition for functional verification
    发表于 07-25 14:49 0次下载
    功能验证覆盖测量与分析

    AVM Based Unified Verification

    This paper addresses the problem of current SoC functional verification productivityby describing a
    发表于 07-04 11:39 17次下载

    FPV58口系列智能涡街流量计技术资料

    概述: FPV58□系列智能型涡街流量计,由FPV580、FPV581、FPV582组成。 〖1〗FPV580=
    发表于 08-26 12:09 16次下载

    新思科技升级Verification Continuum平台继续引领技术

    新思科技近日发布新版Verification Continuum™平台,将各种验证工具进行新的原生集成,实现高达五倍的验证性能。Verification Continuum平台基于新思科技开发的高速
    的头像 发表于 06-11 08:42 4751次阅读

    分享一些形式验证(Formal Verification)的经典视频

    前段时间很多朋友在微信群里讨论Formal验证的视频资料问题,今天整理好了,分享给大家。
    的头像 发表于 02-11 13:15 800次阅读
    分享一些形式验证(<b class='flag-5'>Formal</b> <b class='flag-5'>Verification</b>)的经典视频

    Formal Verification的基础知识

    通过上一篇对Formal Verification有了基本的认识;本篇将通过一个简单的例子,感受一下Formal的“魅力”;目前Formal Tool主流的有Synopsys的VC
    的头像 发表于 05-25 17:29 2485次阅读
    <b class='flag-5'>Formal</b> <b class='flag-5'>Verification</b>的基础知识

    数字验证中Formal Verification在国内的应用以及前景如何?

    这种中型规模的RTL如果用simulation,妥妥的一分钟能跑十几个sanity case,所以性价比实在太低。尤其是碰到带memory的设计,用formal简直就是噩梦(不过工具好像可以替换掉memory的逻辑,你也可以dummy掉data payload,但控制逻辑的data path同样不短)。
    的头像 发表于 06-26 16:38 1281次阅读