使用abstrct model代替real model

电子说

1.2w人已加入

描述

“空间爆炸”大大增加了formal工具处理的复杂度,在有限的资源内,难以达到收敛。所以采用一些abstraction的手段,是十分有效且必要的。正确的abstraction处理,使用abstrct model代替real model,不会影响目标结果,同时加速证明。

Abstraction vs. Reduction

abstraction不等同于简单的reduction,如下示例:

存储器

RTL中,当timer大于1000时,触发timeout。需要运行1000个cycle才会触发。

Reduction将阈值设置为5,缩减到5个cycle触发。

因为原RTL中还有一个heartbeat,可以重置timer,此时reduction不可以实现原RTL的所有场景(如heartbeat是由另一个计数器控制,阈值是100,而timer每次在5个cycle后就报timeout了,已不满足原有时序关系) Abstraction通过assume重写了rtl:1. heartbeat拉高,重置timer 2. heartbeat为低,timer非0,则下个cycle timer非0 3. heartbeat为低,timer为0,则下个cycle timer非0 Abstraction的方式可以复现原RTL的所有场景,同时缩短cycle depth.

存储器

采用Reduction还是Abstraction,需要case by case分析;有时Redcution也是Abstraction,理解RTL意图才是关键。

Complexity Manager

有些需要abstraction处理的地方是显而易见的,如较大的counter或者mem;我们也可以通过FPV工具自带的复杂度分析功能来提取哪些地方是收敛瓶颈,然后针对此处做abstraction处理。

当然并不是所有东西都要尽善尽美,要综合ROI考量;对于难以full proof的assertion,采用bounded的方式也是合理可取的,后节对bounded proof会补充介绍。

常见的abstraction策略总结如下几种:

Case Splitting

通过assume区分不同场景的case,单独运行。例如:assume property (mode == 2’b00); JasperGold也支持task分隔,更方便管理case splitting。

存储器

Counter Abstraction (Design Reductions)

FPV工具支持自动识别counter,jaspergold中可以通过abstract -counter处理;当然也可以手动处理;

Constant Propagation and blackboxing

对于不关心的功能,可以设置为常量,如.scan_mode(0); 对于不关心的逻辑,可以设置为blackboxing;

Design Size (parameter) Reduction

对于参数化配置的rtl,缩减参数配置;对于较大的mem,过约束地址访问空间;如下:

存储器

直接Reduction地址空间有一点不“安全”,这改变了原有RTL行为;需要配合simulation仿真加强验证结果的置信度;或者采用abstraction的方式,FPV工具也提供常见的mem,fifo abstraction model供用户快速部署;Jaspergold的abstraction model如下:

存储器

Cutpoints and Abstract Models

Cutpoint:切断rtl中的某个信号,其输出值不再受原有逻辑锥影响,FPV工具会赋值为任意值驱动后续逻辑。blackboxing的所有输出端口其实就是每个cutpoint的node.

Cupoint在不同FPV工具设置语法不同,JG中Stopat设置,VC Formal中snip_drive设置

存储器

单独cutpoint某个信号,不加约束,可能会assertion误报;一般需要额外assumption处理;如果简单几行assumption无法准确描述,需要glue logic或者glue moduel提供abstract model建模描述;

Initial Value Abstractions (IVAs)

FPV工具每次从reset状态开始,随着cycle的深入,遍历状态空间。如果某些状态需要较大的cycle depth,那么是否可以从一个中间状态开始呢?答案是可以的,从某个中间状态,而不是复位状态开始,我们称为“warm" state。Jaspergold可以通过abstrace -init_value约束一个初始值

存储器

Engine selection

fomal工具内置不同的算法引擎,每个App的适用场景不同,调用的engine不同;对于FPV app,不同类型的assertion,也和不同类型的engine相”友好“。每个engine的具体特性,验证人员不需要特别了解(有些engine需要配合使用才能发挥最大效果;有些engine同时运行可能冲突;有些engine一次只能处理一个assertion,有些可以并行处理多个),一般使用工具的auto模式,由工具自动编排调度engines即可。

不同FPV tool的Engine selection不同,以JasperGold为例:第一次运行,工具并不知道哪个engine最适合哪个property;而是通过采用多个engine并行处理某一个assertion,如果其中一个engine求解成功,则这些engine会被安排处理下一个未处理的assertion。

相当于多个engine”竞争“; 如果多个engine在限定时间内都没有求解出来,则会放弃当前assertion,安排处理下一个未处理的assertion。当第二次求解之前的assertion时,engine的求解时间会乘以一个系数,例如之前1min没有求解出,第二次可能会10min,第三次可能会100min. JG提供ProofGrid,可以图像化显示engine调度和进展;JG还提供了Proof Profiling Database,可以记录上次求解时的高效engien,下次运行优先调度此engien;Proof Cache则可以保留一些中间数据,如果rtl和env改动不大,下次运行可以使用这些中间数据,加速求解;

Property Writing

