I am very new to formal verification and I started my formal verification with SymbiYosys. I had written some code in System Verilog for learning formal verification, I was able to pass BMC and cover for the code but it is failing (UNKNOWN sate) for induction.
I don't have much understanding of formal proving but my current understanding of induction proving is: my design will start in the future time in the assertion sate and all my register will be set in some state that would have triggered my assertion and from that state SymbiYosys engine will try to find a valid state in the reverse timestep which would have made to the assertion sate. Maybe my understanding is wrong.
My design passes assertions and also covers but in induction it sets the values RCON registers to zero but RCON registers are initialized by rcon.mem file using $readmemh("box.mem",mem); then if this register initialization can be overridden by in induction prove then how do I write my code that will pass induction. What is the best method to initalize a register in RTL.
Please Help on this, I have my mcve .sv code, .sby configuration, .mem file and .vcd gtkwave screenshot attached.
my error logfile is also attached
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 screenshot
I was going through the slides from Clifford wolf(link is below), and found a slide-29 where he had illustrated an example memcmp.v to demonstrate induction proving for two memmory modules by using .smtc file in his .sby file. Then I used the same method to initialize my RCON register, then my induction proving passed(my .sby and .smtc files are attached)
Link to Clifford wolf's slides (Check slide-29)
My initialize_RCON.smtc file (I had just copied the assume statements from cover directory engin0 .smtc file, which will be created if we had covered statements for memory initialization and all the cover statement passes. Same is copied to assert section):
My test_mcve.sby
To run induction test only, I use prove task as shown below: