如何通过SymbiYosys中的归纳法？

编程问答 2022-06-09

问题描述

我对形式验证非常陌生，我从SymbiYosys开始了形式验证。 我已经在System Verilog中编写了一些用于学习形式验证的代码，我能够通过BMC并覆盖该代码，但是无法归纳（未知状态）。

我对形式证明没有太多的了解，但是我目前对归纳证明的理解是：我的设计将在将来的时间在断言状态开始，并且我所有的寄存器都将设置为某种状态，这将触发我的断言然后从该状态开始，SymbiYosys引擎将尝试以相反的时间步长找到一个有效状态，该状态将对断言状态进行处理。也许我的理解是错误的。

我的设计通过了断言，并且覆盖了所有内容，但是在归纳法中，它会将RCON寄存器的值设置为零，但是RCON寄存器是由$readmemh("box.mem",mem);的rcon.mem文件初始化的，如果该寄存器的初始化可以被归纳法覆盖，则证明然后如何编写将通过归纳的代码。在RTL中初始化寄存器的最佳方法是什么。

请对此提供帮助，我随附了我的mcve .sv代码，.sby配置，.mem文件和.vcd gtkwave屏幕截图。

我的错误日志文件也已附加

test_mcve_prove / logfile.txt 

SBY 21:27:37 [test_mcve_bmc] Removing directory 'test_mcve_bmc'.
SBY 21:27:39 [test_mcve_cover] Removing directory 'test_mcve_cover'.
SBY 21:27:47 [test_mcve_prove] Removing directory 'test_mcve_prove'.
SBY 21:27:47 [test_mcve_prove] Copy 'test_mcve.sv' to 'test_mcve_prove/src/test_mcve.sv'.
SBY 21:27:47 [test_mcve_prove] Copy 'rcon.mem' to 'test_mcve_prove/src/rcon.mem'.
SBY 21:27:47 [test_mcve_prove] engine_0: smtbmc
SBY 21:27:47 [test_mcve_prove] base: starting process "cd test_mcve_prove/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 21:27:47 [test_mcve_prove] base: finished (returncode=0)
SBY 21:27:47 [test_mcve_prove] smt2: starting process "cd test_mcve_prove/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 21:27:47 [test_mcve_prove] smt2: finished (returncode=0)
SBY 21:27:47 [test_mcve_prove] engine_0.basecase: starting process "cd test_mcve_prove; yosys-smtbmc --presat --unroll --noprogress -t 4  --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 21:27:47 [test_mcve_prove] engine_0.induction: starting process "cd test_mcve_prove; yosys-smtbmc --presat --unroll -i --noprogress -t 4  --append 0 --dump-vcd engine_0/trace_induct.vcd --dump-vlogtb engine_0/trace_induct_tb.v --dump-smtc engine_0/trace_induct.smtc model/design_smt2.smt2"
SBY 21:27:48 [test_mcve_prove] engine_0.basecase: ##   0:00:00  Solver: yices
SBY 21:27:48 [test_mcve_prove] engine_0.induction: ##   0:00:00  Solver: yices
SBY 21:27:48 [test_mcve_prove] engine_0.basecase: ##   0:00:00  Checking assumptions in step 0..
SBY 21:27:48 [test_mcve_prove] engine_0.basecase: ##   0:00:00  Checking assertions in step 0..
SBY 21:27:48 [test_mcve_prove] engine_0.induction: ##   0:00:00  Trying induction in step 4..
SBY 21:27:48 [test_mcve_prove] engine_0.basecase: ##   0:00:00  Checking assumptions in step 1..
SBY 21:27:48 [test_mcve_prove] engine_0.basecase: ##   0:00:00  Checking assertions in step 1..
SBY 21:27:48 [test_mcve_prove] engine_0.induction: ##   0:00:00  Trying induction in step 3..
SBY 21:27:48 [test_mcve_prove] engine_0.basecase: ##   0:00:00  Checking assumptions in step 2..
SBY 21:27:48 [test_mcve_prove] engine_0.basecase: ##   0:00:00  Checking assertions in step 2..
SBY 21:27:48 [test_mcve_prove] engine_0.induction: ##   0:00:00  Trying induction in step 2..
SBY 21:27:48 [test_mcve_prove] engine_0.induction: ##   0:00:00  Trying induction in step 1..
SBY 21:27:48 [test_mcve_prove] engine_0.basecase: ##   0:00:00  Checking assumptions in step 3..
SBY 21:27:48 [test_mcve_prove] engine_0.basecase: ##   0:00:00  Checking assertions in step 3..
SBY 21:27:48 [test_mcve_prove] engine_0.induction: ##   0:00:00  Trying induction in step 0..
SBY 21:27:48 [test_mcve_prove] engine_0.induction: ##   0:00:00  Temporal induction failed!
SBY 21:27:48 [test_mcve_prove] engine_0.induction: ##   0:00:00  Assert failed in test_mcve: test_mcve.sv:111.46-112.39
SBY 21:27:48 [test_mcve_prove] engine_0.induction: ##   0:00:00  Writing trace to VCD file: engine_0/trace_induct.vcd
SBY 21:27:48 [test_mcve_prove] engine_0.basecase: ##   0:00:00  Status: passed
SBY 21:27:48 [test_mcve_prove] engine_0.basecase: finished (returncode=0)
SBY 21:27:48 [test_mcve_prove] engine_0: Status returned by engine for basecase: pass
SBY 21:27:48 [test_mcve_prove] engine_0.induction: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_induct_tb.v
SBY 21:27:48 [test_mcve_prove] engine_0.induction: ##   0:00:00  Writing trace to constraints file: engine_0/trace_induct.smtc
SBY 21:27:48 [test_mcve_prove] engine_0.induction: ##   0:00:00  Status: failed
SBY 21:27:48 [test_mcve_prove] engine_0.induction: finished (returncode=1)
SBY 21:27:48 [test_mcve_prove] engine_0: Status returned by engine for induction: FAIL
SBY 21:27:48 [test_mcve_prove] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:01 (1)
SBY 21:27:48 [test_mcve_prove] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:01 (1)
SBY 21:27:48 [test_mcve_prove] summary: engine_0 (smtbmc) returned pass for basecase
SBY 21:27:48 [test_mcve_prove] summary: engine_0 (smtbmc) returned FAIL for induction
SBY 21:27:48 [test_mcve_prove] DONE (UNKNOWN,rc=4)

