diff --git a/rtl/mini/formal/bus_formal.sv b/rtl/mini/formal/bus_formal.sv index f2c7b6c9..1849a660 100644 --- a/rtl/mini/formal/bus_formal.sv +++ b/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(), diff --git a/rtl/mini/formal/clint_formal.sv b/rtl/mini/formal/clint_formal.sv index 52ac1a5c..774abf12 100644 --- a/rtl/mini/formal/clint_formal.sv +++ b/rtl/mini/formal/clint_formal.sv @@ -22,11 +22,14 @@ module clint_formal_design ( // verilog_format: on ); - ribp_if ribp (); - (* anyseq *)logic f_rib_valid; - (* anyseq *)logic [31:0] f_rib_addr; - (* anyseq *)logic [31:0] f_rib_wdata; - (* anyseq *)logic [ 3:0] f_rib_wstrb; + apb4_if apb4 ( + .pclk (clk_i), + .presetn(rst_n_i) + ); + (* 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 ribp.addr = f_rib_addr; - assign ribp.wdata = f_rib_wdata; - assign ribp.wstrb = f_rib_wstrb; + assign apb4.psel = f_apb_sel; + assign apb4.penable = f_apb_sel; + assign apb4.pwrite = |f_apb_pstrb; + 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_addr = ribp.addr; - assign rib_wdata = ribp.wdata; - assign rib_wstrb = ribp.wstrb; - assign rib_ready = ribp.ready; - assign rib_resp_err = ribp.resp_err; + assign rib_valid = apb4.psel; + assign rib_addr = apb4.paddr; + assign rib_wdata = apb4.pwdata; + assign rib_wstrb = apb4.pstrb; + assign rib_ready = apb4.pready; + 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), diff --git a/rtl/mini/formal/dvp_formal.sv b/rtl/mini/formal/dvp_formal.sv index a08e61cd..2a01fcc0 100644 --- a/rtl/mini/formal/dvp_formal.sv +++ b/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 (); - (* anyseq *) logic f_rib_valid; - (* anyseq *) logic [31:0] f_rib_addr, f_rib_wdata; - (* anyseq *) logic [3:0] f_rib_wstrb; + apb4_if apb4 ( + .pclk (clk_i), + .presetn(rst_n_i) + ); + (* 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 rib.addr = f_rib_addr; - assign rib.wdata = f_rib_wdata; - assign rib.wstrb = f_rib_wstrb; - assign rib_valid = rib.valid; - assign rib_addr = rib.addr; - assign rib_wdata = rib.wdata; - assign rib_wstrb = rib.wstrb; - assign rib_ready = rib.ready; - assign rib_resp_err = rib.resp_err; + assign apb4.psel = f_apb_sel; + assign apb4.penable = f_apb_sel; + assign apb4.pwrite = |f_apb_pstrb; + 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 = apb4.psel; + assign rib_addr = apb4.paddr; + 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), diff --git a/rtl/mini/formal/generate_formal_filelist.py b/rtl/mini/formal/generate_formal_filelist.py index df6f7128..8d538065 100644 --- a/rtl/mini/formal/generate_formal_filelist.py +++ b/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", diff --git a/rtl/mini/formal/gpio_formal.sv b/rtl/mini/formal/gpio_formal.sv index 1bfbc4a7..dba5bce3 100644 --- a/rtl/mini/formal/gpio_formal.sv +++ b/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 [31:0] f_ribp_addr; - (* anyseq *)logic [31:0] f_ribp_wdata; - (* anyseq *)logic [ 3:0] f_ribp_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 [ 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 ribp.addr = f_ribp_addr; - assign ribp.wdata = f_ribp_wdata; - assign ribp.wstrb = f_ribp_wstrb; + assign apb4.psel = f_apb_sel; + assign apb4.penable = f_apb_sel; + assign apb4.pwrite = |f_apb_pstrb; + 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_ready = ribp.ready; - assign ribp_resp_err = ribp.resp_err; - assign ribp_addr = ribp.addr; - assign ribp_wdata = ribp.wdata; - assign ribp_wstrb = ribp.wstrb; + assign ribp_valid = apb4.psel; + assign ribp_ready = apb4.pready; + assign ribp_resp_err = apb4.pslverr; + assign ribp_addr = apb4.paddr; + assign ribp_wdata = apb4.pwdata; + 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) ); diff --git a/rtl/mini/formal/i2c_formal.sv b/rtl/mini/formal/i2c_formal.sv index 2ed96d3a..8ee146e0 100644 --- a/rtl/mini/formal/i2c_formal.sv +++ b/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 [31:0] f_rib_addr; - (* 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_scl; (* anyseq *)logic f_sda; - assign ribp.valid = f_rib_valid; - assign ribp.addr = f_rib_addr; - assign ribp.wdata = f_rib_wdata; - assign ribp.wstrb = f_rib_wstrb; + assign apb4.psel = f_apb_sel; + assign apb4.penable = f_apb_sel; + assign apb4.pwrite = |f_apb_pstrb; + 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_addr = ribp.addr; - assign rib_wdata = ribp.wdata; - assign rib_wstrb = ribp.wstrb; - assign rib_ready = ribp.ready; - assign rib_resp_err = ribp.resp_err; + assign rib_valid = apb4.psel; + assign rib_addr = apb4.paddr; + assign rib_wdata = apb4.pwdata; + assign rib_wstrb = apb4.pstrb; + assign rib_ready = apb4.pready; + 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) ); diff --git a/rtl/mini/formal/sysctrl_formal.sv b/rtl/mini/formal/sysctrl_formal.sv index 06f06c8d..037aded8 100644 --- a/rtl/mini/formal/sysctrl_formal.sv +++ b/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 [31:0] f_rib_addr; - (* 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_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 rib.addr = f_rib_addr; - assign rib.wdata = f_rib_wdata; - assign rib.wstrb = f_rib_wstrb; + assign apb4.psel = f_apb_sel; + assign apb4.penable = f_apb_sel; + assign apb4.pwrite = |f_apb_pstrb; + 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_addr = rib.addr; - assign rib_wdata = rib.wdata; - assign rib_wstrb = rib.wstrb; - assign rib_ready = rib.ready; + assign rib_valid = apb4.psel; + assign rib_addr = apb4.paddr; + assign rib_wdata = apb4.pwdata; + assign rib_wstrb = apb4.pstrb; + 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) ); diff --git a/rtl/mini/formal/timer_formal.sv b/rtl/mini/formal/timer_formal.sv index ebee9ec8..dad4f2de 100644 --- a/rtl/mini/formal/timer_formal.sv +++ b/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 [31:0] f_rib_addr; - (* 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_debug_halted; - assign rib.valid = f_rib_valid; - assign rib.addr = f_rib_addr; - assign rib.wdata = f_rib_wdata; - assign rib.wstrb = f_rib_wstrb; + assign apb4.psel = f_apb_sel; + assign apb4.penable = f_apb_sel; + assign apb4.pwrite = |f_apb_pstrb; + 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_addr = rib.addr; - assign rib_wdata = rib.wdata; - assign rib_wstrb = rib.wstrb; - assign rib_ready = rib.ready; - assign rib_resp_err = rib.resp_err; + assign rib_valid = apb4.psel; + assign rib_addr = apb4.paddr; + assign rib_wdata = apb4.pwdata; + assign rib_wstrb = apb4.pstrb; + assign rib_ready = apb4.pready; + 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) ); diff --git a/rtl/mini/formal/uart_formal.sv b/rtl/mini/formal/uart_formal.sv index 716adf94..d44d98ac 100644 --- a/rtl/mini/formal/uart_formal.sv +++ b/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 [31:0] f_rib_addr; - (* 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_uart_rx; (* anyseq *)logic f_uart_cts_n; - assign ribp.valid = f_rib_valid; - assign ribp.addr = f_rib_addr; - assign ribp.wdata = f_rib_wdata; - assign ribp.wstrb = f_rib_wstrb; + assign apb4.psel = f_apb_sel; + assign apb4.penable = f_apb_sel; + assign apb4.pwrite = |f_apb_pstrb; + 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_addr = ribp.addr; - assign rib_wdata = ribp.wdata; - assign rib_wstrb = ribp.wstrb; - assign rib_ready = ribp.ready; - assign rib_resp_err = ribp.resp_err; + assign rib_valid = apb4.psel; + assign rib_addr = apb4.paddr; + assign rib_wdata = apb4.pwdata; + assign rib_wstrb = apb4.pstrb; + assign rib_ready = apb4.pready; + 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) ); diff --git a/rtl/mini/formal/ws2812_formal.sv b/rtl/mini/formal/ws2812_formal.sv index eb0275cb..1ae69131 100644 --- a/rtl/mini/formal/ws2812_formal.sv +++ b/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 [31:0] f_rib_addr; - (* 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; - assign rib.valid = f_rib_valid; - assign rib.addr = f_rib_addr; - assign rib.wdata = f_rib_wdata; - assign rib.wstrb = f_rib_wstrb; + assign apb4.psel = f_apb_sel; + assign apb4.penable = f_apb_sel; + assign apb4.pwrite = |f_apb_pstrb; + 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_addr = rib.addr; - assign rib_wdata = rib.wdata; - assign rib_wstrb = rib.wstrb; - assign rib_ready = rib.ready; - assign rib_resp_err = rib.resp_err; + assign rib_valid = apb4.psel; + assign rib_addr = apb4.paddr; + assign rib_wdata = apb4.pwdata; + assign rib_wstrb = apb4.pstrb; + assign rib_ready = apb4.pready; + 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) ); diff --git a/rtl/mini/mk/formal.mk b/rtl/mini/mk/formal.mk index 16fccc8e..e4310c9a 100644 --- a/rtl/mini/mk/formal.mk +++ b/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 \ diff --git a/tests/test_script_tools.py b/tests/test_script_tools.py index c93155f2..650c2d68 100644 --- a/tests/test_script_tools.py +++ b/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