使用abstrct model代替real model

“空间爆炸”大大增加了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,对工具也更友好。如下示例：

genvari;
generatefor(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；

审核编辑：刘清