test_mcve.sv 

`default_nettype    none

module test_mcve(ext_Clk,ext_Resetn,ext_Start,ext_round,ext_next_round,xor_in_if);
//parameter for module

parameter WIDTH = 8;
parameter NUMBER_OF_ROUNDS = 10;



//external interface signals
input ext_Clk,ext_Start; //clk,reset,start
input  [3:0] ext_round;
output logic [3:0] ext_next_round;
output logic [WIDTH-1:0] xor_in_if;

//input round register
logic [3:0] round;
logic [1:0]index_sel;

//Round constant 8 bits
reg [WIDTH-1:0]RCON[(NUMBER_OF_ROUNDS-1):0] /* synthesis ram_init_file = "rcon.mif" */; 
initial begin
    $readmemh("rcon.mem",RCON);
end


//state machine states
typedef enum logic[1:0] {Idle_s,Comput_s} state_t;
state_t state,next_state;

//###################################################### state register
logic reset;
assign reset = !ext_Resetn;
always_ff@(posedge ext_Clk,posedge reset) begin
    if(reset) state <= Idle_s;
    else      state <= next_state;
end

//###################################################### next state logic
always_comb begin
    case (state)
        Idle_s: if ((ext_Start == 1)&&(ext_round == ext_next_round)&&(ext_round<NUMBER_OF_ROUNDS)&&(reset == 0)) next_state = Comput_s;
                else next_state = Idle_s;

        Comput_s: if (index_sel==3) next_state = Idle_s;
                else next_state = Comput_s;

        default: next_state = Idle_s;

    endcase
end
//####################################################### output logic



logic [WIDTH-1:0] temp_rcon;
assign xor_in_if = (index_sel == 3)?temp_rcon:0;



//next round output logic
always@(posedge ext_Clk,posedge reset)begin
    if(reset) ext_next_round<=0;
    else if(index_sel==3) ext_next_round<=ext_next_round+1;
end



//output logic
always@(posedge ext_Clk) begin
    case (state)
        Idle_s: begin
            index_sel<=0;
            if(ext_round<10)
                round <= ext_round;
            else
                round <= NUMBER_OF_ROUNDS;
        end
        Comput_s: begin
            index_sel<=index_sel+1;
            temp_rcon<=RCON[round];
        end
        default:begin
            
        end
    endcase
end

//#########################################################
//################### FORMAL VERIFICATION #################
//#########################################################
`ifdef FORMAL
  //Using Immediate assertion

  
logic verf_valid;

initial begin
    assume(verf_valid==0);
    assume(ext_Resetn == 0);
end
always @(posedge(ext_Clk))begin
    verf_valid<=1;
end

