feat: replace ribp interface with apb4 interface across multiple formal modules and update related file lists

rtl/mini/formal/bus_formal.sv

@@ -31,6 +31,7 @@ module bus_formal_design (
 );
 
   ribp_if mgmt_ribp ();
+  rib_if mgmt_rib ();
   rib_if user_rib ();
   rib_if dma_rib ();
   rib_if rib ();
@@ -188,10 +189,17 @@ module bus_formal_design (
   assign rib_cmd_len    = rib.cmd_len;
   assign apb_valid      = apb_rib.cmd_valid;
 
+  ribp2rib u_mgmt_ribp2rib (
+      .clk_i  (clk_i),
+      .rst_n_i(rst_n_i),
+      .ribp   (mgmt_ribp),
+      .rib    (mgmt_rib)
+  );
+
   rib_bus u_dut (
       .clk_i            (clk_i),
       .rst_n_i          (rst_n_i),
-      .mgmt_ribp        (mgmt_ribp),
+      .mgmt_rib         (mgmt_rib),
       .user_rib         (user_rib),
       .dma_rib          (dma_rib),
       .user_bus_enable_i(1'b1),
@@ -210,7 +218,7 @@ module bus_formal_design (
       .perf_mgmt_wait_o (),
       .perf_user_wait_o (),
       .perf_dma_wait_o  (),
-      .perf_ribp_wait_o (),
+      .perf_apb4_wait_o (),
       .perf_apb_wait_o  (),
       .perf_sdram_wait_o(),
       .perf_psram_wait_o(),

rtl/mini/formal/clint_formal.sv

@@ -22,11 +22,14 @@ module clint_formal_design (
     // verilog_format: on
 );
 
-  ribp_if ribp ();
+  apb4_if apb4 (
-  (* anyseq *)logic        f_rib_valid;
+      .pclk   (clk_i),
-  (* anyseq *)logic [31:0] f_rib_addr;
+      .presetn(rst_n_i)
-  (* anyseq *)logic [31:0] f_rib_wdata;
+  );
-  (* anyseq *)logic [ 3:0] f_rib_wstrb;
+  (* anyseq *)logic        f_apb_sel;
+  (* anyseq *)logic [31:0] f_apb_addr;
+  (* anyseq *)logic [31:0] f_apb_wdata;
+  (* anyseq *)logic [ 3:0] f_apb_pstrb;
   (* anyseq *)logic        f_tick;
   logic        s_mtime_load;
   logic [63:0] s_mtime_load_value;
@@ -35,17 +38,20 @@ module clint_formal_design (
   logic [63:0] s_mtimecmp         [0:1];
   logic [ 1:0] s_timer_irq;
 
-  assign ribp.valid        = f_rib_valid;
+  assign apb4.psel         = f_apb_sel;
-  assign ribp.addr         = f_rib_addr;
+  assign apb4.penable      = f_apb_sel;
-  assign ribp.wdata        = f_rib_wdata;
+  assign apb4.pwrite       = |f_apb_pstrb;
-  assign ribp.wstrb        = f_rib_wstrb;
+  assign apb4.paddr        = f_apb_addr;
+  assign apb4.pwdata       = f_apb_wdata;
+  assign apb4.pstrb        = f_apb_pstrb;
+  assign apb4.pprot        = 3'b000;
 
-  assign rib_valid         = ribp.valid;
+  assign rib_valid         = apb4.psel;
-  assign rib_addr          = ribp.addr;
+  assign rib_addr          = apb4.paddr;
-  assign rib_wdata         = ribp.wdata;
+  assign rib_wdata         = apb4.pwdata;
-  assign rib_wstrb         = ribp.wstrb;
+  assign rib_wstrb         = apb4.pstrb;
-  assign rib_ready         = ribp.ready;
+  assign rib_ready         = apb4.pready;
-  assign rib_resp_err      = ribp.resp_err;
+  assign rib_resp_err      = apb4.pslverr;
   assign tick              = f_tick;
   assign mtime             = s_mtime;
   assign mtime_load        = s_mtime_load;
@@ -60,7 +66,7 @@ module clint_formal_design (
   ) u_clint_reg (
       .clk_i             (clk_i),
       .rst_n_i           (rst_n_i),
-      .ribp              (ribp),
+      .apb4              (apb4),
       .mtime_i           (s_mtime),
       .mtime_load_o      (s_mtime_load),
       .mtime_load_value_o(s_mtime_load_value),

rtl/mini/formal/dvp_formal.sv

@@ -15,30 +15,36 @@ module dvp_formal_design (
     output logic [ 6:0] intr_enable,
     output logic        irq
 );
-  ribp_if rib ();
+  apb4_if apb4 (
-  (* anyseq *) logic f_rib_valid;
+      .pclk   (clk_i),
-  (* anyseq *) logic [31:0] f_rib_addr, f_rib_wdata;
+      .presetn(rst_n_i)
-  (* anyseq *) logic [3:0] f_rib_wstrb;
+  );
+  (* anyseq *) logic f_apb_sel;
+  (* anyseq *) logic [31:0] f_apb_addr, f_apb_wdata;
+  (* anyseq *) logic [3:0] f_apb_pstrb;
   (* anyseq *) logic f_active, f_fifo_empty, f_fifo_full;
   (* anyseq *)logic [  5:0] f_error_flags;
   (* anyseq *)logic [127:0] f_frame_stats;
   (* anyseq *)logic         f_frame_stats_valid;
-  assign rib.valid    = f_rib_valid;
+  assign apb4.psel    = f_apb_sel;
-  assign rib.addr     = f_rib_addr;
+  assign apb4.penable = f_apb_sel;
-  assign rib.wdata    = f_rib_wdata;
+  assign apb4.pwrite  = |f_apb_pstrb;
-  assign rib.wstrb    = f_rib_wstrb;
+  assign apb4.paddr   = f_apb_addr;
-  assign rib_valid    = rib.valid;
+  assign apb4.pwdata  = f_apb_wdata;
-  assign rib_addr     = rib.addr;
+  assign apb4.pstrb   = f_apb_pstrb;
-  assign rib_wdata    = rib.wdata;
+  assign apb4.pprot   = 3'b000;
-  assign rib_wstrb    = rib.wstrb;
+  assign rib_valid    = apb4.psel;
-  assign rib_ready    = rib.ready;
+  assign rib_addr     = apb4.paddr;
-  assign rib_resp_err = rib.resp_err;
+  assign rib_wdata    = apb4.pwdata;
+  assign rib_wstrb    = apb4.pstrb;
+  assign rib_ready    = apb4.pready;
+  assign rib_resp_err = apb4.pslverr;
   assign intr_state   = u_dut.s_intr_stat_q;
   assign intr_enable  = u_dut.s_intr_en_q;
   dvp_reg u_dut (
       .clk_i              (clk_i),
       .rst_n_i            (rst_n_i),
-      .ribp               (rib),
+      .apb4               (apb4),
       .active_i           (f_active),
       .fifo_empty_i       (f_fifo_empty),
       .fifo_full_i        (f_fifo_full),

rtl/mini/formal/generate_formal_filelist.py

@@ -31,6 +31,7 @@ def target_defines(target: str) -> list[str]:
 def source_files(target: str) -> list[Path]:
     common = [
         COMMON_RTL / "interface/axi4_if.sv",
+        COMMON_RTL / "interface/apb4_if.sv",
         COMMON_RTL / "interface/ribp_if.sv",
         COMMON_RTL / "interface/ram_if.sv",
         COMMON_RTL / "utils/register.sv",
@@ -106,7 +107,7 @@ def source_files(target: str) -> list[Path]:
         ]
     if target == "ws2812":
         return [
-            COMMON_RTL / "interface/ribp_if.sv",
+            COMMON_RTL / "interface/apb4_if.sv",
             COMMON_RTL / "utils/register.sv",
             COMMON_RTL / "utils/fifo.sv",
             SERIAL / "ws2812_if.sv",
@@ -117,7 +118,7 @@ def source_files(target: str) -> list[Path]:
         ]
     if target == "uart":
         return [
-            COMMON_RTL / "interface/ribp_if.sv",
+            COMMON_RTL / "interface/apb4_if.sv",
             COMMON_RTL / "cdc/cdc_sync.sv",
             COMMON_RTL / "utils/register.sv",
             COMMON_RTL / "utils/edge_det.sv",
@@ -134,7 +135,7 @@ def source_files(target: str) -> list[Path]:
         ]
     if target == "i2c":
         return [
-            COMMON_RTL / "interface/ribp_if.sv",
+            COMMON_RTL / "interface/apb4_if.sv",
             COMMON_RTL / "utils/register.sv",
             COMMON_RTL / "utils/fifo.sv",
             COMMON_RTL / "cdc/cdc_sync.sv",
@@ -147,7 +148,7 @@ def source_files(target: str) -> list[Path]:
         ]
     if target == "timer":
         return [
-            COMMON_RTL / "interface/ribp_if.sv",
+            COMMON_RTL / "interface/apb4_if.sv",
             COMMON_RTL / "utils/register.sv",
             COMMON_RTL / "clkrst/counter.sv",
             PERIPHERAL / "timer_core.sv",
@@ -157,7 +158,7 @@ def source_files(target: str) -> list[Path]:
         ]
     if target == "clint":
         return [
-            COMMON_RTL / "interface/ribp_if.sv",
+            COMMON_RTL / "interface/apb4_if.sv",
             COMMON_RTL / "utils/register.sv",
             COMMON_RTL / "clkrst/counter.sv",
             PERIPHERAL / "clint_if.sv",
@@ -168,7 +169,8 @@ def source_files(target: str) -> list[Path]:
         ]
     if target == "dvp":
         return [
-            COMMON_RTL / "interface/ribp_if.sv", COMMON_RTL / "utils/register.sv",
+            COMMON_RTL / "interface/apb4_if.sv",
+            COMMON_RTL / "utils/register.sv",
             ROOT / "rtl/ip/multimedia/dvp_define.svh",
             ROOT / "rtl/ip/multimedia/dvp_reg.sv",
             SCRIPT_DIR / "dvp_formal.sv",

rtl/mini/formal/gpio_formal.sv

@@ -30,14 +30,17 @@ module gpio_formal_design (
     // verilog_format: on
 );
 
-  ribp_if ribp ();
+  apb4_if apb4 (
+      .pclk   (clk_i),
+      .presetn(rst_n_i)
+  );
   gpio_if #(4) gpio ();
   user_gpio_if #(4) user_gpio ();
 
-  (* anyseq *)logic        f_ribp_valid;
+  (* anyseq *)logic        f_apb_sel;
-  (* anyseq *)logic [31:0] f_ribp_addr;
+  (* anyseq *)logic [31:0] f_apb_addr;
-  (* anyseq *)logic [31:0] f_ribp_wdata;
+  (* anyseq *)logic [31:0] f_apb_wdata;
-  (* anyseq *)logic [ 3:0] f_ribp_wstrb;
+  (* anyseq *)logic [ 3:0] f_apb_pstrb;
   (* anyseq *)logic [ 3:0] f_gpio_di;
   (* anyseq *)logic [ 3:0] f_alt0_do;
   (* anyseq *)logic [ 3:0] f_alt0_oe;
@@ -46,10 +49,13 @@ module gpio_formal_design (
   (* anyseq *)logic [ 3:0] f_user_do;
   (* anyseq *)logic [ 3:0] f_user_oe;
 
-  assign ribp.valid     = f_ribp_valid;
+  assign apb4.psel      = f_apb_sel;
-  assign ribp.addr      = f_ribp_addr;
+  assign apb4.penable   = f_apb_sel;
-  assign ribp.wdata     = f_ribp_wdata;
+  assign apb4.pwrite    = |f_apb_pstrb;
-  assign ribp.wstrb     = f_ribp_wstrb;
+  assign apb4.paddr     = f_apb_addr;
+  assign apb4.pwdata    = f_apb_wdata;
+  assign apb4.pstrb     = f_apb_pstrb;
+  assign apb4.pprot     = 3'b000;
   assign gpio.di_i      = f_gpio_di;
   assign gpio.alt0_do_i = f_alt0_do;
   assign gpio.alt0_oe_i = f_alt0_oe;
@@ -58,12 +64,12 @@ module gpio_formal_design (
   assign user_gpio.do_o = f_user_do;
   assign user_gpio.oe_o = f_user_oe;
 
-  assign ribp_valid     = ribp.valid;
+  assign ribp_valid     = apb4.psel;
-  assign ribp_ready     = ribp.ready;
+  assign ribp_ready     = apb4.pready;
-  assign ribp_resp_err  = ribp.resp_err;
+  assign ribp_resp_err  = apb4.pslverr;
-  assign ribp_addr      = ribp.addr;
+  assign ribp_addr      = apb4.paddr;
-  assign ribp_wdata     = ribp.wdata;
+  assign ribp_wdata     = apb4.pwdata;
-  assign ribp_wstrb     = ribp.wstrb;
+  assign ribp_wstrb     = apb4.pstrb;
   assign gpio_oe        = gpio.oe_o;
   assign gpio_do        = gpio.do_o;
   assign user_oe        = user_gpio.oe_o;
@@ -80,7 +86,7 @@ module gpio_formal_design (
   assign intr_state     = u_dut.u_gpio_reg.s_intr_state_q;
   assign irq            = gpio.irq_o;
 
-  ribp_gpio #(
+  apb4_gpio #(
       .PinNum       (4),
       .UserBaseAddr (32'h1000_0000),
       .AdminBaseAddr(32'h1001_4000),
@@ -90,7 +96,7 @@ module gpio_formal_design (
   ) u_dut (
       .clk_i    (clk_i),
       .rst_n_i  (rst_n_i),
-      .ribp     (ribp),
+      .apb4     (apb4),
       .gpio     (gpio),
       .user_gpio(user_gpio)
   );

rtl/mini/formal/i2c_formal.sv

@@ -33,29 +33,35 @@ module i2c_formal_design (
     // verilog_format: on
 );
 
-  ribp_if ribp ();
+  apb4_if apb4 (
+      .pclk   (clk_i),
+      .presetn(rst_n_i)
+  );
   i2c_if i2c ();
 
-  (* anyseq *)logic        f_rib_valid;
+  (* anyseq *)logic        f_apb_sel;
-  (* anyseq *)logic [31:0] f_rib_addr;
+  (* anyseq *)logic [31:0] f_apb_addr;
-  (* anyseq *)logic [31:0] f_rib_wdata;
+  (* anyseq *)logic [31:0] f_apb_wdata;
-  (* anyseq *)logic [ 3:0] f_rib_wstrb;
+  (* anyseq *)logic [ 3:0] f_apb_pstrb;
   (* anyseq *)logic        f_scl;
   (* anyseq *)logic        f_sda;
 
-  assign ribp.valid      = f_rib_valid;
+  assign apb4.psel       = f_apb_sel;
-  assign ribp.addr       = f_rib_addr;
+  assign apb4.penable    = f_apb_sel;
-  assign ribp.wdata      = f_rib_wdata;
+  assign apb4.pwrite     = |f_apb_pstrb;
-  assign ribp.wstrb      = f_rib_wstrb;
+  assign apb4.paddr      = f_apb_addr;
+  assign apb4.pwdata     = f_apb_wdata;
+  assign apb4.pstrb      = f_apb_pstrb;
+  assign apb4.pprot      = 3'b000;
   assign i2c.scl_i       = f_scl;
   assign i2c.sda_i       = f_sda;
 
-  assign rib_valid       = ribp.valid;
+  assign rib_valid       = apb4.psel;
-  assign rib_addr        = ribp.addr;
+  assign rib_addr        = apb4.paddr;
-  assign rib_wdata       = ribp.wdata;
+  assign rib_wdata       = apb4.pwdata;
-  assign rib_wstrb       = ribp.wstrb;
+  assign rib_wstrb       = apb4.pstrb;
-  assign rib_ready       = ribp.ready;
+  assign rib_ready       = apb4.pready;
-  assign rib_resp_err    = ribp.resp_err;
+  assign rib_resp_err    = apb4.pslverr;
   assign command_count   = u_dut.u_i2c_reg.s_cmd_count;
   assign rx_count        = u_dut.u_i2c_reg.s_rx_count;
   assign error_status    = u_dut.u_i2c_reg.s_err_stat_q;
@@ -73,12 +79,12 @@ module i2c_formal_design (
   assign sda_oe          = i2c.sda_oe_o;
   assign irq             = i2c.irq_o;
 
-  ribp_i2c u_dut (
+  apb4_i2c u_dut (
       .clk_i         (clk_i),
       .rst_n_i       (rst_n_i),
       .dma_tx_stall_o(tx_dma_stall),
       .dma_rx_stall_o(rx_dma_stall),
-      .ribp          (ribp),
+      .apb4          (apb4),
       .i2c           (i2c)
   );
 

rtl/mini/formal/sysctrl_formal.sv

@@ -38,14 +38,17 @@ module sysctrl_formal_design (
     output logic [ 7:0] test_code
 );
 
-  ribp_if rib ();
+  apb4_if apb4 (
+      .pclk   (clk_i),
+      .presetn(rst_n_i)
+  );
   sysctrl_if sysctrl ();
   pll_ctrl_if pll_ctrl ();
 
-  (* anyseq *)logic        f_rib_valid;
+  (* anyseq *)logic        f_apb_sel;
-  (* anyseq *)logic [31:0] f_rib_addr;
+  (* anyseq *)logic [31:0] f_apb_addr;
-  (* anyseq *)logic [31:0] f_rib_wdata;
+  (* anyseq *)logic [31:0] f_apb_wdata;
-  (* anyseq *)logic [ 3:0] f_rib_wstrb;
+  (* anyseq *)logic [ 3:0] f_apb_pstrb;
   (* anyseq *)logic        f_pll_req_ready;
   (* anyseq *)logic [ 2:0] f_pll_active_sel;
   (* anyseq *)logic        f_pll_active_valid;
@@ -59,10 +62,13 @@ module sysctrl_formal_design (
   (* anyseq *)logic [ 3:0] f_fault_wstrb;
   (* anyseq *)logic        f_fault_reserved;
 
-  assign rib.valid = f_rib_valid;
+  assign apb4.psel = f_apb_sel;
-  assign rib.addr = f_rib_addr;
+  assign apb4.penable = f_apb_sel;
-  assign rib.wdata = f_rib_wdata;
+  assign apb4.pwrite = |f_apb_pstrb;
-  assign rib.wstrb = f_rib_wstrb;
+  assign apb4.paddr = f_apb_addr;
+  assign apb4.pwdata = f_apb_wdata;
+  assign apb4.pstrb = f_apb_pstrb;
+  assign apb4.pprot = 3'b000;
   assign sysctrl.user_bus_idle_i = 1'b1;
   assign sysctrl.fault_access_i = 1'b0;
   assign sysctrl.fault_master_i = '0;
@@ -70,7 +76,7 @@ module sysctrl_formal_design (
   assign sysctrl.perf_mgmt_wait_i = '0;
   assign sysctrl.perf_user_wait_i = '0;
   assign sysctrl.perf_dma_wait_i = '0;
-  assign sysctrl.perf_ribp_wait_i = '0;
+  assign sysctrl.perf_apb4_wait_i = '0;
   assign sysctrl.perf_apb_wait_i = '0;
   assign sysctrl.perf_sdram_wait_i = '0;
   assign sysctrl.perf_psram_wait_i = '0;
@@ -85,11 +91,11 @@ module sysctrl_formal_design (
   assign pll_ctrl.rsp_valid_i = f_pll_rsp_valid;
   assign pll_ctrl.capable_i = f_pll_capable;
 
-  assign rib_valid = rib.valid;
+  assign rib_valid = apb4.psel;
-  assign rib_addr = rib.addr;
+  assign rib_addr = apb4.paddr;
-  assign rib_wdata = rib.wdata;
+  assign rib_wdata = apb4.pwdata;
-  assign rib_wstrb = rib.wstrb;
+  assign rib_wstrb = apb4.pstrb;
-  assign rib_ready = rib.ready;
+  assign rib_ready = apb4.pready;
   assign ip_sel = sysctrl.ip_sel_o;
   assign core_sel = u_dut.u_sysctrl_core.s_sysctrl_coresel_q;
   assign user_reset = {{(32 - `USER_CORE_COUNT) {1'b0}}, u_dut.u_sysctrl_core.s_user_reset_q};
@@ -117,14 +123,14 @@ module sysctrl_formal_design (
   assign test_pass = sysctrl.test_pass_o;
   assign test_code = sysctrl.test_code_o;
 
-  ribp_sysctrl u_dut (
+  apb4_sysctrl u_dut (
       .clk_i           (clk_i),
       .rst_n_i         (rst_n_i),
       .fault_valid_i   (f_fault_valid),
       .fault_addr_i    (f_fault_addr),
       .fault_wstrb_i   (f_fault_wstrb),
       .fault_reserved_i(f_fault_reserved),
-      .ribp            (rib),
+      .apb4            (apb4),
       .sysctrl         (sysctrl),
       .pll_ctrl        (pll_ctrl)
   );

rtl/mini/formal/timer_formal.sv

@@ -29,25 +29,31 @@ module timer_formal_design (
     // verilog_format: on
 );
 
-  ribp_if rib ();
+  apb4_if apb4 (
+      .pclk   (clk_i),
+      .presetn(rst_n_i)
+  );
 
-  (* anyseq *)logic        f_rib_valid;
+  (* anyseq *)logic        f_apb_sel;
-  (* anyseq *)logic [31:0] f_rib_addr;
+  (* anyseq *)logic [31:0] f_apb_addr;
-  (* anyseq *)logic [31:0] f_rib_wdata;
+  (* anyseq *)logic [31:0] f_apb_wdata;
-  (* anyseq *)logic [ 3:0] f_rib_wstrb;
+  (* anyseq *)logic [ 3:0] f_apb_pstrb;
   (* anyseq *)logic        f_debug_halted;
 
-  assign rib.valid      = f_rib_valid;
+  assign apb4.psel      = f_apb_sel;
-  assign rib.addr       = f_rib_addr;
+  assign apb4.penable   = f_apb_sel;
-  assign rib.wdata      = f_rib_wdata;
+  assign apb4.pwrite    = |f_apb_pstrb;
-  assign rib.wstrb      = f_rib_wstrb;
+  assign apb4.paddr     = f_apb_addr;
+  assign apb4.pwdata    = f_apb_wdata;
+  assign apb4.pstrb     = f_apb_pstrb;
+  assign apb4.pprot     = 3'b000;
 
-  assign rib_valid      = rib.valid;
+  assign rib_valid      = apb4.psel;
-  assign rib_addr       = rib.addr;
+  assign rib_addr       = apb4.paddr;
-  assign rib_wdata      = rib.wdata;
+  assign rib_wdata      = apb4.pwdata;
-  assign rib_wstrb      = rib.wstrb;
+  assign rib_wstrb      = apb4.pstrb;
-  assign rib_ready      = rib.ready;
+  assign rib_ready      = apb4.pready;
-  assign rib_resp_err   = rib.resp_err;
+  assign rib_resp_err   = apb4.pslverr;
   assign debug_halted   = f_debug_halted;
   assign active         = u_dut.s_en;
   assign debug_frozen   = u_dut.s_debug_frozen;
@@ -62,11 +68,11 @@ module timer_formal_design (
   assign intr_state     = u_dut.u_timer_reg.s_intr_state_q;
   assign intr_enable    = u_dut.u_timer_reg.s_intr_en_q;
 
-  ribp_timer u_dut (
+  apb4_timer u_dut (
       .clk_i         (clk_i),
       .rst_n_i       (rst_n_i),
       .debug_halted_i(f_debug_halted),
-      .ribp          (rib),
+      .apb4          (apb4),
       .irq_o         (irq)
   );
 

rtl/mini/formal/uart_formal.sv

@@ -37,29 +37,35 @@ module uart_formal_design (
     // verilog_format: on
 );
 
-  ribp_if ribp ();
+  apb4_if apb4 (
+      .pclk   (clk_i),
+      .presetn(rst_n_i)
+  );
   uart_if uart ();
 
-  (* anyseq *)logic        f_rib_valid;
+  (* anyseq *)logic        f_apb_sel;
-  (* anyseq *)logic [31:0] f_rib_addr;
+  (* anyseq *)logic [31:0] f_apb_addr;
-  (* anyseq *)logic [31:0] f_rib_wdata;
+  (* anyseq *)logic [31:0] f_apb_wdata;
-  (* anyseq *)logic [ 3:0] f_rib_wstrb;
+  (* anyseq *)logic [ 3:0] f_apb_pstrb;
   (* anyseq *)logic        f_uart_rx;
   (* anyseq *)logic        f_uart_cts_n;
 
-  assign ribp.valid       = f_rib_valid;
+  assign apb4.psel        = f_apb_sel;
-  assign ribp.addr        = f_rib_addr;
+  assign apb4.penable     = f_apb_sel;
-  assign ribp.wdata       = f_rib_wdata;
+  assign apb4.pwrite      = |f_apb_pstrb;
-  assign ribp.wstrb       = f_rib_wstrb;
+  assign apb4.paddr       = f_apb_addr;
+  assign apb4.pwdata      = f_apb_wdata;
+  assign apb4.pstrb       = f_apb_pstrb;
+  assign apb4.pprot       = 3'b000;
   assign uart.rx_i        = f_uart_rx;
   assign uart.cts_n_i     = f_uart_cts_n;
 
-  assign rib_valid        = ribp.valid;
+  assign rib_valid        = apb4.psel;
-  assign rib_addr         = ribp.addr;
+  assign rib_addr         = apb4.paddr;
-  assign rib_wdata        = ribp.wdata;
+  assign rib_wdata        = apb4.pwdata;
-  assign rib_wstrb        = ribp.wstrb;
+  assign rib_wstrb        = apb4.pstrb;
-  assign rib_ready        = ribp.ready;
+  assign rib_ready        = apb4.pready;
-  assign rib_resp_err     = ribp.resp_err;
+  assign rib_resp_err     = apb4.pslverr;
   assign tx_count         = u_dut.u_uart_reg.s_tx_count;
   assign rx_count         = u_dut.u_uart_reg.s_rx_count;
   assign error_status     = u_dut.u_uart_reg.s_err_stat_q;
@@ -81,12 +87,12 @@ module uart_formal_design (
   assign rts_n            = uart.rts_n_o;
   assign irq              = uart.irq_o;
 
-  ribp_uart u_dut (
+  apb4_uart u_dut (
       .clk_i         (clk_i),
       .rst_n_i       (rst_n_i),
       .dma_tx_stall_o(tx_dma_stall),
       .dma_rx_stall_o(rx_dma_stall),
-      .ribp          (ribp),
+      .apb4          (apb4),
       .uart          (uart)
   );
 

rtl/mini/formal/ws2812_formal.sv

@@ -29,25 +29,31 @@ module ws2812_formal_design (
     output logic [ 3:0] intr_enable
 );
 
-  ribp_if rib ();
+  apb4_if apb4 (
+      .pclk   (clk_i),
+      .presetn(rst_n_i)
+  );
   ws2812_if ws2812 ();
 
-  (* anyseq *)logic        f_rib_valid;
+  (* anyseq *)logic        f_apb_sel;
-  (* anyseq *)logic [31:0] f_rib_addr;
+  (* anyseq *)logic [31:0] f_apb_addr;
-  (* anyseq *)logic [31:0] f_rib_wdata;
+  (* anyseq *)logic [31:0] f_apb_wdata;
-  (* anyseq *)logic [ 3:0] f_rib_wstrb;
+  (* anyseq *)logic [ 3:0] f_apb_pstrb;
 
-  assign rib.valid      = f_rib_valid;
+  assign apb4.psel      = f_apb_sel;
-  assign rib.addr       = f_rib_addr;
+  assign apb4.penable   = f_apb_sel;
-  assign rib.wdata      = f_rib_wdata;
+  assign apb4.pwrite    = |f_apb_pstrb;
-  assign rib.wstrb      = f_rib_wstrb;
+  assign apb4.paddr     = f_apb_addr;
+  assign apb4.pwdata    = f_apb_wdata;
+  assign apb4.pstrb     = f_apb_pstrb;
+  assign apb4.pprot     = 3'b000;
 
-  assign rib_valid      = rib.valid;
+  assign rib_valid      = apb4.psel;
-  assign rib_addr       = rib.addr;
+  assign rib_addr       = apb4.paddr;
-  assign rib_wdata      = rib.wdata;
+  assign rib_wdata      = apb4.pwdata;
-  assign rib_wstrb      = rib.wstrb;
+  assign rib_wstrb      = apb4.pstrb;
-  assign rib_ready      = rib.ready;
+  assign rib_ready      = apb4.pready;
-  assign rib_resp_err   = rib.resp_err;
+  assign rib_resp_err   = apb4.pslverr;
   assign dat            = ws2812.dat_o;
   assign irq            = ws2812.irq_o;
   assign busy           = u_dut.s_busy;
@@ -65,10 +71,10 @@ module ws2812_formal_design (
   assign intr_state     = u_dut.u_ws2812_reg.s_intr_state_q;
   assign intr_enable    = u_dut.u_ws2812_reg.s_intr_en_q;
 
-  ribp_ws2812 u_dut (
+  apb4_ws2812 u_dut (
       .clk_i  (clk_i),
       .rst_n_i(rst_n_i),
-      .ribp   (rib),
+      .apb4   (apb4),
       .ws2812 (ws2812)
   );
 

rtl/mini/mk/formal.mk

@@ -97,6 +97,7 @@ FORMAL_SOURCE_FILES       := $(RTL_PATH)/formal/bus_formal.sv \
                              $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/clkrst/counter.sv \
                              $(RTL_PATH)/top/rcu.sv \
                              $(RTL_PATH)/top/pll_rcu_controller.sv \
+                             $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/interface/apb4_if.sv \
                              $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/interface/ribp_if.sv \
                              $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/interface/apb4_pure_if.sv \
                              $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/cdc/cdc_sync.sv \

tests/test_script_tools.py

@@ -267,12 +267,14 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non
     assert ROOT / "rtl/mini/top/pll_rcu_controller.sv" in pll_rcu.files
     assert ROOT / "rtl/managed/clusterip/common/rtl/cdc/cdc_2phase.sv" in pll_rcu.files
     assert ROOT / "rtl/managed/clusterip/common/rtl/clkrst/rst_sync.sv" in pll_rcu.files
+    assert ROOT / "rtl/managed/clusterip/common/rtl/interface/apb4_if.sv" in gpio.files
     assert ROOT / "rtl/ip/peripheral/gpio_core.sv" in gpio.files
     assert ROOT / "rtl/ip/peripheral/gpio_reg.sv" in gpio.files
     assert ROOT / "rtl/ip/peripheral/apb4_gpio.sv" in gpio.files
     assert ROOT / "rtl/ip/peripheral/user_gpio_if.sv" in gpio.files
     assert ROOT / "rtl/managed/clusterip/common/rtl/cdc/cdc_sync.sv" in gpio.files
     assert ROOT / "rtl/mini/formal/gpio_formal.sv" in gpio.files
+    assert ROOT / "rtl/managed/clusterip/common/rtl/interface/apb4_if.sv" in ws2812.files
     assert ROOT / "rtl/ip/serial/apb4_ws2812.sv" in ws2812.files
     assert ROOT / "rtl/managed/clusterip/common/rtl/utils/fifo.sv" in ws2812.files
     assert ROOT / "rtl/mini/formal/ws2812_formal.sv" in ws2812.files