Refine fazyrv_pc formal checks

Author: meiniKi

fv/pc/fazyrv_pc_bmc.sby

@@ -1,7 +1,7 @@
 
 [options]
 mode bmc
-depth 80
+depth 200
 
 [engines]
 smtbmc z3

fv/pc/fazyrv_pc_cov.sby

@@ -1,7 +1,7 @@
 
 [options]
 mode cover
-depth 80
+depth 200
 
 [engines]
 smtbmc z3

fv/pc/fazyrv_pc_fv.sv

@@ -63,9 +63,14 @@ end
 
 // Remember shifted in data
 //
-logic [31:0] fv_din = 'b0;
+logic [31:0] fv_din = 2'b11;
 always_ff @(posedge clk_i) fv_din <= {din, fv_din[31:CHUNKSIZE]};
 
+// We can safely assume the PC does not overflow
+always_ff @(posedge clk_i) begin
+  if (fv_cycle_check) assume (fv_din != 32'hFFFF_FFFF);
+end
+
 logic [31:0] fv_pcinc = 'b0;
 always_ff @(posedge clk_i) fv_pcinc <= {pc_ser_inc, fv_pcinc[31:CHUNKSIZE]};
 
@@ -85,7 +90,7 @@ fazyrv_pc #(
   .rst_in        ( rst_in             ),
   // Continuous inc to strobe; handle here for simplicity
   .inc_i         ( inc & fv_cycle_lsb & fv_pc_op ),
-  .shift_i       ( shift  & fv_pc_op  ),
+  .shift_i       ( shift & fv_pc_op   ),
   .din_i         ( din                ),
   .pc_ser_o      ( pc_ser             ), 
   .pc_ser_inc_o  ( pc_ser_inc         ),
@@ -101,8 +106,6 @@ always_comb begin
   if (inc) assume(shift);
   // Assume normal pc increment
   if (inc) assume(din == pc_ser_inc);
-  // Loading PC, assume data != 0 for easier debugging
-  if (shift & ~inc) assume(din != 'b0);
 end
 
 
@@ -152,18 +155,22 @@ end
 
 always_ff @(posedge clk_i) begin
   cover (rst_in);
-  cover (rst_in & (pc == BOOTADR));
-  cover (fv_cycle_check);
-  cover (fv_cycle_check && $past(inc));
-  cover (fv_cycle_check && $past(shift));
-  cover (fv_cycle_check & (~inc & ~shift));
-  cover (fv_cycle_check & (inc != $past(inc)));
-
+  cover (rst_in && (pc == BOOTADR));
+  cover (rst_in && fv_cycle_check);
+  cover (rst_in && fv_cycle_check && $past(inc));
+  cover (rst_in && fv_cycle_check && $past(shift));
+
+  cover (rst_in && fv_cycle_check & (inc != $past(inc)));
+  cover (rst_in && fv_cycle_check && (fv_pcinc == 32'h0000_00F3) && $past(inc));
+  cover (rst_in && fv_cycle_check && (fv_pcinc == 32'h0000_FF03) && $past(inc));
+  cover (rst_in && fv_cycle_check && (fv_pcinc == 32'hFFFF_FFF3) && $past(inc));
+  cover (rst_in && fv_cycle_check && (fv_pcinc == 32'h0000_FF03) && $past(inc));
+  cover (rst_in && fv_cycle_check && (fv_pcinc == 32'hFFFF_FFF3) && $past(inc));
   //
-  cover ($past(shift) & $past(inc) & (pc == fv_prev_pc + 'd4));
-  cover ($past(shift) & $past(inc) & (pc == fv_pcinc));
-  cover ($past(shift) & (pc == fv_din));
-  cover ($past(shift) & (fv_prev_pc == fv_pcser));
+  cover (rst_in && fv_cycle_check && $past(shift) && $past(inc) && (pc == fv_prev_pc + 'd4));
+  cover (rst_in && fv_cycle_check && $past(shift) && $past(inc) && (pc == fv_pcinc));
+  cover (rst_in && fv_cycle_check && $past(shift) && (pc == fv_din));
+  cover (rst_in && fv_cycle_check && $past(shift) && (fv_prev_pc == fv_pcser));
 end
 
 endmodule

rtl/fazyrv_pc.sv

@@ -1,4 +1,4 @@
-// Copyright (c) 2023 - 2024 Meinhard Kissich
+// Copyright (c) 2023 - 2025 Meinhard Kissich
 // SPDX-License-Identifier: MIT
 // -----------------------------------------------------------------------------
 // File  :  fazyrv_pc.sv
@@ -11,7 +11,7 @@
 // Ports
 //  - clk_i         Clock input, sensitive to rising edge.
 //  - rst_in        Reset, low active.
-//  - inc_i         Strobe to increment PC in the subsequent cylce.
+//  - inc_i         Strobe to increment PC in the subsequent cycle.
 //  - shift_i       Shift PC register.
 //  - din_i         New input data part when PC is shifted.
 //  - pc_ser_o      Serial output part of PC register.
@@ -31,11 +31,9 @@ module fazyrv_pc #( parameter CHUNKSIZE=2, parameter BOOTADR=32'hFFFF )
   output logic [31:0]           pc_o
 );
 
-// restrictions: pc currenctly must be %4
-// otherwise opt with carry does not work
 
 logic [31:0] pc_r, pc_n;
-logic [CHUNKSIZE-1:0]  pc_inc;
+logic [CHUNKSIZE-1:0] pc_inc;
 
 assign pc_o         = pc_r;
 assign pc_ser_o     = pc_r[CHUNKSIZE-1:0];
@@ -87,7 +85,7 @@ generate
     end else begin
       assign b = carry_vec[i];
     end
-    //             a,     b,   y,         c
+    //                    a,     b,   y,         c
     fazyrv_hadd i_hadd (pc_r[i], b, pc_inc[i], carry_vec[i+1]);
   end
 endgenerate