Formal Verification (三) abstraction strategy、reduce complexity for convergence

admin管理员组

文章数量:1534215

“空间爆炸”大大增加了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 在这一篇中讲解如何书写友好的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也是。

3. 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的基本原理）：

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；

对于icache采用simulation+fpv的验证手段是十分常见的，可以参考🔗：DVcon-2020 Formal Verification of Macro-op Cache for Arm Cortex-A77, and its Successor CPU

本文标签： abstractionVerificationformalStrategyconvergence