diff --git a/Makefile b/Makefile index c253b9a2..9bf0e749 100644 --- a/Makefile +++ b/Makefile @@ -210,7 +210,7 @@ endif benchmark-report \ pin-map check-pin-map soc-topology check-soc-topology user-extensions check-user-extensions \ check-clock-reset-domains tech-cell-test rtl-lint check-rtl-lint \ - formal formal-bus formal-rib-adapter formal-ribp2apb formal-clean formal-doctor + formal formal-bus formal-rib-adapter formal-rib2apb formal-clean formal-doctor .NOTPARALLEL: setup help: @@ -235,7 +235,7 @@ help: ' check-user-extensions validate the canonical user-extension map' \ ' check-clock-reset-domains validate the root clock/reset and CDC inventory' \ ' rtl-lint | check-rtl-lint run/check strict Verilator RTL lint warnings' \ - ' formal | formal-bus | formal-rib-adapter | formal-ribp2apb run SBY protocol proofs' \ + ' formal | formal-bus | formal-rib-adapter | formal-rib2apb run SBY protocol proofs' \ ' formal-sysctrl | formal-pll-rcu | formal-gpio-user run SBY peripheral-control proofs' \ ' formal-doctor check the SBY, Yosys, sv2v, and Bitwuzla formal toolchain' \ ' benchmark-report run the benchmark profile and write meta/performance.json' \ @@ -383,4 +383,4 @@ regress-nightly: sim-asm: asm $(MAKE) SIM_FIRMWARE_NAME=$(ASM_FIRMWARE_NAME) \ - SIM_SUCCESS_MARKER='Mem wr/rd test success' sim \ No newline at end of file + SIM_SUCCESS_MARKER='Mem wr/rd test success' sim diff --git a/docs/engineering.md b/docs/engineering.md index e044c235..a0a36f9d 100644 --- a/docs/engineering.md +++ b/docs/engineering.md @@ -111,7 +111,7 @@ Verilator regressions. `make CONFIG=configs/ci/ihp130.mk formal` proves selected protocol invariants with SymbiYosys, Yosys, `sv2v`, and Bitwuzla. The current -targets are `bus`, `rib_adapter`, `ribp2apb`, `sysctrl`, `pll_rcu`, and +targets are `bus`, `rib_adapter`, `rib2apb`, `sysctrl`, `pll_rcu`, and `gpio_user`; each uses the SBY `prove` task for bounded model checking and k-induction, plus a `cover` task, at depth 20. `sysctrl` checks register side effects, PLL request diff --git a/docs/mini-soc-block-diagram.dot b/docs/mini-soc-block-diagram.dot index b82255c1..2e42c300 100644 --- a/docs/mini-soc-block-diagram.dot +++ b/docs/mini-soc-block-diagram.dot @@ -104,7 +104,7 @@ digraph mini_soc_block_diagram { ]; apb_adapter [ fillcolor="#E5E7EB", - label="RIB2RIBP\nAPB bridge" + label="RIB2APB\ndirect APB bridge" ]; sysctrl [ fillcolor="#F9E1E7", @@ -124,7 +124,7 @@ digraph mini_soc_block_diagram { ]; irq [ fillcolor="#FCE7F3", - label="Interrupt aggregation\nRIBP and APB sources to management core" + label="Interrupt aggregation\nRIBP and APB target IRQs to management core" ]; } } @@ -149,7 +149,7 @@ digraph mini_soc_block_diagram { fabric -> apb_adapter [label="RIB"]; ribp_adapter -> sysctrl [label="RIBP"]; ribp_adapter -> ribp_targets [label="RIBP"]; - apb_adapter -> apb_targets [label="RIBP / APB"]; + apb_adapter -> apb_targets [label="APB"]; ribp_targets -> gpio_bridge [label="GPIO alternate functions"]; apb_targets -> gpio_bridge [label="user_gpio"]; diff --git a/docs/mini-soc-block-diagram.svg b/docs/mini-soc-block-diagram.svg index 82d030e0..c8db78f7 100644 --- a/docs/mini-soc-block-diagram.svg +++ b/docs/mini-soc-block-diagram.svg @@ -44,10 +44,10 @@ ext_io - -External I/O and memory -GPIO, UART0, XPI Flash, SDRAM, PSRAM -SD card, I2C, I2S, DVP and serial I/O + +External I/O and memory +GPIO, UART0, XPI Flash, SDRAM, PSRAM +SD card, I2C, I2S, DVP and serial I/O @@ -152,22 +152,22 @@ ribp_adapter - -RIB2RIBP + +RIB2RIBP fabric->ribp_adapter - - -RIB + + +RIB apb_adapter - -RIB2RIBP -APB bridge + +RIB2APB +direct APB bridge @@ -179,91 +179,91 @@ sysctrl - -SYSCTRL and CLINT -PLL, user-core select/reset/bus enable -fault and performance control + +SYSCTRL and CLINT +PLL, user-core select/reset/bus enable +fault and performance control ribp_adapter->sysctrl - - -RIBP + + +RIBP ribp_targets - -RIBP target wrapper -XPI/Flash, SDRAM, PSRAM, SPI-SD, DVP -GPIO, UART0, timers, I2C, I2S and 1-Wire + +RIBP target wrapper +XPI/Flash, SDRAM, PSRAM, SPI-SD, DVP +GPIO, UART0, timers, I2C, I2S and 1-Wire ribp_adapter->ribp_targets - - -RIBP + + +RIBP apb_targets - -APB target wrapper -Archinfo, RNG, UART1, PWM, PS/2, RTC -watchdog, CRC, advanced timer and user IP + +APB target wrapper +Archinfo, RNG, UART1, PWM, PS/2, RTC +watchdog, CRC, advanced timer and user IP apb_adapter->apb_targets - - -RIBP / APB + + +APB ribp_targets->ext_io - - - -device interfaces + + + +device interfaces gpio_bridge - -GPIO pad bridge -software, alternate and user modes + +GPIO pad bridge +software, alternate and user modes ribp_targets->gpio_bridge - - -GPIO alternate functions + + +GPIO alternate functions apb_targets->gpio_bridge - - -user_gpio + + +user_gpio gpio_bridge->ext_io - - - -pad control + + + +pad control irq - -Interrupt aggregation -RIBP and APB sources to management core + +Interrupt aggregation +RIBP and APB target IRQs to management core diff --git a/rtl/ip/ribp/interconnect/ribp2apb.sv b/rtl/ip/ribp/interconnect/ribp2apb.sv deleted file mode 100644 index ef07107c..00000000 --- a/rtl/ip/ribp/interconnect/ribp2apb.sv +++ /dev/null @@ -1,84 +0,0 @@ -// Copyright (c) 2023-2026 Yuchi Miao -// retroSoC is licensed under Mulan PSL v2. -// You can use this software according to the terms and conditions of the Mulan PSL v2. -// You may obtain a copy of Mulan PSL v2 at: -// http://license.coscl.org.cn/MulanPSL2 -// THIS SOFTWARE IS PROVIDED ON AN "AS IS" BASIS, WITHOUT WARRANTIES OF ANY KIND, -// EITHER EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO NON-INFRINGEMENT, -// MERCHANTABILITY OR FIT FOR A PARTICULAR PURPOSE. -// See the Mulan PSL v2 for more details. - -`include "mmap_define.svh" - -module ribp2apb ( - // verilog_format: off - input logic clk_i, - input logic rst_n_i, - ribp_if.slave ribp, -`include "soc_apb_ports.svh" - // verilog_format: on -); - - localparam FSM_IDLE = 2'd0; - localparam FSM_SETP = 2'd1; - localparam FSM_ENAB = 2'd2; - - logic [31:0] s_rd_data; - logic s_xfer_valid, s_xfer_ready, s_xfer_error; - logic s_mem_valid_re; - logic [1:0] s_fsm_d, s_fsm_q; - - // Registered slave-select one-hot for response mux - `include "soc_apb_declarations.svh" - - - // Generated APB request routing retains the scalar interface protocol. - `include "soc_apb_request_routes.svh" - - // verilog_format: off - edge_det_sync_re #(1) u_mem_valid_edge_det_sync_re ( - clk_i, - rst_n_i, - ribp.valid, - s_mem_valid_re - ); - // verilog_format: on - - assign s_xfer_valid = ((s_fsm_q == FSM_IDLE) && s_mem_valid_re) || - (s_fsm_q == FSM_SETP) || (s_fsm_q == FSM_ENAB); - - always_comb begin - s_fsm_d = s_fsm_q; - unique case (s_fsm_q) - FSM_IDLE: if (s_mem_valid_re) s_fsm_d = FSM_SETP; - FSM_SETP: s_fsm_d = FSM_ENAB; - FSM_ENAB: if (s_xfer_ready) s_fsm_d = FSM_IDLE; - default: s_fsm_d = s_fsm_q; - endcase - end - dffr #(2) u_fsm_dffr ( - clk_i, - rst_n_i, - s_fsm_d, - s_fsm_q - ); - - assign ribp.ready = ribp.valid && (s_fsm_q == FSM_ENAB) && s_xfer_ready; - assign ribp.rdata = {32{ribp.ready}} & s_rd_data; - assign ribp.resp_err = ribp.ready && s_xfer_error; - - // Capture slave-select one-hot at FSM_SETP for cleaner response mux. - `include "soc_apb_select_routes.svh" - - assign s_psel_d = (s_fsm_q == FSM_IDLE && s_mem_valid_re) ? s_psel_comb : s_psel_q; - dffr #(NSLV) u_psel_dffr ( - clk_i, - rst_n_i, - s_psel_d, - s_psel_q - ); - - // Generated response mux uses the registered one-hot target selection. - `include "soc_apb_response_mux.svh" - -endmodule diff --git a/rtl/mini/dv/sva/rib_protocol_sva.sv b/rtl/mini/dv/sva/rib_protocol_sva.sv index ebe3157a..c3f840a2 100644 --- a/rtl/mini/dv/sva/rib_protocol_sva.sv +++ b/rtl/mini/dv/sva/rib_protocol_sva.sv @@ -61,25 +61,34 @@ module rib2apb_sva #( input logic rst_n_i, input logic [NSLV-1:0] psel_comb_i, input logic [NSLV-1:0] psel_q_i, - input logic rib_ready_i, + input logic [ 2:0] fsm_q_i, + input logic rsp_valid_i, + input logic [ 1:0] rsp_beat_i, + input logic rsp_last_i, input logic xfer_ready_i ); // Address regions are disjoint and only the registered select drives a response. assert property (@(posedge clk_i) disable iff (!rst_n_i) $onehot0(psel_comb_i)); assert property (@(posedge clk_i) disable iff (!rst_n_i) $onehot0(psel_q_i)); - assert property (@(posedge clk_i) disable iff (!rst_n_i) rib_ready_i |-> xfer_ready_i); + assert property (@(posedge clk_i) disable iff (!rst_n_i) + fsm_q_i == 3'd3 && !xfer_ready_i |=> fsm_q_i == 3'd3); + assert property (@(posedge clk_i) disable iff (!rst_n_i) + rsp_valid_i |-> rsp_beat_i == 2'd0 && rsp_last_i); endmodule -bind ribp2apb rib2apb_sva #( +bind rib2apb rib2apb_sva #( .NSLV(NSLV) ) u_rib2apb_sva ( .clk_i (clk_i), .rst_n_i (rst_n_i), .psel_comb_i (s_psel_comb), .psel_q_i (s_psel_q), - .rib_ready_i (ribp.ready), + .fsm_q_i (s_fsm_q), + .rsp_valid_i (rib.rsp_valid), + .rsp_beat_i (rib.rsp_beat), + .rsp_last_i (rib.rsp_last), .xfer_ready_i(s_xfer_ready) ); diff --git a/rtl/mini/filelist/ip.fl b/rtl/mini/filelist/ip.fl index 7e744a71..0cc5f1ee 100644 --- a/rtl/mini/filelist/ip.fl +++ b/rtl/mini/filelist/ip.fl @@ -40,7 +40,6 @@ /ip/ribp/peripheral/timer.sv /ip/ribp/serial/uart.sv /ip/ribp/peripheral/gpio.sv -/ip/ribp/interconnect/ribp2apb.sv /top/ahbl2ribp.sv /ip/ribp/interconnect/axi4l2ribp.sv /ip/ribp/util/async_fifo.sv diff --git a/rtl/mini/filelist/top.fl b/rtl/mini/filelist/top.fl index b8ad144d..82367f5a 100644 --- a/rtl/mini/filelist/top.fl +++ b/rtl/mini/filelist/top.fl @@ -2,6 +2,7 @@ /top/gpio_pad_bridge.sv /top/ribp2rib.sv /top/rib2ribp.sv +/top/rib2apb.sv /top/rib_error_slave.sv /top/rib2ram.sv /top/core_wrapper.sv diff --git a/rtl/mini/formal/bus_formal.sv b/rtl/mini/formal/bus_formal.sv index 79a60040..f018ab79 100644 --- a/rtl/mini/formal/bus_formal.sv +++ b/rtl/mini/formal/bus_formal.sv @@ -34,7 +34,7 @@ module bus_formal_design ( rib_if user_rib (); rib_if dma_rib (); rib_if rib (); - ribp_if apb_ribp (); + rib_if apb_rib (); (* anyseq *)logic f_mgmt_valid; (* anyseq *)logic [31:0] f_mgmt_addr; @@ -64,6 +64,9 @@ module bus_formal_design ( logic target_write_done_q; logic [ 1:0] target_len_q; logic [ 1:0] target_beat_q; + logic apb_active_q; + logic apb_write_q; + logic apb_write_done_q; logic [31:0] fault_addr; logic [ 3:0] fault_wstrb; logic fault_reserved; @@ -138,27 +141,52 @@ module bus_formal_design ( end end - assign apb_ribp.ready = apb_ribp.valid; - assign apb_ribp.rdata = 32'h1234_5678; - assign apb_ribp.resp_err = 1'b0; + assign apb_rib.cmd_ready = ~apb_active_q; + assign apb_rib.w_ready = apb_active_q && apb_write_q && ~apb_write_done_q; + assign apb_rib.rsp_valid = apb_active_q && (~apb_write_q || apb_write_done_q); + assign apb_rib.rdata = 32'h1234_5678; + assign apb_rib.resp_err = 1'b0; + assign apb_rib.resp_code = `RIB_RESP_OK; + assign apb_rib.rsp_beat = '0; + assign apb_rib.rsp_last = 1'b1; - assign mgmt_valid = mgmt_ribp.valid; - assign mgmt_addr = mgmt_ribp.addr; - assign mgmt_wstrb = mgmt_ribp.wstrb; - assign mgmt_ready = mgmt_ribp.ready; - assign user_cmd_valid = user_rib.cmd_valid; - assign user_cmd_ready = user_rib.cmd_ready; - assign user_cmd_addr = user_rib.cmd_addr; - assign user_cmd_write = user_rib.cmd_write; - assign user_cmd_len = user_rib.cmd_len; - assign dma_cmd_valid = dma_rib.cmd_valid; - assign dma_cmd_ready = dma_rib.cmd_ready; - assign dma_cmd_addr = dma_rib.cmd_addr; - assign dma_cmd_write = dma_rib.cmd_write; - assign dma_cmd_len = dma_rib.cmd_len; - assign rib_cmd_valid = rib.cmd_valid; - assign rib_cmd_len = rib.cmd_len; - assign apb_valid = apb_ribp.valid; + always_ff @(posedge clk_i) begin + if (!rst_n_i) begin + apb_active_q <= 1'b0; + apb_write_q <= 1'b0; + apb_write_done_q <= 1'b0; + end else begin + if (apb_rib.cmd_valid && apb_rib.cmd_ready) begin + apb_active_q <= 1'b1; + apb_write_q <= apb_rib.cmd_write; + apb_write_done_q <= 1'b0; + end + if (apb_rib.w_valid && apb_rib.w_ready && apb_rib.wlast) begin + apb_write_done_q <= 1'b1; + end + if (apb_rib.rsp_valid && apb_rib.rsp_ready) begin + apb_active_q <= 1'b0; + end + end + end + + assign mgmt_valid = mgmt_ribp.valid; + assign mgmt_addr = mgmt_ribp.addr; + assign mgmt_wstrb = mgmt_ribp.wstrb; + assign mgmt_ready = mgmt_ribp.ready; + assign user_cmd_valid = user_rib.cmd_valid; + assign user_cmd_ready = user_rib.cmd_ready; + assign user_cmd_addr = user_rib.cmd_addr; + assign user_cmd_write = user_rib.cmd_write; + assign user_cmd_len = user_rib.cmd_len; + assign dma_cmd_valid = dma_rib.cmd_valid; + assign dma_cmd_ready = dma_rib.cmd_ready; + assign dma_cmd_addr = dma_rib.cmd_addr; + assign dma_cmd_write = dma_rib.cmd_write; + assign dma_cmd_len = dma_rib.cmd_len; + assign rib_cmd_valid = rib.cmd_valid; + assign rib_cmd_len = rib.cmd_len; + assign apb_valid = apb_rib.cmd_valid; bus u_dut ( .clk_i (clk_i), @@ -169,7 +197,7 @@ module bus_formal_design ( .user_bus_enable_i(1'b1), .user_bus_idle_o (user_idle), .rib (rib), - .apb_ribp (apb_ribp), + .apb_rib (apb_rib), .perf_enable_i (1'b0), .perf_clear_i (1'b0), .fault_valid_o (fault_valid), diff --git a/rtl/mini/formal/generate_formal_filelist.py b/rtl/mini/formal/generate_formal_filelist.py index 6baf9f2d..af91c053 100644 --- a/rtl/mini/formal/generate_formal_filelist.py +++ b/rtl/mini/formal/generate_formal_filelist.py @@ -51,14 +51,14 @@ def source_files(target: str) -> list[Path]: TOP / "rib2ribp.sv", SCRIPT_DIR / "rib_adapter_formal.sv", ] - if target == "ribp2apb": + if target == "rib2apb": return [ - COMMON_RTL / "interface/ribp_if.sv", COMMON_RTL / "interface/apb4_pure_if.sv", COMMON_RTL / "utils/register.sv", - COMMON_RTL / "utils/edge_det.sv", - INTERCONNECT / "ribp2apb.sv", - SCRIPT_DIR / "ribp2apb_formal.sv", + COMMON_RTL / "utils/spill_register.sv", + TOP / "rib_if.sv", + TOP / "rib2apb.sv", + SCRIPT_DIR / "rib2apb_formal.sv", ] if target == "sysctrl": return [ @@ -122,7 +122,7 @@ def parse_args() -> argparse.Namespace: choices=( "bus", "rib_adapter", - "ribp2apb", + "rib2apb", "sysctrl", "pll_rcu", "gpio_user", diff --git a/rtl/mini/formal/rib2apb_formal.sv b/rtl/mini/formal/rib2apb_formal.sv new file mode 100644 index 00000000..02e6e5f6 --- /dev/null +++ b/rtl/mini/formal/rib2apb_formal.sv @@ -0,0 +1,153 @@ +// Copyright (c) 2026 Yuchi Miao +// retroSoC is licensed under Mulan PSL v2. +// You can use this software according to the terms and conditions of the Mulan PSL v2. +// You may obtain a copy of the Mulan PSL v2 at: +// http://license.coscl.org.cn/MulanPSL2 +// THIS SOFTWARE IS PROVIDED ON AN "AS IS" BASIS, WITHOUT WARRANTIES OF ANY KIND, +// EITHER EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO NON-INFRINGEMENT, +// MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE. +// See the Mulan PSL v2 for more details. + +module formal_apb_slave ( + apb4_pure_if.slave apb +); + + (* anyseq *)logic f_ready; + (* anyseq *)logic [31:0] f_rdata; + (* anyseq *)logic f_slverr; + + assign apb.pready = f_ready; + assign apb.prdata = f_rdata; + assign apb.pslverr = f_slverr; + +endmodule + + +module rib2apb_formal_design ( + input logic clk_i, + output logic rst_n_i, + output logic f_past_valid, + output logic rib_cmd_valid, + output logic [31:0] rib_cmd_addr, + output logic rib_cmd_write, + output logic [ 1:0] rib_cmd_len, + output logic rib_cmd_ready, + output logic rib_w_valid, + output logic [31:0] rib_wdata, + output logic [ 3:0] rib_wstrb, + output logic rib_wlast, + output logic rib_w_ready, + output logic rib_rsp_valid, + output logic [31:0] rib_rdata, + output logic rib_resp_err, + output logic [ 2:0] rib_resp_code, + output logic [ 1:0] rib_rsp_beat, + output logic rib_rsp_last, + output logic rib_rsp_ready, + output logic [ 9:0] psel_comb, + output logic [ 9:0] psel_q, + output logic xfer_ready, + output logic xfer_error, + output logic rsp_input_valid, + output logic rsp_input_ready, + output logic [38:0] rsp_input_data, + output logic [ 2:0] fsm_q +); + + rib_if rib (); + apb4_pure_if archinfo (); + apb4_pure_if rng (); + apb4_pure_if uart (); + apb4_pure_if pwm (); + apb4_pure_if ps2 (); + apb4_pure_if rtc (); + apb4_pure_if wdg (); + apb4_pure_if crc (); + apb4_pure_if tmr (); + apb4_pure_if user_ip (); + + (* anyseq *)logic f_rib_cmd_valid; + (* anyseq *)logic [31:0] f_rib_cmd_addr; + (* anyseq *)logic f_rib_cmd_write; + (* anyseq *)logic [ 1:0] f_rib_cmd_len; + (* anyseq *)logic f_rib_w_valid; + (* anyseq *)logic [31:0] f_rib_wdata; + (* anyseq *)logic [ 3:0] f_rib_wstrb; + (* anyseq *)logic f_rib_wlast; + (* anyseq *)logic f_rib_rsp_ready; + + assign rib.cmd_valid = f_rib_cmd_valid; + assign rib.cmd_addr = f_rib_cmd_addr; + assign rib.cmd_write = f_rib_cmd_write; + assign rib.cmd_len = f_rib_cmd_len; + assign rib.w_valid = f_rib_w_valid; + assign rib.wdata = f_rib_wdata; + assign rib.wstrb = f_rib_wstrb; + assign rib.wlast = f_rib_wlast; + assign rib.rsp_ready = f_rib_rsp_ready; + + assign rib_cmd_valid = rib.cmd_valid; + assign rib_cmd_addr = rib.cmd_addr; + assign rib_cmd_write = rib.cmd_write; + assign rib_cmd_len = rib.cmd_len; + assign rib_cmd_ready = rib.cmd_ready; + assign rib_w_valid = rib.w_valid; + assign rib_wdata = rib.wdata; + assign rib_wstrb = rib.wstrb; + assign rib_wlast = rib.wlast; + assign rib_w_ready = rib.w_ready; + assign rib_rsp_valid = rib.rsp_valid; + assign rib_rdata = rib.rdata; + assign rib_resp_err = rib.resp_err; + assign rib_resp_code = rib.resp_code; + assign rib_rsp_beat = rib.rsp_beat; + assign rib_rsp_last = rib.rsp_last; + assign rib_rsp_ready = rib.rsp_ready; + + formal_apb_slave u_archinfo_slave (.apb(archinfo)); + formal_apb_slave u_rng_slave (.apb(rng)); + formal_apb_slave u_uart_slave (.apb(uart)); + formal_apb_slave u_pwm_slave (.apb(pwm)); + formal_apb_slave u_ps2_slave (.apb(ps2)); + formal_apb_slave u_rtc_slave (.apb(rtc)); + formal_apb_slave u_wdg_slave (.apb(wdg)); + formal_apb_slave u_crc_slave (.apb(crc)); + formal_apb_slave u_tmr_slave (.apb(tmr)); + formal_apb_slave u_user_ip_slave (.apb(user_ip)); + + rib2apb u_dut ( + .clk_i (clk_i), + .rst_n_i (rst_n_i), + .rib (rib), + .archinfo(archinfo), + .rng (rng), + .uart (uart), + .pwm (pwm), + .ps2 (ps2), + .rtc (rtc), + .wdg (wdg), + .crc (crc), + .tmr (tmr), + .user_ip (user_ip) + ); + + assign psel_comb = u_dut.s_psel_comb; + assign psel_q = u_dut.s_psel_q; + assign xfer_ready = u_dut.s_xfer_ready; + assign xfer_error = u_dut.s_xfer_error; + assign rsp_input_valid = u_dut.s_rsp_input_valid; + assign rsp_input_ready = u_dut.s_rsp_input_ready; + assign rsp_input_data = u_dut.s_rsp_input_data; + assign fsm_q = u_dut.s_fsm_q; + + initial begin + rst_n_i = 1'b0; + f_past_valid = 1'b0; + end + + always_ff @(posedge clk_i) begin + rst_n_i <= 1'b1; + f_past_valid <= 1'b1; + end + +endmodule diff --git a/rtl/mini/formal/rib2apb_formal_props.sv b/rtl/mini/formal/rib2apb_formal_props.sv new file mode 100644 index 00000000..6dc523fc --- /dev/null +++ b/rtl/mini/formal/rib2apb_formal_props.sv @@ -0,0 +1,113 @@ +// Copyright (c) 2026 Yuchi Miao +// retroSoC is licensed under Mulan PSL v2. +// You can use this software according to the terms and conditions of the Mulan PSL v2. +// You may obtain a copy of the Mulan PSL v2 at: +// http://license.coscl.org.cn/MulanPSL2 +// THIS SOFTWARE IS PROVIDED ON AN "AS IS" BASIS, WITHOUT WARRANTIES OF ANY KIND, +// EITHER EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO NON-INFRINGEMENT, +// MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE. +// See the Mulan PSL v2 for more details. + +module rib2apb_formal; + + localparam logic [2:0] FSM_ENAB = 3'd3; + localparam logic [2:0] FSM_ERR = 3'd5; + localparam logic [2:0] RIB_RESP_OK = 3'd0; + localparam logic [2:0] RIB_RESP_SLVERR = 3'd3; + + (* anyseq *) (* gclk *)reg clk_i; + wire rst_n_i; + wire f_past_valid; + wire rib_cmd_valid; + wire [31:0] rib_cmd_addr; + wire rib_cmd_write; + wire [ 1:0] rib_cmd_len; + wire rib_cmd_ready; + wire rib_w_valid; + wire [31:0] rib_wdata; + wire [ 3:0] rib_wstrb; + wire rib_wlast; + wire rib_w_ready; + wire rib_rsp_valid; + wire [31:0] rib_rdata; + wire rib_resp_err; + wire [ 2:0] rib_resp_code; + wire [ 1:0] rib_rsp_beat; + wire rib_rsp_last; + wire rib_rsp_ready; + wire [ 9:0] psel_comb; + wire [ 9:0] psel_q; + wire xfer_ready; + wire xfer_error; + wire rsp_input_valid; + wire rsp_input_ready; + wire [38:0] rsp_input_data; + wire [ 2:0] fsm_q; + + rib2apb_formal_design u_design ( + .clk_i (clk_i), + .rst_n_i (rst_n_i), + .f_past_valid (f_past_valid), + .rib_cmd_valid (rib_cmd_valid), + .rib_cmd_addr (rib_cmd_addr), + .rib_cmd_write (rib_cmd_write), + .rib_cmd_len (rib_cmd_len), + .rib_cmd_ready (rib_cmd_ready), + .rib_w_valid (rib_w_valid), + .rib_wdata (rib_wdata), + .rib_wstrb (rib_wstrb), + .rib_wlast (rib_wlast), + .rib_w_ready (rib_w_ready), + .rib_rsp_valid (rib_rsp_valid), + .rib_rdata (rib_rdata), + .rib_resp_err (rib_resp_err), + .rib_resp_code (rib_resp_code), + .rib_rsp_beat (rib_rsp_beat), + .rib_rsp_last (rib_rsp_last), + .rib_rsp_ready (rib_rsp_ready), + .psel_comb (psel_comb), + .psel_q (psel_q), + .xfer_ready (xfer_ready), + .xfer_error (xfer_error), + .rsp_input_valid(rsp_input_valid), + .rsp_input_ready(rsp_input_ready), + .rsp_input_data (rsp_input_data), + .fsm_q (fsm_q) + ); + + always @(posedge clk_i) begin + if (f_past_valid && $past(rst_n_i && rib_cmd_valid && !rib_cmd_ready)) begin + assume (rib_cmd_valid); + assume (rib_cmd_addr == $past(rib_cmd_addr)); + assume (rib_cmd_write == $past(rib_cmd_write)); + assume (rib_cmd_len == $past(rib_cmd_len)); + end + if (f_past_valid && $past(rst_n_i && rib_w_valid && !rib_w_ready)) begin + assume (rib_w_valid); + assume (rib_wdata == $past(rib_wdata)); + assume (rib_wstrb == $past(rib_wstrb)); + assume (rib_wlast == $past(rib_wlast)); + end + + if (rst_n_i) begin + assert ($onehot0(psel_comb)); + if (f_past_valid && $past(rst_n_i && fsm_q == FSM_ENAB && !xfer_ready)) begin + assert (fsm_q == FSM_ENAB); + assert (psel_q == $past(psel_q)); + end + if (fsm_q == FSM_ENAB && xfer_ready) begin + assert (rsp_input_valid); + assert (rsp_input_data[38:36] == 3'b100); + assert (rsp_input_data[32] == xfer_error); + assert (rsp_input_data[35:33] == (xfer_error ? RIB_RESP_SLVERR : RIB_RESP_OK)); + end + if (fsm_q == FSM_ERR) begin + assert (rsp_input_valid); + assert (rsp_input_data[38:36] == 3'b100); + assert (rsp_input_data[32]); + end + cover (fsm_q == FSM_ENAB && xfer_ready && rsp_input_ready); + end + end + +endmodule diff --git a/rtl/mini/formal/ribp2apb_formal.sv b/rtl/mini/formal/ribp2apb_formal.sv deleted file mode 100644 index c7faf12d..00000000 --- a/rtl/mini/formal/ribp2apb_formal.sv +++ /dev/null @@ -1,113 +0,0 @@ -// Copyright (c) 2026 Yuchi Miao -// retroSoC is licensed under Mulan PSL v2. -// You can use this software according to the terms and conditions of the Mulan PSL v2. -// You may obtain a copy of Mulan PSL v2 at: -// http://license.coscl.org.cn/MulanPSL2 -// THIS SOFTWARE IS PROVIDED ON AN "AS IS" BASIS, WITHOUT WARRANTIES OF ANY KIND, -// EITHER EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO NON-INFRINGEMENT, -// MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE. -// See the Mulan PSL v2 for more details. - -module formal_apb_slave ( - apb4_pure_if.slave apb -); - - (* anyseq *)logic f_ready; - (* anyseq *)logic [31:0] f_rdata; - (* anyseq *)logic f_slverr; - - assign apb.pready = f_ready; - assign apb.prdata = f_rdata; - assign apb.pslverr = f_slverr; - -endmodule - -module ribp2apb_formal_design ( - input logic clk_i, - output logic rst_n_i, - output logic f_past_valid, - output logic rib_valid, - output logic [31:0] rib_addr, - output logic [31:0] rib_wdata, - output logic [ 3:0] rib_wstrb, - output logic rib_ready, - output logic rib_resp_err, - output logic [ 9:0] psel_comb, - output logic [ 9:0] psel_q, - output logic xfer_ready, - output logic xfer_error, - output logic [ 1:0] fsm_q -); - - ribp_if rib (); - apb4_pure_if archinfo (); - apb4_pure_if rng (); - apb4_pure_if uart (); - apb4_pure_if pwm (); - apb4_pure_if ps2 (); - apb4_pure_if rtc (); - apb4_pure_if wdg (); - apb4_pure_if crc (); - apb4_pure_if tmr (); - apb4_pure_if user_ip (); - - (* 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; - - 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; - - formal_apb_slave u_archinfo_slave (.apb(archinfo)); - formal_apb_slave u_rng_slave (.apb(rng)); - formal_apb_slave u_uart_slave (.apb(uart)); - formal_apb_slave u_pwm_slave (.apb(pwm)); - formal_apb_slave u_ps2_slave (.apb(ps2)); - formal_apb_slave u_rtc_slave (.apb(rtc)); - formal_apb_slave u_wdg_slave (.apb(wdg)); - formal_apb_slave u_crc_slave (.apb(crc)); - formal_apb_slave u_tmr_slave (.apb(tmr)); - formal_apb_slave u_user_ip_slave (.apb(user_ip)); - - ribp2apb u_dut ( - .clk_i (clk_i), - .rst_n_i (rst_n_i), - .ribp (rib), - .archinfo(archinfo), - .rng (rng), - .uart (uart), - .pwm (pwm), - .ps2 (ps2), - .rtc (rtc), - .wdg (wdg), - .crc (crc), - .tmr (tmr), - .user_ip (user_ip) - ); - - assign psel_comb = u_dut.s_psel_comb; - assign psel_q = u_dut.s_psel_q; - assign xfer_ready = u_dut.s_xfer_ready; - assign xfer_error = u_dut.s_xfer_error; - assign fsm_q = u_dut.s_fsm_q; - - initial begin - rst_n_i = 1'b0; - f_past_valid = 1'b0; - end - - always_ff @(posedge clk_i) begin - rst_n_i <= 1'b1; - f_past_valid <= 1'b1; - end - -endmodule diff --git a/rtl/mini/formal/ribp2apb_formal_props.sv b/rtl/mini/formal/ribp2apb_formal_props.sv deleted file mode 100644 index 773362d3..00000000 --- a/rtl/mini/formal/ribp2apb_formal_props.sv +++ /dev/null @@ -1,75 +0,0 @@ -// Copyright (c) 2026 Yuchi Miao -// retroSoC is licensed under Mulan PSL v2. -// You can use this software according to the terms and conditions of the Mulan PSL v2. -// You may obtain a copy of Mulan PSL v2 at: -// http://license.coscl.org.cn/MulanPSL2 -// THIS SOFTWARE IS PROVIDED ON AN "AS IS" BASIS, WITHOUT WARRANTIES OF ANY KIND, -// EITHER EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO NON-INFRINGEMENT, -// MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE. -// See the Mulan PSL v2 for more details. - -module ribp2apb_formal; - - localparam [1:0] FSM_SETP = 2'd1; - localparam [1:0] FSM_ENAB = 2'd2; - - (* anyseq *) (* gclk *)reg clk_i; - wire rst_n_i; - wire f_past_valid; - wire rib_valid; - wire [31:0] rib_addr; - wire [31:0] rib_wdata; - wire [ 3:0] rib_wstrb; - wire rib_ready, rib_resp_err; - wire [9:0] psel_comb; - wire [9:0] psel_q; - wire xfer_ready, xfer_error; - wire [1:0] fsm_q; - - ribp2apb_formal_design u_design ( - .clk_i (clk_i), - .rst_n_i (rst_n_i), - .f_past_valid(f_past_valid), - .rib_valid (rib_valid), - .rib_addr (rib_addr), - .rib_wdata (rib_wdata), - .rib_wstrb (rib_wstrb), - .rib_ready (rib_ready), - .rib_resp_err(rib_resp_err), - .psel_comb (psel_comb), - .psel_q (psel_q), - .xfer_ready (xfer_ready), - .xfer_error (xfer_error), - .fsm_q (fsm_q) - ); - - always @(posedge clk_i) begin - if (f_past_valid && $past(rst_n_i && rib_valid && !rib_ready)) begin - assume (rib_valid); - assume (rib_addr == $past(rib_addr)); - assume (rib_wdata == $past(rib_wdata)); - assume (rib_wstrb == $past(rib_wstrb)); - end - - if (rst_n_i) begin - assert ($onehot0(psel_comb)); - assert ($onehot0(psel_q)); - if (rib_ready) begin - assert (xfer_ready); - assert (fsm_q == FSM_ENAB); - assert (rib_resp_err == xfer_error); - end else begin - assert (!rib_resp_err); - end - if (f_past_valid && $past(rst_n_i && fsm_q == FSM_SETP)) begin - assert (psel_q == $past(psel_q)); - end - if (f_past_valid && $past(rst_n_i && fsm_q == FSM_ENAB && !xfer_ready)) begin - assert (fsm_q == FSM_ENAB); - assert (psel_q == $past(psel_q)); - end - cover (fsm_q == FSM_ENAB && rib_ready); - end - end - -endmodule diff --git a/rtl/mini/integration/README.md b/rtl/mini/integration/README.md index ea74fc77..cb9703f1 100644 --- a/rtl/mini/integration/README.md +++ b/rtl/mini/integration/README.md @@ -5,7 +5,7 @@ that is not part of the software address-map ABI or the package pad map. The topology generator validates rib RIB and APB target ownership against `../address_map/memory_map.json` and emits generated SystemVerilog include -files for `ip_ribp_wrapper.sv`, `ip_apb_wrapper.sv`, `ribp2apb.sv`, and +files for `ip_ribp_wrapper.sv`, `ip_apb_wrapper.sv`, `rib2apb.sv`, and `retrosoc.sv`. The output retains scalar interface instances and ports, so it does not depend on interface-array support in FPGA or netlist simulation tools. diff --git a/rtl/mini/integration/generate_soc_topology.py b/rtl/mini/integration/generate_soc_topology.py index 6e6797bf..4ece9183 100644 --- a/rtl/mini/integration/generate_soc_topology.py +++ b/rtl/mini/integration/generate_soc_topology.py @@ -22,7 +22,7 @@ FABRIC_PROTOCOLS = { "user": "rib", "dma": "rib", "rib": "rib", - "apb": "ribp", + "apb": "rib", } IRQ_GROUP_NAMES = ("ribp", "apb") IRQ_VECTOR_WIDTH = 32 @@ -657,7 +657,7 @@ def render_apb_declarations(targets: list[ApbTarget]) -> str: [ "// Generated by rtl/mini/integration/generate_soc_topology.py; do not edit.", f" localparam int NSLV = {count};", - " logic [NSLV-1:0] s_psel_comb, s_psel_d, s_psel_q;", + " logic [NSLV-1:0] s_psel_comb, s_psel_q;", "", ] ) @@ -668,13 +668,13 @@ def render_apb_request_routes(targets: list[ApbTarget]) -> str: for target in targets: lines.extend( [ - f" assign {target.name}.paddr = ribp.addr;", + f" assign {target.name}.paddr = s_addr_q;", f" assign {target.name}.pprot = '0;", - f" assign {target.name}.psel = s_xfer_valid && `SOC_ADDR_IS_{target.region}(ribp.addr);", + f" assign {target.name}.psel = s_xfer_valid && s_psel_q[{target.slot}];", f" assign {target.name}.penable = s_fsm_q == FSM_ENAB;", - f" assign {target.name}.pwrite = |ribp.wstrb;", - f" assign {target.name}.pwdata = ribp.wdata;", - f" assign {target.name}.pstrb = ribp.wstrb;", + f" assign {target.name}.pwrite = s_write_q;", + f" assign {target.name}.pwdata = s_wdata_q;", + f" assign {target.name}.pstrb = s_wstrb_q;", "", ] ) @@ -684,7 +684,7 @@ def render_apb_request_routes(targets: list[ApbTarget]) -> str: def render_apb_select_routes(targets: list[ApbTarget]) -> str: lines = ["// Generated by rtl/mini/integration/generate_soc_topology.py; do not edit."] lines.extend( - f" assign s_psel_comb[{target.slot}] = `SOC_ADDR_IS_{target.region}(ribp.addr);" + f" assign s_psel_comb[{target.slot}] = `SOC_ADDR_IS_{target.region}(rib.cmd_addr);" for target in targets ) return "\n".join(lines) + "\n" @@ -736,7 +736,7 @@ def render_bus_fabric_connections(links: list[FabricLink]) -> str: "user": "user_rib", "dma": "dma_rib", "rib": "rib", - "apb": "apb_ribp", + "apb": "apb_rib", } interfaces = {link.name: link.interface for link in links} lines = ["// Generated by rtl/mini/integration/generate_soc_topology.py; do not edit."] @@ -905,7 +905,7 @@ def generate(topology_path: Path, memory_map_path: Path, output_dir: Path) -> No ) atomic_write( rtl_dir / "soc_ip_apb_wrapper_fabric.svh", - render_fabric_connection(fabric_links, "apb", "ribp"), + render_fabric_connection(fabric_links, "apb", "rib"), ) atomic_write(rtl_dir / "soc_gpio_alt_bindings.svh", render_gpio_bindings(gpio_functions)) atomic_write(rtl_dir / "soc_irq_config.svh", render_irq_config(irq_vector_width, irq_groups)) diff --git a/rtl/mini/integration/soc_topology.json b/rtl/mini/integration/soc_topology.json index 1c440a0f..0dd82f84 100644 --- a/rtl/mini/integration/soc_topology.json +++ b/rtl/mini/integration/soc_topology.json @@ -50,7 +50,7 @@ {"name": "user", "interface": "u_user_rib_if", "protocol": "rib"}, {"name": "dma", "interface": "u_dma_rib_if", "protocol": "rib"}, {"name": "rib", "interface": "u_rib_if", "protocol": "rib"}, - {"name": "apb", "interface": "u_apb_ribp_if", "protocol": "ribp"} + {"name": "apb", "interface": "u_apb_rib_if", "protocol": "rib"} ], "apb_targets": [ {"slot": 0, "name": "archinfo", "timed_interface": "u_archinfo_apb_if", "pure_interface": "u_archinfo_apb_pure_if", "region": "APB_ARCHINFO"}, diff --git a/rtl/mini/mk/formal.mk b/rtl/mini/mk/formal.mk index 4047bcff..7a29020d 100644 --- a/rtl/mini/mk/formal.mk +++ b/rtl/mini/mk/formal.mk @@ -6,7 +6,7 @@ FORMAL_SOLVER_DIR := $(FORMAL_DIR)/bin FORMAL_SOLVER_WRAPPER := $(FORMAL_SOLVER_DIR)/bitwuzla FORMAL_DEPTH ?= 20 FORMAL_TIMEOUT ?= 60 -FORMAL_TARGETS := bus rib_adapter ribp2apb sysctrl pll_rcu gpio_user +FORMAL_TARGETS := bus rib_adapter rib2apb sysctrl pll_rcu gpio_user FORMAL_FILELIST_GENERATOR := $(RTL_PATH)/formal/generate_formal_filelist.py FORMAL_SBY_GENERATOR := $(RTL_PATH)/formal/generate_sby_config.py FORMAL_RESULT_GENERATOR := $(RTL_PATH)/formal/formal_results.py @@ -14,8 +14,8 @@ FORMAL_SOURCE_FILES := $(RTL_PATH)/formal/bus_formal.sv \ $(RTL_PATH)/formal/bus_formal_props.sv \ $(RTL_PATH)/formal/rib_adapter_formal.sv \ $(RTL_PATH)/formal/rib_adapter_formal_props.sv \ - $(RTL_PATH)/formal/ribp2apb_formal.sv \ - $(RTL_PATH)/formal/ribp2apb_formal_props.sv \ + $(RTL_PATH)/formal/rib2apb_formal.sv \ + $(RTL_PATH)/formal/rib2apb_formal_props.sv \ $(RTL_PATH)/formal/sysctrl_formal.sv \ $(RTL_PATH)/formal/sysctrl_formal_props.sv \ $(RTL_PATH)/formal/pll_rcu_formal.sv \ @@ -27,8 +27,8 @@ FORMAL_SOURCE_FILES := $(RTL_PATH)/formal/bus_formal.sv \ $(RTL_PATH)/top/rib_if.sv \ $(RTL_PATH)/top/rib2ram.sv \ $(RTL_PATH)/top/rib2ribp.sv \ + $(RTL_PATH)/top/rib2apb.sv \ $(RTL_PATH)/top/ribp2rib.sv \ - $(ROOT_PATH)/rtl/ip/ribp/interconnect/ribp2apb.sv \ $(ROOT_PATH)/rtl/ip/ribp/interconnect/ribp_regslice.sv \ $(ROOT_PATH)/rtl/ip/ribp/peripheral/gpio.sv \ $(ROOT_PATH)/rtl/ip/ribp/peripheral/pll_ctrl_if.sv \ @@ -117,7 +117,7 @@ formal-bus: $(FORMAL_DIR)/bus/.stamp | manifest formal-rib-adapter: $(FORMAL_DIR)/rib_adapter/.stamp | manifest -formal-ribp2apb: $(FORMAL_DIR)/ribp2apb/.stamp | manifest +formal-rib2apb: $(FORMAL_DIR)/rib2apb/.stamp | manifest formal-sysctrl: $(FORMAL_DIR)/sysctrl/.stamp | manifest @@ -131,4 +131,4 @@ formal-doctor: formal-clean: python3 $(ROOT_PATH)/scripts/clean.py --root $(ROOT_PATH) --path $(FORMAL_DIR) -.PHONY: formal formal-bus formal-rib-adapter formal-ribp2apb formal-sysctrl formal-pll-rcu formal-gpio-user formal-doctor formal-clean \ No newline at end of file +.PHONY: formal formal-bus formal-rib-adapter formal-rib2apb formal-sysctrl formal-pll-rcu formal-gpio-user formal-doctor formal-clean diff --git a/rtl/mini/top/bus.sv b/rtl/mini/top/bus.sv index 0d1fc945..1c38bb73 100644 --- a/rtl/mini/top/bus.sv +++ b/rtl/mini/top/bus.sv @@ -18,13 +18,13 @@ module bus ( `ifdef HAVE_SRAM_IF ram_if.master ram, `endif - ribp_if.slave mgmt_ribp, - rib_if.slave user_rib, - rib_if.slave dma_rib, + ribp_if.slave mgmt_ribp, + rib_if.slave user_rib, + rib_if.slave dma_rib, input logic user_bus_enable_i, output logic user_bus_idle_o, - rib_if.master rib, - ribp_if.master apb_ribp, + rib_if.master rib, + rib_if.master apb_rib, input logic perf_enable_i, input logic perf_clear_i, output logic fault_valid_o, @@ -56,7 +56,6 @@ module bus ( rib_if u_mgmt_rib_if (); rib_if u_mstr_rib_if (); - rib_if u_apb_rib_if (); rib_if u_ram_rib_if (); rib_if u_fault_rib_if (); @@ -97,13 +96,6 @@ module bus ( .rib (u_mgmt_rib_if) ); - rib2ribp u_apb_rib2ribp ( - .clk_i (clk_i), - .rst_n_i(rst_n_i), - .rib (u_apb_rib_if), - .ribp (apb_ribp) - ); - rib_error_slave u_fault_slave ( .clk_i (clk_i), .rst_n_i (rst_n_i), @@ -368,10 +360,10 @@ module bus ( assign rib.cmd_addr = u_mstr_rib_if.cmd_addr; assign rib.cmd_write = u_mstr_rib_if.cmd_write; assign rib.cmd_len = u_mstr_rib_if.cmd_len; - assign u_apb_rib_if.cmd_valid = s_apb_sel; - assign u_apb_rib_if.cmd_addr = u_mstr_rib_if.cmd_addr; - assign u_apb_rib_if.cmd_write = u_mstr_rib_if.cmd_write; - assign u_apb_rib_if.cmd_len = u_mstr_rib_if.cmd_len; + assign apb_rib.cmd_valid = s_apb_sel; + assign apb_rib.cmd_addr = u_mstr_rib_if.cmd_addr; + assign apb_rib.cmd_write = u_mstr_rib_if.cmd_write; + assign apb_rib.cmd_len = u_mstr_rib_if.cmd_len; assign u_ram_rib_if.cmd_valid = s_ram_sel; assign u_ram_rib_if.cmd_addr = u_mstr_rib_if.cmd_addr; assign u_ram_rib_if.cmd_write = u_mstr_rib_if.cmd_write; @@ -386,7 +378,7 @@ module bus ( if (s_ribp_sel) begin u_mstr_rib_if.cmd_ready = rib.cmd_ready; end else if (s_apb_sel) begin - u_mstr_rib_if.cmd_ready = u_apb_rib_if.cmd_ready; + u_mstr_rib_if.cmd_ready = apb_rib.cmd_ready; end else if (s_ram_sel) begin u_mstr_rib_if.cmd_ready = u_ram_rib_if.cmd_ready; end else if (s_fault_sel) begin @@ -424,15 +416,13 @@ module bus ( assign rib.rsp_ready = s_mstr_lock_q && s_cmd_accepted_q && (s_target_q == TARGET_RIBP) ? u_mstr_rib_if.rsp_ready : 1'b0; - assign u_apb_rib_if.w_valid = s_mstr_lock_q && s_cmd_accepted_q && - (s_target_q == TARGET_APB) ? - u_mstr_rib_if.w_valid : 1'b0; - assign u_apb_rib_if.wdata = u_mstr_rib_if.wdata; - assign u_apb_rib_if.wstrb = u_mstr_rib_if.wstrb; - assign u_apb_rib_if.wlast = u_mstr_rib_if.wlast; - assign u_apb_rib_if.rsp_ready = s_mstr_lock_q && s_cmd_accepted_q && - (s_target_q == TARGET_APB) ? - u_mstr_rib_if.rsp_ready : 1'b0; + assign apb_rib.w_valid = s_mstr_lock_q && s_cmd_accepted_q && + (s_target_q == TARGET_APB) ? u_mstr_rib_if.w_valid : 1'b0; + assign apb_rib.wdata = u_mstr_rib_if.wdata; + assign apb_rib.wstrb = u_mstr_rib_if.wstrb; + assign apb_rib.wlast = u_mstr_rib_if.wlast; + assign apb_rib.rsp_ready = s_mstr_lock_q && s_cmd_accepted_q && + (s_target_q == TARGET_APB) ? u_mstr_rib_if.rsp_ready : 1'b0; assign u_ram_rib_if.w_valid = s_mstr_lock_q && s_cmd_accepted_q && (s_target_q == TARGET_RAM) ? @@ -473,13 +463,13 @@ module bus ( u_mstr_rib_if.rsp_last = rib.rsp_last; end TARGET_APB: begin - u_mstr_rib_if.w_ready = s_cmd_accepted_q && u_apb_rib_if.w_ready; - u_mstr_rib_if.rsp_valid = s_cmd_accepted_q && u_apb_rib_if.rsp_valid; - u_mstr_rib_if.rdata = u_apb_rib_if.rdata; - u_mstr_rib_if.resp_err = u_apb_rib_if.resp_err; - u_mstr_rib_if.resp_code = u_apb_rib_if.resp_code; - u_mstr_rib_if.rsp_beat = u_apb_rib_if.rsp_beat; - u_mstr_rib_if.rsp_last = u_apb_rib_if.rsp_last; + u_mstr_rib_if.w_ready = s_cmd_accepted_q && apb_rib.w_ready; + u_mstr_rib_if.rsp_valid = s_cmd_accepted_q && apb_rib.rsp_valid; + u_mstr_rib_if.rdata = apb_rib.rdata; + u_mstr_rib_if.resp_err = apb_rib.resp_err; + u_mstr_rib_if.resp_code = apb_rib.resp_code; + u_mstr_rib_if.rsp_beat = apb_rib.rsp_beat; + u_mstr_rib_if.rsp_last = apb_rib.rsp_last; end TARGET_RAM: begin u_mstr_rib_if.w_ready = s_cmd_accepted_q && u_ram_rib_if.w_ready; diff --git a/rtl/mini/top/ip_apb_wrapper.sv b/rtl/mini/top/ip_apb_wrapper.sv index 72cdabf8..115b78a9 100644 --- a/rtl/mini/top/ip_apb_wrapper.sv +++ b/rtl/mini/top/ip_apb_wrapper.sv @@ -22,7 +22,7 @@ module ip_apb_wrapper ( input logic clk_aud_i, input logic rst_aud_n_i, input logic tmr_capch_i, - ribp_if.slave ribp, + rib_if.slave rib, uart_if.dut uart, pwm_if.dut pwm, ps2_if.dut ps2, @@ -62,10 +62,10 @@ module ip_apb_wrapper ( // Generated IRQ ownership and core-vector bit assignments are topology checked. `include "soc_apb_irq_bindings.svh" -ribp2apb u_ribp2apb ( + rib2apb u_rib2apb ( .clk_i (clk_i), .rst_n_i(rst_n_i), - .ribp (ribp), + .rib (rib), `include "soc_apb_connections.svh" ); diff --git a/rtl/mini/top/rib2apb.sv b/rtl/mini/top/rib2apb.sv new file mode 100644 index 00000000..c47996cd --- /dev/null +++ b/rtl/mini/top/rib2apb.sv @@ -0,0 +1,177 @@ +// Copyright (c) 2026 Yuchi Miao +// retroSoC is licensed under Mulan PSL v2. +// You can use this software according to the terms and conditions of the Mulan PSL v2. +// You may obtain a copy of the Mulan PSL v2 at: +// http://license.coscl.org.cn/MulanPSL2 +// THIS SOFTWARE IS PROVIDED ON AN "AS IS" BASIS, WITHOUT WARRANTIES OF ANY KIND, +// EITHER EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO NON-INFRINGEMENT, +// MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE. +// See the Mulan PSL v2 for more details. + +`include "mmap_define.svh" +`include "rib_defs.svh" + +module rib2apb ( + // verilog_format: off + input logic clk_i, + input logic rst_n_i, + rib_if.slave rib, +`include "soc_apb_ports.svh" + // verilog_format: on +); + + localparam logic [2:0] FSM_CMD = 3'd0; + localparam logic [2:0] FSM_WDATA = 3'd1; + localparam logic [2:0] FSM_SETP = 3'd2; + localparam logic [2:0] FSM_ENAB = 3'd3; + localparam logic [2:0] FSM_DROP_WDATA = 3'd4; + localparam logic [2:0] FSM_ERR = 3'd5; + localparam int RSP_WIDTH = 39; + + logic [31:0] s_rd_data; + logic s_xfer_valid, s_xfer_ready, s_xfer_error; + logic [2:0] s_fsm_d, s_fsm_q; + logic [31:0] s_addr_q, s_wdata_q; + logic [3:0] s_wstrb_q; + logic s_write_q; + logic [2:0] s_error_code_d, s_error_code_q; + logic s_cmd_hdshk, s_w_hdshk, s_rsp_hdshk; + logic s_psel_valid; + logic s_rsp_input_valid, s_rsp_input_ready; + logic [RSP_WIDTH-1:0] s_rsp_input_data, s_rsp_output_data; + + // Registered slave-select one-hot and APB response mux. + `include "soc_apb_declarations.svh" + + assign s_cmd_hdshk = rib.cmd_valid && rib.cmd_ready; + assign s_w_hdshk = rib.w_valid && rib.w_ready; + + assign rib.cmd_ready = (s_fsm_q == FSM_CMD) && !rib.rsp_valid; + assign rib.w_ready = (s_fsm_q == FSM_WDATA) || (s_fsm_q == FSM_DROP_WDATA); + + assign s_xfer_valid = (s_fsm_q == FSM_SETP) || (s_fsm_q == FSM_ENAB); + + // Generated APB routing uses the latched RIB request and selected target. + `include "soc_apb_request_routes.svh" + `include "soc_apb_select_routes.svh" + `include "soc_apb_response_mux.svh" + + assign s_psel_valid = |s_psel_comb; + + assign s_rsp_input_valid = ((s_fsm_q == FSM_ENAB) && s_xfer_ready) || (s_fsm_q == FSM_ERR); + assign s_rsp_input_data = (s_fsm_q == FSM_ENAB) ? + {1'b1, 2'd0, s_xfer_error ? `RIB_RESP_SLVERR : `RIB_RESP_OK, s_xfer_error, + s_write_q ? 32'd0 : s_rd_data} : + {1'b1, 2'd0, s_error_code_q, 1'b1, 32'd0}; + assign s_rsp_hdshk = s_rsp_input_valid && s_rsp_input_ready; + + spill_register #( + .DATA_WIDTH(RSP_WIDTH), + .BYPASS (1'b0) + ) u_rsp_spill_register ( + .clk_i (clk_i), + .rst_n_i(rst_n_i), + .flush_i(1'b0), + .valid_i(s_rsp_input_valid), + .ready_o(s_rsp_input_ready), + .data_i (s_rsp_input_data), + .valid_o(rib.rsp_valid), + .ready_i(rib.rsp_ready), + .data_o (s_rsp_output_data) + ); + + assign rib.rdata = s_rsp_output_data[31:0]; + assign rib.resp_err = s_rsp_output_data[32]; + assign rib.resp_code = s_rsp_output_data[35:33]; + assign rib.rsp_beat = s_rsp_output_data[37:36]; + assign rib.rsp_last = s_rsp_output_data[38]; + + always_comb begin + s_fsm_d = s_fsm_q; + s_error_code_d = s_error_code_q; + unique case (s_fsm_q) + FSM_CMD: begin + if (s_cmd_hdshk) begin + if (rib.cmd_len != `RIB_LEN_INCR1) begin + s_error_code_d = `RIB_RESP_BURSTERR; + s_fsm_d = rib.cmd_write ? FSM_DROP_WDATA : FSM_ERR; + end else if (!s_psel_valid) begin + s_error_code_d = `RIB_RESP_DECERR; + s_fsm_d = rib.cmd_write ? FSM_DROP_WDATA : FSM_ERR; + end else begin + s_fsm_d = rib.cmd_write ? FSM_WDATA : FSM_SETP; + end + end + end + FSM_WDATA: begin + if (s_w_hdshk) begin + if (rib.wlast) begin + s_fsm_d = FSM_SETP; + end else begin + s_error_code_d = `RIB_RESP_BURSTERR; + s_fsm_d = FSM_ERR; + end + end + end + FSM_SETP: s_fsm_d = FSM_ENAB; + FSM_ENAB: begin + if (s_xfer_ready && s_rsp_input_ready) s_fsm_d = FSM_CMD; + end + FSM_DROP_WDATA: begin + if (s_w_hdshk && rib.wlast) s_fsm_d = FSM_ERR; + end + FSM_ERR: begin + if (s_rsp_hdshk) s_fsm_d = FSM_CMD; + end + default: s_fsm_d = FSM_CMD; + endcase + end + + dffr #(3) u_fsm_dffr ( + clk_i, + rst_n_i, + s_fsm_d, + s_fsm_q + ); + dffer #(32) u_addr_dffer ( + clk_i, + rst_n_i, + s_cmd_hdshk, + rib.cmd_addr, + s_addr_q + ); + dffer #(1) u_write_dffer ( + clk_i, + rst_n_i, + s_cmd_hdshk, + rib.cmd_write, + s_write_q + ); + dffer #(32) u_wdata_dffer ( + clk_i, + rst_n_i, + s_w_hdshk && (s_fsm_q == FSM_WDATA), + rib.wdata, + s_wdata_q + ); + dffer #(4) u_wstrb_dffer ( + clk_i, + rst_n_i, + s_w_hdshk && (s_fsm_q == FSM_WDATA), + rib.wstrb, + s_wstrb_q + ); + dffr #(3) u_error_code_dffr ( + clk_i, + rst_n_i, + s_error_code_d, + s_error_code_q + ); + dffr #(NSLV) u_psel_dffr ( + clk_i, + rst_n_i, + s_cmd_hdshk ? s_psel_comb : s_psel_q, + s_psel_q + ); + +endmodule diff --git a/tests/rtl/bus_fault_tb.sv b/tests/rtl/bus_fault_tb.sv index b1e218d5..0cb748e7 100644 --- a/tests/rtl/bus_fault_tb.sv +++ b/tests/rtl/bus_fault_tb.sv @@ -15,20 +15,26 @@ module bus_fault_tb; rib_if user_rib (); rib_if dma_rib (); rib_if rib (); - ribp_if apb_ribp (); + rib_if apb_rib (); always #5 clk_i = ~clk_i; - assign rib.cmd_ready = 1'b1; - assign rib.w_ready = 1'b1; - assign rib.rsp_valid = 1'b0; - assign rib.rdata = 32'hCAFE_BABE; - assign rib.resp_err = 1'b0; - assign rib.resp_code = `RIB_RESP_OK; - assign rib.rsp_beat = '0; - assign rib.rsp_last = 1'b0; - assign apb_ribp.ready = 1'b1; - assign apb_ribp.rdata = 32'h1234_5678; + assign rib.cmd_ready = 1'b1; + assign rib.w_ready = 1'b1; + assign rib.rsp_valid = 1'b0; + assign rib.rdata = 32'hCAFE_BABE; + assign rib.resp_err = 1'b0; + assign rib.resp_code = `RIB_RESP_OK; + assign rib.rsp_beat = '0; + assign rib.rsp_last = 1'b0; + assign apb_rib.cmd_ready = 1'b1; + assign apb_rib.w_ready = 1'b1; + assign apb_rib.rsp_valid = 1'b0; + assign apb_rib.rdata = 32'h1234_5678; + assign apb_rib.resp_err = 1'b0; + assign apb_rib.resp_code = `RIB_RESP_OK; + assign apb_rib.rsp_beat = '0; + assign apb_rib.rsp_last = 1'b1; bus u_bus ( .clk_i (clk_i), @@ -39,7 +45,7 @@ module bus_fault_tb; .user_bus_enable_i(1'b1), .user_bus_idle_o (user_bus_idle_o), .rib (rib), - .apb_ribp (apb_ribp), + .apb_rib (apb_rib), .perf_enable_i (1'b0), .perf_clear_i (1'b0), .fault_valid_o (fault_valid_o), @@ -62,7 +68,7 @@ module bus_fault_tb; while (!fault_valid_o) @(posedge clk_i); if (fault_addr_o !== address || fault_wstrb_o !== write_strobes || fault_reserved_o !== reserved || fault_access_o || fault_code_o !== expected_code || - rib.cmd_valid || apb_ribp.valid) begin + rib.cmd_valid || apb_rib.cmd_valid) begin $fatal(1, "unexpected fault response for address %h", address); end while (!mgmt_ribp.ready) @(posedge clk_i); @@ -95,7 +101,7 @@ module bus_fault_tb; user_rib.w_valid = 1'b0; end while (!fault_valid_o) @(posedge clk_i); - if (!fault_access_o || fault_master_o != 2'd1 || rib.cmd_valid || apb_ribp.valid) begin + if (!fault_access_o || fault_master_o != 2'd1 || rib.cmd_valid || apb_rib.cmd_valid) begin $fatal(1, "user access was not denied locally"); end if (user_rib.rdata !== 32'd0 || !user_rib.resp_err || !user_rib.rsp_last || diff --git a/tests/rtl/rib2apb_tb.sv b/tests/rtl/rib2apb_tb.sv new file mode 100644 index 00000000..4aadf95e --- /dev/null +++ b/tests/rtl/rib2apb_tb.sv @@ -0,0 +1,197 @@ +`timescale 1ns / 1ps + +`include "rib_defs.svh" + +module rib2apb_tb; + logic clk_i = 1'b0; + logic rst_n_i = 1'b0; + logic rng_ready = 1'b0; + logic rng_slverr = 1'b0; + logic [31:0] rng_rdata = 32'h1234_5678; + + rib_if rib (); + apb4_pure_if archinfo (); + apb4_pure_if rng (); + apb4_pure_if uart (); + apb4_pure_if pwm (); + apb4_pure_if ps2 (); + apb4_pure_if rtc (); + apb4_pure_if wdg (); + apb4_pure_if crc (); + apb4_pure_if tmr (); + apb4_pure_if user_ip (); + + always #5 clk_i = ~clk_i; + + assign archinfo.pready = 1'b0; + assign archinfo.prdata = '0; + assign archinfo.pslverr = 1'b0; + assign rng.pready = rng_ready; + assign rng.prdata = rng_rdata; + assign rng.pslverr = rng_slverr; + assign uart.pready = 1'b0; + assign uart.prdata = '0; + assign uart.pslverr = 1'b0; + assign pwm.pready = 1'b0; + assign pwm.prdata = '0; + assign pwm.pslverr = 1'b0; + assign ps2.pready = 1'b0; + assign ps2.prdata = '0; + assign ps2.pslverr = 1'b0; + assign rtc.pready = 1'b0; + assign rtc.prdata = '0; + assign rtc.pslverr = 1'b0; + assign wdg.pready = 1'b0; + assign wdg.prdata = '0; + assign wdg.pslverr = 1'b0; + assign crc.pready = 1'b0; + assign crc.prdata = '0; + assign crc.pslverr = 1'b0; + assign tmr.pready = 1'b0; + assign tmr.prdata = '0; + assign tmr.pslverr = 1'b0; + assign user_ip.pready = 1'b0; + assign user_ip.prdata = '0; + assign user_ip.pslverr = 1'b0; + + rib2apb u_rib2apb ( + .clk_i (clk_i), + .rst_n_i (rst_n_i), + .rib (rib), + .archinfo(archinfo), + .rng (rng), + .uart (uart), + .pwm (pwm), + .ps2 (ps2), + .rtc (rtc), + .wdg (wdg), + .crc (crc), + .tmr (tmr), + .user_ip (user_ip) + ); + + task automatic send_command(input logic [31:0] address, input logic write, + input logic [1:0] length); + begin + @(negedge clk_i); + rib.cmd_addr = address; + rib.cmd_write = write; + rib.cmd_len = length; + rib.cmd_valid = 1'b1; + while (!rib.cmd_ready) @(posedge clk_i); + @(negedge clk_i); + rib.cmd_valid = 1'b0; + end + endtask + + task automatic send_write(input logic [31:0] data, input logic [3:0] strobes, input logic last); + begin + @(negedge clk_i); + rib.wdata = data; + rib.wstrb = strobes; + rib.wlast = last; + rib.w_valid = 1'b1; + while (!rib.w_ready) @(posedge clk_i); + @(negedge clk_i); + rib.w_valid = 1'b0; + end + endtask + + task automatic wait_for_rng_enable; + begin + while (!(rng.psel && rng.penable)) @(posedge clk_i); + end + endtask + + task automatic expect_response(input logic expected_error, input logic [2:0] expected_code, + input logic [31:0] expected_data); + begin + while (!rib.rsp_valid) @(posedge clk_i); + #1; + if (rib.resp_err !== expected_error || rib.resp_code !== expected_code || + rib.rdata !== expected_data || rib.rsp_beat !== 2'd0 || !rib.rsp_last) begin + $fatal(1, "unexpected RIB response error=%b/%b code=%0d/%0d data=%h/%h fsm=%0d", + rib.resp_err, expected_error, rib.resp_code, expected_code, rib.rdata, + expected_data, u_rib2apb.s_fsm_q); + end + end + endtask + + initial begin + rib.cmd_valid = 1'b0; + rib.cmd_addr = '0; + rib.cmd_write = 1'b0; + rib.cmd_len = `RIB_LEN_INCR1; + rib.w_valid = 1'b0; + rib.wdata = '0; + rib.wstrb = '0; + rib.wlast = 1'b0; + rib.rsp_ready = 1'b1; + + repeat (2) @(posedge clk_i); + rst_n_i = 1'b1; + + send_command(32'h2000_1000, 1'b0, `RIB_LEN_INCR1); + while (!(rng.psel && !rng.penable)) @(posedge clk_i); + wait_for_rng_enable(); + if (rng.paddr !== 32'h2000_1000 || rng.pwrite || rng.pstrb !== 4'd0) begin + $fatal(1, "read APB setup was not held from the RIB command"); + end + repeat (2) begin + @(posedge clk_i); + if (!(rng.psel && rng.penable) || rng.paddr !== 32'h2000_1000) begin + $fatal(1, "APB read request changed while PREADY was low"); + end + end + rib.rsp_ready = 1'b0; + @(negedge clk_i); + rng_ready = 1'b1; + expect_response(1'b0, `RIB_RESP_OK, 32'h1234_5678); + repeat (2) begin + @(posedge clk_i); + if (!rib.rsp_valid || rib.rdata !== 32'h1234_5678) begin + $fatal(1, "response did not remain stable under RIB backpressure"); + end + end + rib.rsp_ready = 1'b1; + @(posedge clk_i); + @(negedge clk_i); + rng_ready = 1'b0; + + send_command(32'h2000_1000, 1'b1, `RIB_LEN_INCR1); + send_write(32'hA5A5_5A5A, 4'hC, 1'b1); + wait_for_rng_enable(); + if (!rng.pwrite || rng.pwdata !== 32'hA5A5_5A5A || rng.pstrb !== 4'hC) begin + $fatal(1, "APB write data was not held from the RIB write channel"); + end + @(negedge clk_i); + rng_ready = 1'b1; + expect_response(1'b0, `RIB_RESP_OK, 32'd0); + @(posedge clk_i); + @(negedge clk_i); + rng_ready = 1'b0; + + rng_slverr = 1'b1; + send_command(32'h2000_1000, 1'b0, `RIB_LEN_INCR1); + wait_for_rng_enable(); + @(negedge clk_i); + rng_ready = 1'b1; + expect_response(1'b1, `RIB_RESP_SLVERR, 32'h1234_5678); + @(posedge clk_i); + @(negedge clk_i); + rng_ready = 1'b0; + rng_slverr = 1'b0; + + send_command(32'h2000_1000, 1'b1, `RIB_LEN_INCR4); + send_write(32'h0000_0001, 4'hF, 1'b0); + send_write(32'h0000_0002, 4'hF, 1'b0); + send_write(32'h0000_0003, 4'hF, 1'b0); + send_write(32'h0000_0004, 4'hF, 1'b1); + if (rng.psel) $fatal(1, "illegal RIB burst reached the APB target"); + expect_response(1'b1, `RIB_RESP_BURSTERR, 32'd0); + @(posedge clk_i); + + $display("RIB2APB direct bridge test passed"); + $finish; + end +endmodule diff --git a/tests/rtl/rib_bus_tb.sv b/tests/rtl/rib_bus_tb.sv index 911c72be..ded6e58c 100644 --- a/tests/rtl/rib_bus_tb.sv +++ b/tests/rtl/rib_bus_tb.sv @@ -20,7 +20,7 @@ module rib_bus_tb; rib_if user_rib (); rib_if dma_rib (); rib_if rib (); - ribp_if apb_ribp (); + rib_if apb_rib (); always #5 clk_i = ~clk_i; always @(posedge clk_i) cycle_count <= cycle_count + 1; @@ -57,8 +57,14 @@ module rib_bus_tb; end end - assign apb_ribp.ready = apb_ribp.valid; - assign apb_ribp.rdata = 32'h1234_5678; + assign apb_rib.cmd_ready = 1'b1; + assign apb_rib.w_ready = 1'b1; + assign apb_rib.rsp_valid = 1'b0; + assign apb_rib.rdata = 32'h1234_5678; + assign apb_rib.resp_err = 1'b0; + assign apb_rib.resp_code = `RIB_RESP_OK; + assign apb_rib.rsp_beat = '0; + assign apb_rib.rsp_last = 1'b1; bus u_bus ( .clk_i (clk_i), @@ -69,7 +75,7 @@ module rib_bus_tb; .user_bus_enable_i(1'b1), .user_bus_idle_o (user_bus_idle_o), .rib (rib), - .apb_ribp (apb_ribp), + .apb_rib (apb_rib), .perf_enable_i (1'b0), .perf_clear_i (1'b0), .fault_valid_o (fault_valid_o), @@ -163,7 +169,7 @@ module rib_bus_tb; issue_read(32'h1000_0000, `RIB_LEN_INCR4, 1'b1); issue_read(32'h2000_0000, `RIB_LEN_INCR4, 1'b1); issue_read(32'h3800_1000, 2'd2, 1'b1); - if (rib_command_count != 1 || apb_ribp.valid) begin + if (rib_command_count != 1 || apb_rib.cmd_valid) begin $fatal(1, "illegal burst reached a downstream target"); end diff --git a/tests/test_rib2apb.py b/tests/test_rib2apb.py new file mode 100644 index 00000000..eb1ca1a6 --- /dev/null +++ b/tests/test_rib2apb.py @@ -0,0 +1,89 @@ +"""RTL test for the direct RIB-to-APB bridge.""" + +from __future__ import annotations + +import shutil +import subprocess +import sys +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[1] + + +def test_rib2apb_preserves_apb_and_rib_handshakes(tmp_path: Path) -> None: + iverilog = shutil.which("iverilog") + sv2v = shutil.which("sv2v") + vvp = shutil.which("vvp") + if iverilog is None or sv2v is None or vvp is None: + return + + memory_map = tmp_path / "memory_map" + topology = tmp_path / "soc_topology" + subprocess.run( + [ + sys.executable, + str(ROOT / "rtl/mini/address_map/generate_memory_map.py"), + "--map", + str(ROOT / "rtl/mini/address_map/memory_map.json"), + "--output-dir", + str(memory_map), + "--have-sram-if", + "NO", + ], + check=True, + ) + subprocess.run( + [ + sys.executable, + str(ROOT / "rtl/mini/integration/generate_soc_topology.py"), + "--map", + str(ROOT / "rtl/mini/integration/soc_topology.json"), + "--memory-map", + str(ROOT / "rtl/mini/address_map/memory_map.json"), + "--output-dir", + str(topology), + ], + check=True, + ) + + source_list = tmp_path / "rib2apb.fl" + source_list.write_text( + "\n".join( + [ + "+define+SV_ASSRT_DISABLE", + f"+incdir+{memory_map / 'rtl'}", + f"+incdir+{topology / 'rtl'}", + f"+incdir+{ROOT / 'rtl/mini/top'}", + f"+incdir+{ROOT / 'rtl/managed/clusterip/common/rtl'}", + str(ROOT / "rtl/managed/clusterip/common/rtl/interface/apb4_pure_if.sv"), + str(ROOT / "rtl/managed/clusterip/common/rtl/utils/register.sv"), + str(ROOT / "rtl/managed/clusterip/common/rtl/utils/spill_register.sv"), + str(ROOT / "rtl/mini/top/rib_if.sv"), + str(ROOT / "rtl/mini/top/rib2apb.sv"), + str(ROOT / "tests/rtl/rib2apb_tb.sv"), + "", + ] + ), + encoding="utf-8", + ) + converted = tmp_path / "rib2apb_tb.v" + subprocess.run( + [ + sys.executable, + str(ROOT / "rtl/mini/script/convt_sv2v.py"), + "-f", + str(source_list), + "--output", + str(converted), + ], + check=True, + ) + simulation = tmp_path / "rib2apb_tb" + subprocess.run( + [iverilog, "-g2012", "-s", "rib2apb_tb", "-o", str(simulation), str(converted)], + check=True, + ) + result = subprocess.run([vvp, str(simulation)], text=True, capture_output=True, check=True) + + assert "RIB2APB direct bridge test passed" in result.stdout diff --git a/tests/test_script_tools.py b/tests/test_script_tools.py index d171bb25..e789272c 100644 --- a/tests/test_script_tools.py +++ b/tests/test_script_tools.py @@ -181,7 +181,7 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non bus_filelist = tmp_path / "bus.fl" rib_adapter_filelist = tmp_path / "rib_adapter.fl" - rib2apb_filelist = tmp_path / "ribp2apb.fl" + rib2apb_filelist = tmp_path / "rib2apb.fl" sysctrl_filelist = tmp_path / "sysctrl.fl" pll_rcu_filelist = tmp_path / "pll_rcu.fl" gpio_user_filelist = tmp_path / "gpio_user.fl" @@ -190,7 +190,7 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non "rib_adapter", rib_adapter_filelist, memory_map, topology, user_extensions ) assert generate_formal_filelist( - "ribp2apb", rib2apb_filelist, memory_map, topology, user_extensions + "rib2apb", rib2apb_filelist, memory_map, topology, user_extensions ) assert generate_formal_filelist( "sysctrl", sysctrl_filelist, memory_map, topology, user_extensions @@ -204,7 +204,7 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non bus = parse_filelists([bus_filelist], require_files=False) rib_adapter = parse_filelists([rib_adapter_filelist], require_files=False) - ribp2apb = parse_filelists([rib2apb_filelist], require_files=False) + rib2apb = parse_filelists([rib2apb_filelist], require_files=False) sysctrl = parse_filelists([sysctrl_filelist], require_files=False) pll_rcu = parse_filelists([pll_rcu_filelist], require_files=False) gpio_user = parse_filelists([gpio_user_filelist], require_files=False) @@ -216,9 +216,9 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non assert ROOT / "rtl/mini/formal/bus_formal.sv" in bus.files assert ROOT / "rtl/mini/top/rib2ribp.sv" in rib_adapter.files assert ROOT / "rtl/mini/formal/rib_adapter_formal.sv" in rib_adapter.files - assert ROOT / "rtl/ip/ribp/interconnect/ribp2apb.sv" in ribp2apb.files - assert ROOT / "rtl/mini/formal/ribp2apb_formal.sv" in ribp2apb.files - assert ROOT / "rtl/managed/clusterip/common/rtl/interface/apb4_pure_if.sv" in ribp2apb.files + assert ROOT / "rtl/mini/top/rib2apb.sv" in rib2apb.files + assert ROOT / "rtl/mini/formal/rib2apb_formal.sv" in rib2apb.files + assert ROOT / "rtl/managed/clusterip/common/rtl/interface/apb4_pure_if.sv" in rib2apb.files assert ROOT / "rtl/ip/ribp/peripheral/sysctrl.sv" in sysctrl.files assert ROOT / "rtl/mini/formal/sysctrl_formal.sv" in sysctrl.files assert ROOT / "rtl/mini/top/rcu.sv" in pll_rcu.files @@ -270,7 +270,7 @@ def test_fatfs_release_script_uses_the_locked_archive_contract() -> None: def test_formal_result_summary_requires_every_passing_step(tmp_path: Path) -> None: - proofs = ("bus", "ribp2apb", "sysctrl", "pll_rcu", "gpio_user") + proofs = ("bus", "rib2apb", "sysctrl", "pll_rcu", "gpio_user") for proof in proofs: directory = tmp_path / proof directory.mkdir() @@ -292,7 +292,7 @@ def test_formal_result_summary_requires_every_passing_step(tmp_path: Path) -> No "--proof", f"bus={tmp_path / 'bus'}", "--proof", - f"ribp2apb={tmp_path / 'ribp2apb'}", + f"rib2apb={tmp_path / 'rib2apb'}", "--proof", f"sysctrl={tmp_path / 'sysctrl'}", "--proof", diff --git a/tests/test_soc_topology.py b/tests/test_soc_topology.py index 70deb1ca..84c545cf 100644 --- a/tests/test_soc_topology.py +++ b/tests/test_soc_topology.py @@ -86,14 +86,14 @@ def test_topology_generates_complete_rib_apb_and_gpio_bindings(tmp_path: Path) - assert "assign u_gpio_if.alt1_do_i[22] = u_psram_if.nss_o[0];" in gpio assert apb_interfaces.count("apb4_if u_") == 10 assert "apb4_pure_if u_archinfo_apb_pure_if ();" in apb_interfaces - assert "assign tmr.paddr = ribp.addr;" in apb_routes + assert "assign tmr.paddr = s_addr_q;" in apb_routes assert "({32{s_psel_q[8]}} & tmr.prdata)" in apb_response assert "localparam int NSLV = 10;" in apb_declarations - assert fabric.count("ribp_if u_") == 2 - assert fabric.count("rib_if u_") == 3 + assert fabric.count("ribp_if u_") == 1 + assert fabric.count("rib_if u_") == 4 assert ".mgmt_ribp(u_mgmt_ribp_if)" in bus_fabric assert ".user_rib(u_user_rib_if)" in bus_fabric - assert ".apb_ribp(u_apb_ribp_if)" in bus_fabric + assert ".apb_rib(u_apb_rib_if)" in bus_fabric assert ".rib(u_rib_if)" in bus_fabric assert "`define SOC_IRQ_VECTOR_WIDTH 32" in irq_config assert "`define SOC_IRQ_RIBP_WIDTH 10" in irq_config @@ -147,8 +147,8 @@ def test_topology_always_adds_the_user_apb_target(tmp_path: Path) -> None: interfaces = (tmp_path / "rtl/soc_apb_interfaces.svh").read_text(encoding="utf-8") declarations = (tmp_path / "rtl/soc_apb_declarations.svh").read_text(encoding="utf-8") response = (tmp_path / "rtl/soc_apb_response_mux.svh").read_text(encoding="utf-8") - formal_design = (ROOT / "rtl/mini/formal/ribp2apb_formal.sv").read_text(encoding="utf-8") - formal_properties = (ROOT / "rtl/mini/formal/ribp2apb_formal_props.sv").read_text( + formal_design = (ROOT / "rtl/mini/formal/rib2apb_formal.sv").read_text(encoding="utf-8") + formal_properties = (ROOT / "rtl/mini/formal/rib2apb_formal_props.sv").read_text( encoding="utf-8" ) @@ -158,7 +158,7 @@ def test_topology_always_adds_the_user_apb_target(tmp_path: Path) -> None: assert "apb4_pure_if user_ip ();" in formal_design assert ".user_ip (user_ip)" in formal_design assert "logic [ 9:0] psel_comb" in formal_design - assert "wire [9:0] psel_comb" in formal_properties + assert "wire [ 9:0] psel_comb" in formal_properties def test_topology_rejects_unknown_or_non_rib_regions(tmp_path: Path) -> None: