Formal: Lint fixup

Mostly line lengths and indexes.
This commits also adds a Verible waiver file.

.github/workflows/pr_lint.yml

@@ -36,3 +36,4 @@ jobs:
           reviewdog_reporter: github-pr-check
           suggest_fixes: "false"
           config_file: ${{ env.verible_config }}
+          extra_args: "--waiver_files lint/verible_waiver.vbw"

dv/formal/check/peek/follower.sv

@@ -49,7 +49,9 @@ always_comb begin
         ex_has_branched_d = ex_has_branched_q;
     end
 
-    ex_has_branched_d = (ex_has_branched_d | `IF.branch_req) && ~ex_kill && (`IDC.ctrl_fsm_cs == `IDC.DECODE);
+    ex_has_branched_d = (ex_has_branched_d | `IF.branch_req) &&
+                        ~ex_kill &&
+                        (`IDC.ctrl_fsm_cs == `IDC.DECODE);
 end
 
 always @(posedge clk_i or negedge rst_ni) begin

dv/formal/check/top.sv

@@ -124,7 +124,11 @@ ConstantBoot: assume property (boot_addr_i == $past(boot_addr_i));
 // 3. Always fetch enable
 FetchEnable: assume property (fetch_enable_i == IbexMuBiOn);
 // 4. Never try to sleep if we couldn't ever wake up
-WFIStart: assume property (`IDC.ctrl_fsm_cs == SLEEP |-> `CSR.mie_q.irq_software | `CSR.mie_q.irq_timer | `CSR.mie_q.irq_external);
+WFIStart: assume property (`IDC.ctrl_fsm_cs == SLEEP |-> (
+                                                          `CSR.mie_q.irq_software |
+                                                          `CSR.mie_q.irq_timer |
+                                                          `CSR.mie_q.irq_external
+                                                         ));
 // 5. Disable clock gating
 TestEn: assume property (test_en_i);
 // See protocol/* for further assumptions
@@ -169,7 +173,7 @@ TestEn: assume property (test_en_i);
 ////////////////////// Abstract State //////////////////////
 
 // Pre state is the architectural state of Ibex at the start of the cycle
-logic [31:0] pre_regs[31:0];
+logic [31:0] pre_regs[32];
 logic [31:0] pre_nextpc;
 logic [31:0] pre_mip;
 
@@ -262,10 +266,11 @@ assign lsu_had_first_resp = `LSU.ls_fsm_cs == `LSU.WAIT_GNT && `LSU.split_misali
 ////////////////////// Wrap signals //////////////////////
 
 logic spec_en; // The specification is being queried in this cycle
-logic has_spec_past; // There is a previous step to compare against. Will become 0 on uncheckable CSRs and at reset.
+logic has_spec_past; // There is a previous step to compare against.
+                     // Will become 0 on uncheckable CSRs and at reset.
 
 // The previous specification output to be compared with the new input
-logic [31:0] spec_past_regs[31:0];
+logic [31:0] spec_past_regs[32];
 logic [31:0] spec_past_has_reg; // Registers will have past values only when they are written to.
 `define X(n) spec_past_``n
 `X_EACH_CSR_TYPED
@@ -286,7 +291,8 @@ logic wbexc_illegal; // EXC has an illegal instruction
 logic wbexc_compressed_illegal; // EXC has an illegal instruction
 logic wbexc_err; // EXC has an error
 logic instr_will_progress; // Instruction will finish EX
-logic wfi_will_finish; // WFI instruction retire by flushing the pipeline, but that isn't an exception
+logic wfi_will_finish; // WFI instruction retire by flushing the pipeline,
+                       // but that isn't an exception.
 logic wbexc_csr_pipe_flush; // The pipeline is being flushed due to a CSR write
 logic wbexc_handling_irq; // Check the results of handling an IRQ
 
@@ -326,7 +332,8 @@ logic spec_post_wX_en;
 
 logic spec_int_err;
 
-logic spec_fetch_err; // The specification has experienced a fetch error, regardless of whether or not it was told to.
+logic spec_fetch_err; // The specification has experienced a fetch error,
+                      // regardless of whether or not it was told to.
 assign spec_fetch_err =
     (main_mode == MAIN_IFERR && spec_api_i.main_result == MAINRES_OK) ||
     spec_api_i.main_result == MAINRES_IFERR_1 || spec_api_i.main_result == MAINRES_IFERR_2;
@@ -386,10 +393,14 @@ assign lsu_waiting_for_misal =
       ((`LSU.data_type_q == 2'b01) && (`LSU.rdata_offset_q == 2'b11));
 
 logic addr_last_matches;
-assign addr_last_matches = `ID.rf_rdata_a_fwd + (ex_is_store_instr? `ID.imm_s_type : `ID.imm_i_type) == `LSU.addr_last_q;
+assign addr_last_matches = `ID.rf_rdata_a_fwd +
+                           (ex_is_store_instr? `ID.imm_s_type : `ID.imm_i_type) ==
+                           `LSU.addr_last_q;
 
 logic addr_last_d_matches;