// verification
always@(posedge(ext_Clk)) begin
    if((verf_valid==1) && (ext_Resetn != 0))begin
        if((round==0)&&(index_sel == 3))begin
            assert(xor_in_if == 8'h01);
            cover(xor_in_if == 8'h01);
        end
         if((round==1)&&(index_sel == 3))begin
            assert(xor_in_if == 8'h02);
            cover(xor_in_if == 8'h02);
        end
        if((round==2)&&(index_sel == 3))begin
            assert(xor_in_if == 8'h04);
            cover(xor_in_if == 8'h04);
        end
        if((round==3)&&(index_sel == 3))begin
            assert(xor_in_if == 8'h08);
            cover(xor_in_if == 8'h08);
        end
        if((round==4)&&(index_sel == 3))begin
            assert(xor_in_if == 8'h10);
            cover(xor_in_if == 8'h10);
        end
        if((round==5)&&(index_sel == 3))begin
            assert(xor_in_if == 8'h20);
            cover(xor_in_if == 8'h20);
        end
        if((round==6)&&(index_sel == 3))begin
            assert(xor_in_if == 8'h40);
            cover(xor_in_if == 8'h40);
        end
        if((round==7)&&(index_sel == 3))begin
            assert(xor_in_if == 8'h80);
            cover(xor_in_if == 8'h80);
        end
        if((round==8)&&(index_sel == 3))begin
            assert(xor_in_if == 8'h1b);
            cover(xor_in_if == 8'h1b);
        end
        if((round==9)&&(index_sel == 3))begin
            assert(xor_in_if == 8'h36);
            cover(xor_in_if == 8'h36);
        end
          
    end
 end

`endif

endmodule

test_mcve.sby 

[tasks]
bmc d_12
cover d_120
prove d_4

[options]
bmc:mode bmc
cover:mode cover
prove:mode prove
d_120:depth 120
d_12:depth 12
d_4:depth 4

[engines]
smtbmc

[script]
read -formal -sv test_mcve.sv
prep -top test_mcve

[files]
test_mcve.sv
rcon.mem

rcon.mem 

01 02 04 08 10 
20 40 80 1B 36

trace_induct.vcd屏幕截图

enter image description here

解决方法

我正在浏览Clifford wolf的幻灯片（链接在下面），找到一张幻灯片29，他在其中演示了一个memcmp.v示例，以演示在他的.sby中使用.smtc文件对两个内存模块进行归纳证明的过程。文件。然后，我使用相同的方法初始化RCON寄存器，然后通过归纳证明（附加了.sby和.smtc文件）

我不知道使用.smtc文件初始化寄存器是否 归纳证明的良好实践。如果你们有更好的答案 请建议我。

链接到Clifford wolf's slides (Check slide-29)

我的initialize_RCON.smtc文件（我刚刚从封面目录engin0 .smtc文件中复制了前提语句，如果我们有用于内存初始化的覆盖语句并且所有Cover语句都通过，则会创建该假定语句。将其复制到assert部分） ：

async function f() {

  function delayedResponse() {
    setTimeout(function() { return 100},5000);
  }
  return await delayedResponse();

}

f().then(alert); // 100

我的test_mcve.sby 

initial
assume (= (select [RCON] #b0000) #b00000001)
assume (= (select [RCON] #b1000) #b00011011)
assume (= (select [RCON] #b0001) #b00000010)
assume (= (select [RCON] #b0010) #b00000100)
assume (= (select [RCON] #b0011) #b00001000)
assume (= (select [RCON] #b0100) #b00010000)
assume (= (select [RCON] #b0101) #b00100000)
assume (= (select [RCON] #b0110) #b01000000)
assume (= (select [RCON] #b0111) #b10000000)
assume (= (select [RCON] #b1001) #b00110110)

仅运行归纳测试，我使用证明任务，如下所示：

[tasks]
bmc d_12
cover d_120
prove d_12 smtc_prove

[options]
bmc:mode bmc
cover:mode cover
prove:mode prove
d_120:depth 120
d_12:depth 12
smtc_prove:smtc initialize_RCON.smtc

[engines]
smtbmc

[script]
read -formal -sv test_mcve.sv
prep -top test_mcve

[files]
initialize_RCON.smtc
test_mcve.sv
rcon.mem
formal-verificationfpgainductionsystem-verilogyosys

相关问答

matplotlib报错：AttributeError: module 'backend_interagg' has no attribute 'FigureCanvas'. Did you mean: 'FigureCanvasAgg'?
使用本地python环境可以成功执行 import pandas as pd impor...
gitlab登录失败，报错：This challenge page was accidentally cached by an intermediary and is no longer available.
设置时间 控制面板
后端开发常见错误
错误1：Request method ‘DELETE‘ not supported 错误还原：...
docker常见错误
错误1：启动docker镜像时报错：Error response from daemon:...
idea常见错误
错误1：private field ‘xxx‘ is never assigned 按Alt...
pip安装依赖失败
报错如下，通过源不能下载，最后警告pip需升级版本 Requirem...