jaspergold c2rtl 验证一个基于srt的除法模块(没验出来)_formal c2rtl

基于SRT的除法模块流程大致如下：

假设除法模块参数如下：

module div_top(clk,reset,
                a,b,c,//a/b=c
                ivalid,iready,//输入握手
                ovalid,oready)//输出握手
 
//cycle delay 4~20

假设除法c model为：

#include "jasperc.h"
#include "stdint.h"
uint64_t div(uint64_t a,uint64_t b);
 
int main() {
 
uint64_t  a, b;
uint64_t  out;
int64_t a_;
int64_t b_;
 
JG_INPUT(a);
JG_INPUT(b);
a_ = a;
b_ = b;
 
out = a_ % b_;
JG_OUTPUT (out);
}

div cycledelay是和输入相关的，在验证的时候，一种方法是可以将输入分组，每一组对应固定n个cycledelay，每组对应一个task(我嫌麻烦)；另一种就是写一个fifo，然后将c的输出放到fifo中，当rtl的ovalid=oready==1的时候pop比对。

构造fifo如下：

module sync_fifo(clock, reset,
                ivalid, iready, 
                ovalid, oready,
                data_in, data_out);
//fifo 深度最好是可容忍的最小值
 
always(@ posedge clock) begin
    if(ivalid&iready)begin
    //push data_in
    end
end
//其他逻辑。。。。
endmodule 

编写tcl脚本：

check_c2rtl -compile -spec div.c 
 
check_c2rtl -analyze -imp -sv div.v
check_c2rtl -elaborate -imp -top div 
 
 
check_c2rtl -setup
 
analyze -repository 1 -sv fifo.sv
elaborate -repository 1 -top fifo -disable_auto_bbox 
//这里如果不添加-disable_auto_bbox，c2rtl会自动视fifo为一个黑盒，fifo的输出会变成随机数
connect -repository 1 \
	fifo fifo_inst \
	-connect clk div.clk \
	-connect reset div.reset \
	-connect ivalid div.ivalid \
	-connect iready div.iready\
	-connect ovalid div.oready\
	-connect oready div.oready\
    -connect data_in out\  #这里连接fifo的data_in和c model的out
 
//添加clk reset
clock
reset
 
//添加assume  assertion cover; 
assert {div.ovalid&div.oready |-> fifo.data_out == div.c}
//virtual_net
 
//其他脚本

额外写的fifo需要analye 和 elaborate，添加连接，添加assertion对比输出时将fifo输出和rtl输出进行对比。

也可以直接在fifo模块中添加assertion，c2rtl会自动提取assertion。

模块位宽比较小时可以验全，位宽在32bit以上时基本验不出来。