-assign addr_last_d_matches = `ID.rf_rdata_a_fwd + (ex_is_store_instr? `ID.imm_s_type : `ID.imm_i_type) == `LSU.addr_last_d;
+assign addr_last_d_matches = `ID.rf_rdata_a_fwd +
+                             (ex_is_store_instr? `ID.imm_s_type : `ID.imm_i_type) ==
+                             `LSU.addr_last_d;
 
 ////////////////////// Compare //////////////////////
 

dv/formal/spec/spec_api.sv

@@ -99,27 +99,27 @@ module spec_api #(
     output logic [3:0] mem_write_snd_be_o
 );
 
-bit rX_sail_invoke[1:0];
-logic [31:0] rX_sail_invoke_ret[1:0];
-logic [63:0] rX_sail_invoke_arg_0[1:0];
+bit rX_sail_invoke[2];
+logic [31:0] rX_sail_invoke_ret[2];
+logic [63:0] rX_sail_invoke_arg_0[2];
 assign rx_a_en_o = rX_sail_invoke[0];
 assign rx_a_addr_o = rX_sail_invoke_arg_0[0][4:0];
 assign rX_sail_invoke_ret[0] = rx_a_i;
 assign rx_b_en_o = rX_sail_invoke[1];
 assign rx_b_addr_o = rX_sail_invoke_arg_0[1][4:0];
 assign rX_sail_invoke_ret[1] = rx_b_i;
 
-logic wX_sail_invoke[0:0];
-logic [63:0] wX_sail_invoke_arg_0[0:0];
-logic [31:0] wX_sail_invoke_arg_1[0:0];
+logic wX_sail_invoke[1];
+logic [63:0] wX_sail_invoke_arg_0[1];
+logic [31:0] wX_sail_invoke_arg_1[1];
 assign wx_en_o = wX_sail_invoke[0];
 assign wx_addr_o = wX_sail_invoke_arg_0[0][4:0];
 assign wx_o = wX_sail_invoke_arg_1[0];
 
-logic write_ram_sail_invoke[1:0];
-logic [31:0] write_ram_sail_invoke_arg_1[1:0];
-logic [31:0] write_ram_sail_invoke_arg_2[1:0];
-logic [3:0] write_ram_sail_invoke_arg_3[1:0];
+logic write_ram_sail_invoke[2];
+logic [31:0] write_ram_sail_invoke_arg_1[2];
+logic [31:0] write_ram_sail_invoke_arg_2[2];
+logic [3:0] write_ram_sail_invoke_arg_3[2];
 assign mem_write_o = write_ram_sail_invoke[0];
 assign mem_write_snd_gran_o = write_ram_sail_invoke[1];
 assign mem_write_fst_addr_o = write_ram_sail_invoke_arg_1[0];
@@ -129,9 +129,9 @@ assign mem_write_snd_wdata_o = write_ram_sail_invoke_arg_2[1];
 assign mem_write_fst_be_o = write_ram_sail_invoke_arg_3[0];
 assign mem_write_snd_be_o = write_ram_sail_invoke_arg_3[1];
 
-logic read_ram_sail_invoke[1:0];
-logic [31:0] read_ram_sail_invoke_ret[1:0];
-logic [31:0] read_ram_sail_invoke_arg_1[1:0];
+logic read_ram_sail_invoke[2];
+logic [31:0] read_ram_sail_invoke_ret[2];
+logic [31:0] read_ram_sail_invoke_arg_1[2];
 assign mem_read_o = read_ram_sail_invoke[0];
 assign mem_read_snd_gran_o = read_ram_sail_invoke[1];
 assign mem_read_fst_addr_o = read_ram_sail_invoke_arg_1[0];
@@ -160,10 +160,10 @@ assign mcounteren_o = mcounteren_out.bits;
 t_Mtvec mtvec_out;
 assign mtvec_o = mtvec_out.bits;
 
-t_Pmpcfg_ent pmpcfg_n_in[63:0];
-logic [31:0] pmpaddr_n_in[63:0];
-t_Pmpcfg_ent pmpcfg_n_out[63:0];
-logic [31:0] pmpaddr_n_out[63:0];
+t_Pmpcfg_ent pmpcfg_n_in[64];
+logic [31:0] pmpaddr_n_in[64];
+t_Pmpcfg_ent pmpcfg_n_out[64];
+logic [31:0] pmpaddr_n_out[64];
 for (genvar i = 0; i < 64; i++) begin: g_pmp_bind
     if (i < PMPNumRegions) begin: g_pmp_bind_real
         assign pmpcfg_n_in[i] = '{bits: pmp_cfg_i[i]};

lint/verible_waiver.vbw

@@ -0,0 +1 @@
+waive --rule=module-port --location="spec_instance.sv"