From d1ddec1e4c197f17b82adb80862f5db0bc7ffcdb Mon Sep 17 00:00:00 2001 From: Marno van der Maas Date: Mon, 13 Jan 2025 13:51:02 +0000 Subject: [PATCH] Formal: Lint fixup Mostly line lengths and indexes. This commits also adds a Verible waiver file. --- .github/workflows/pr_lint.yml | 1 + dv/formal/check/peek/follower.sv | 4 +++- dv/formal/check/top.sv | 26 ++++++++++++++++-------- dv/formal/spec/spec_api.sv | 34 ++++++++++++++++---------------- lint/verible_waiver.vbw | 1 + 5 files changed, 40 insertions(+), 26 deletions(-) create mode 100644 lint/verible_waiver.vbw diff --git a/.github/workflows/pr_lint.yml b/.github/workflows/pr_lint.yml index 91eeb1e497..e7c107a02f 100644 --- a/.github/workflows/pr_lint.yml +++ b/.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" diff --git a/dv/formal/check/peek/follower.sv b/dv/formal/check/peek/follower.sv index ff40c27d3f..85ad311bec 100644 --- a/dv/formal/check/peek/follower.sv +++ b/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 diff --git a/dv/formal/check/top.sv b/dv/formal/check/top.sv index 07253d6719..f391a42553 100644 --- a/dv/formal/check/top.sv +++ b/dv/formal/check/top.sv @@ -124,7 +124,10 @@ 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 +172,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 +265,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 +290,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 +331,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 +392,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 ////////////////////// diff --git a/dv/formal/spec/spec_api.sv b/dv/formal/spec/spec_api.sv index 3d24a0dfcd..ca2fcafe37 100644 --- a/dv/formal/spec/spec_api.sv +++ b/dv/formal/spec/spec_api.sv @@ -99,9 +99,9 @@ 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; @@ -109,17 +109,17 @@ 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]}; diff --git a/lint/verible_waiver.vbw b/lint/verible_waiver.vbw new file mode 100644 index 0000000000..cb8644e2cb --- /dev/null +++ b/lint/verible_waiver.vbw @@ -0,0 +1 @@ +waive --rule=module-port --location="spec_instance.sv"