Я новичок в формальной верификации и начал формальную верификацию с SymbiYosys. Я написал некоторый код в System Verilog для изучения формальной проверки, я смог пройти BMC и прикрыть код, но он не работает (НЕИЗВЕСТНО) для индукции.
У меня нет большого понимания формального доказательства, но мое текущее понимание индукционного доказательства таково: мой проект начнется в будущем в состоянии утверждения, и все мои регистры будут установлены в каком-то состоянии, которое вызвало бы мое утверждение, и из этого state Движок SymbiYosys попытается найти допустимое состояние в обратном временном шаге, который бы соответствовал состоянию утверждения. Может быть, мое понимание неправильно.
Мой дизайн передает утверждения, а также охватывает, но в индукции он устанавливает значения регистров RCON в ноль, но регистры RCON инициализируются файлом rcon.mem с использованием $readmemh("box.mem",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_Resetn,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 