Formal Verification (二) FPV、APPs[1] 在这一篇中讲解如何书写友好的property;本节再补充三点:

1. Cut assertion 

如果一个end-to-end的assertion跨越的cycle很长,可以尝试在中间分隔多个assertion

存储器

2. livness assertion 

对于livness assertion(含有[0:$], eventually等无限周期的),如果可以使用固定周期值,建议使用固定值,切换为safety assertion。

存储器

livness assertion的求解,工具会在stem后寻找一个loop,当找到这个loop时,就相当于找个一CEX,此assertion被证伪。

engine对于loop的寻找是很艰难的,所以livness assertion一般很难被full proof。

当发现CEX时,也不一定是RTL的问题,可能是缺少fairness constraints. 例如两个入口port(A,B), 一个出口port(C),C round-robin处理A,B的burst数据;断言当A port接收数据后,无限期 s_eventually周期后,C port一定把A的数据送出;断言当B port接收数据后,无限期 s_eventually周期后,C port一定把B的数据送出;此时两个livness assertion fail。

CEX场景是A一直发送数据,C一直输出A的数据,B发送的第一笔数据被无限期阻塞。实际情况是A不会无限期连续发送数据,总会停止发送。可以加上fairness constraints约束A的最大长度为某一个值。同理B也是。

存储器

1. Symbolic Variables 

Symbolic Variables有很多叫法例如Pseudo-constants 、Free variables,采用这总方式书写assertion,不仅减少assertion数量,便于描述assertion,对工具也更友好。如下示例:

 

 genvar i;
  generate for (i = 0; i < N_SOURCE; i++) begin : gen_rv_plic_fpv
    `ASSERT(LevelTriggeredIp_A, $rose(rv_plic.ip[i]) |->
            $past(rv_plic.le[i]) || $past(intr_src_i[i]), clk_i, !rst_ni)
  end

 

上述通过generate生成多个并行重复的assertion;而使用Symbolic Variables,声明一个变量src_sel,并加上合理的约束,可以实现多个并行assertion的效果。

 

 logic [$clog2(N_SOURCE)-1:0] src_sel;
  `ASSUME_FPV(IsrcRange_M, src_sel >= 0 && src_sel < N_SOURCE, clk_i, !rst_ni)
  `ASSUME_FPV(IsrcStable_M, ##1 $stable(src_sel), clk_i, !rst_ni)
  `ASSERT(LevelTriggeredIp_A, $rose(rv_plic.ip[src_sel]) |->
          $past(rv_plic.le[src_sel]) || $past(intr_src_i[src_sel]), clk_i, !rst_ni)

 

小结

上述介绍的多种方法,都是为了降低复杂度;需要case by case的分析采用哪一种;还有一些方法属于更高阶的使用,需要tool by tool。如JasperGold提供SST(State-Space Tunneling)功能,通过增加helper assertions加速求解。

FPV for cache

验证cache采用FPV的手段,是一个典型的场景,会覆盖上述提到的所有abstraction strategy。

以icache为例:icache大小32 KB,4路组相连,每个cache line大小是32B,一共有256组set;cache line size是32 Bytes,offset为5位;256组,index为8位,剩下的为tag部分,占用35位,其中tag的最高bit为valid flag;tam部分放在tag_mem存储;data放在data_mem存储;当发生cache evict时,根据LRU(least recently used)策略替换某一个way的cacheline,lru数据放在lru_mem存储,下图未画出(Cache的基本原理[2]):

存储器

Case Splitting : 将assertion归为不同task分别运行;

 Counter Abstraction : 执行cache flush时,内部counter会递增,依次flush 每个cacahe line。对整个空间做flush不现实,需要对counter做abstract; 

Constant Propagation and blackboxing : 测试function feature时,约束mbist为disabel constant;对不关心的逻辑blackboxing; 

Design Size (parameter) Reduction : icache可能支持多bank,不同组相连,不同cache line size的配置,选取一个最小的特征配置; 

Cutpoints and Abstract Models : 为了减少mem空间,需要过约束取指端口命中的set数量,同时对tag_mem,data_mem,lru_mem做abstraction处理; 

Initial Value Abstractions : FPV默认从复位开始,icache复位后自动flush cache,所有每次都是从invalid状态开始 ”震荡“ 状态空间;可以利用IVAs给tag_mem,data_men,lru_mem使用约束赋合理的初始值,加速求解; 

Cut assertion : 对从取指到icache返回指令的断言,可以看作一个end to end的断言,如果cache miss, cycle-depth会增加,FPV求解难度加大,可以尝试cut assertion; 

livness assertion : 上述end to end的assertion,一般也是livness的;可能需要添加一些fairness constraints;一般livness assertion都是bounded proof; 

Symbolic Variables : 对于同一set不可能出现相同tag的断言,采用Symbolic Variables的方式书写assertion;





审核编辑:刘清

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

全部0条评论

快来发表一下你的评论吧 !

×
20
完善资料,
赚取积分