admin/retroSoC
1
0 Fork 0
mirror of https://github.com/retroSoC/retroSoC.git synced 2026-11-04 22:32:36 +00:00
Code Issues Packages Projects Releases Wiki Activity

fix: update SDRAM simulation time and enhance test coverage for GA2D and SDRAM access

Browse Source
This commit is contained in:
maksyuki committed 2026-09-21 12:35:56 +08:00
1 parent 491d38fd0e
commit d544788ec9
7 files changed
+101 -84
Download Patch File Download Diff File Expand all files Collapse all files

No files matched your search

README.md
+8 -7
View File
@@ -112,10 +112,11 @@ fail-closed behavior, and test-status completion without the verbose startup
report. ARCHINFO checks include its
ABI and the build/configuration identifiers generated for that variant. The
IHP130 PR run links this image into the 32 KiB SRAM, explicitly enables the
fast-flash backend, and allows 360 seconds; Icarus keeps the real serial XPI
boot-model check. The profiles retain `bringup`
as their default for manual diagnostics. To run the full report in Verilator,
use:
fast-flash backend, and allows 600 seconds. GF180, ICS55, and SKY130 allow
1800 seconds because their smoke image and GA2D traffic share the SDRAM target.
Icarus keeps the real serial XPI boot-model check. The profiles retain
`bringup` as their default for manual diagnostics. To run the full report in
Verilator, use:
```sh
make CONFIG=configs/ci/ihp130.mk APP=bringup SIMU=VERILATOR SOC_SIM_TIME=300 firmware sim
@@ -216,9 +217,9 @@ analysis consume the Yosys netlist, so run the synthesis command first. The CI-p
regression uses the assembly self-test image:
Verilator simulations run for 180 seconds by default. The IHP130 `ci_smoke`
regression explicitly uses 360 seconds because its LP memory accesses traverse
the asynchronous data gateway. Set `SOC_SIM_TIME` explicitly only when an
exploratory local run needs a different limit.
regression explicitly uses 600 seconds. The GF180, ICS55, and SKY130
SDRAM-linked smoke runs use 1800 seconds. Set `SOC_SIM_TIME` explicitly only
when an exploratory local run needs a different limit.
VCS flow commands use `bsub -Is` by default: this includes parse-time Python helpers used to
calculate the variant and dependency-lock digest, generated-flow Python helpers, VCS, `simv`, and
app/apps/ci_smoke/main.c
+19 -11
View File
@@ -23,6 +23,9 @@
#include <retrosoc/lib/printf.h>
#include <retrosoc/service/test.h>
#define RS_CI_SMOKE_SDRAM_STACK_RESERVE_BYTES UINT32_C(65536)
#define RS_CI_SMOKE_SDRAM_SCRATCH_END (RS_SOC_SDRAM_END - RS_CI_SMOKE_SDRAM_STACK_RESERVE_BYTES)
static bool rs_ci_smoke_archinfo_v2(void) {
rs_archinfo_t info;
uint32_t device_id[4];
@@ -622,7 +625,7 @@ static bool rs_ci_smoke_ga2d_bounded_wait(void) {
const uint32_t rows = UINT32_C(256);
const uint32_t span = UINT32_C(18432);
volatile uint32_t *const destination =
(volatile uint32_t *)(uintptr_t)(RS_SOC_SDRAM_END - span - UINT32_C(15));
(volatile uint32_t *)(uintptr_t)(RS_CI_SMOKE_SDRAM_SCRATCH_END - span - UINT32_C(15));
const rs_ga2d_job_t job = {
.operation = RS_GA2D_OP_FILL,
.foreground = {0U, 0U, RS_GA2D_FORMAT_A8},
@@ -699,8 +702,9 @@ static bool rs_ci_smoke_ga2d_dma_contention(void) {
static const rs_dma_config_t dma_config = {
.kind = RS_DMA_KIND_MM_TO_MM,
.request = RS_DMA_REQUEST_SOFTWARE,
.source = RS_SOC_SDRAM_END - RS_CI_SMOKE_GA2D_DMA_WINDOW_BACK,
.destination = RS_SOC_SDRAM_END - RS_CI_SMOKE_GA2D_DMA_WINDOW_BACK + UINT32_C(0x100),
.source = RS_CI_SMOKE_SDRAM_SCRATCH_END - RS_CI_SMOKE_GA2D_DMA_WINDOW_BACK,
.destination =
RS_CI_SMOKE_SDRAM_SCRATCH_END - RS_CI_SMOKE_GA2D_DMA_WINDOW_BACK + UINT32_C(0x100),
.byte_count = RS_CI_SMOKE_GA2D_DMA_WORDS * UINT32_C(4),
.width = RS_DMA_WIDTH_32,
.source_increment = true,
@@ -710,10 +714,12 @@ static bool rs_ci_smoke_ga2d_dma_contention(void) {
};
static const rs_ga2d_job_t job = {
.operation = RS_GA2D_OP_COPY,
.foreground = {RS_SOC_SDRAM_END - RS_CI_SMOKE_GA2D_DMA_WINDOW_BACK + UINT32_C(0x780),
.foreground = {RS_CI_SMOKE_SDRAM_SCRATCH_END - RS_CI_SMOKE_GA2D_DMA_WINDOW_BACK +
UINT32_C(0x780),
UINT32_C(64), RS_GA2D_FORMAT_XRGB8888},
.background = {0U, 0U, RS_GA2D_FORMAT_A8},
.destination = {RS_SOC_SDRAM_END - RS_CI_SMOKE_GA2D_DMA_WINDOW_BACK + UINT32_C(0x340),
.destination = {RS_CI_SMOKE_SDRAM_SCRATCH_END - RS_CI_SMOKE_GA2D_DMA_WINDOW_BACK +
UINT32_C(0x340),
UINT32_C(64), RS_GA2D_FORMAT_XRGB8888},
.width = 16U,
.height = 16U,
@@ -731,11 +737,12 @@ static bool rs_ci_smoke_ga2d_dma_contention(void) {
/* The LP core is itself a competitor: these setup writes and the bounded
waits below keep LP-fabric traffic active while both engines run. */
rs_ci_smoke_ga2d_pattern_fill(
(volatile uint32_t *)(uintptr_t)(RS_SOC_SDRAM_END - RS_CI_SMOKE_GA2D_DMA_WINDOW_BACK),
(volatile uint32_t *)(uintptr_t)(RS_CI_SMOKE_SDRAM_SCRATCH_END -
RS_CI_SMOKE_GA2D_DMA_WINDOW_BACK),
RS_CI_SMOKE_GA2D_DMA_WORDS);
rs_ci_smoke_ga2d_pattern_fill(
(volatile uint32_t *)(uintptr_t)(RS_SOC_SDRAM_END - RS_CI_SMOKE_GA2D_DMA_WINDOW_BACK +
UINT32_C(0x780)),
(volatile uint32_t *)(uintptr_t)(RS_CI_SMOKE_SDRAM_SCRATCH_END -
RS_CI_SMOKE_GA2D_DMA_WINDOW_BACK + UINT32_C(0x780)),
RS_CI_SMOKE_GA2D_JOB_WORDS);
if ((rs_fabric_monitor_snapshot() != RS_OK) ||
(rs_fabric_monitor_read_master(RS_FABRIC_MASTER_DMA, &dma_before) != RS_OK) ||
@@ -752,12 +759,12 @@ static bool rs_ci_smoke_ga2d_dma_contention(void) {
return false;
}
if (!rs_ci_smoke_ga2d_pattern_check(
(const volatile uint32_t *)(uintptr_t)(RS_SOC_SDRAM_END -
(const volatile uint32_t *)(uintptr_t)(RS_CI_SMOKE_SDRAM_SCRATCH_END -
RS_CI_SMOKE_GA2D_DMA_WINDOW_BACK +
UINT32_C(0x100)),
RS_CI_SMOKE_GA2D_DMA_WORDS) ||
!rs_ci_smoke_ga2d_pattern_check(
(const volatile uint32_t *)(uintptr_t)(RS_SOC_SDRAM_END -
(const volatile uint32_t *)(uintptr_t)(RS_CI_SMOKE_SDRAM_SCRATCH_END -
RS_CI_SMOKE_GA2D_DMA_WINDOW_BACK +
UINT32_C(0x340)),
RS_CI_SMOKE_GA2D_JOB_WORDS)) {
@@ -1070,7 +1077,8 @@ static bool rs_ci_smoke_sdram_wait_ready(void) {
}
static bool rs_ci_smoke_sdram_access(void) {
const uintptr_t scratch = (uintptr_t)(RS_SOC_SDRAM_END - RS_CI_SMOKE_SDRAM_SPAN + UINT32_C(1));
const uintptr_t scratch =
(uintptr_t)(RS_CI_SMOKE_SDRAM_SCRATCH_END - RS_CI_SMOKE_SDRAM_SPAN + UINT32_C(1));
volatile uint8_t *const bytes = (volatile uint8_t *)scratch;
volatile uint16_t *const halfs = (volatile uint16_t *)scratch;
volatile uint32_t *const words = (volatile uint32_t *)scratch;
docs/engineering.md
+7 -5
View File
@@ -16,11 +16,13 @@
Regression Verilator firmware simulations override the profiles' manual
`bringup` default with `APP=ci_smoke`. The IHP130 PR simulation also uses the
32 KiB `ld2_all_sram` layout, the explicit Verilator `--fast-flash` backend,
and a 360-second wall-clock budget. GF180, ICS55, and SKY130 use the common
`ld2_sdram` execution layout, the same fast-flash backend, and a 600-second
budget so the broad smoke does not execute from the serial PSRAM model. The
full serial XPI and PSRAM path remains covered by the Icarus assembly self-test
and directed memory-model tests. This application verifies UART output,
and a 600-second wall-clock budget. GF180, ICS55, and SKY130 use the common
`ld2_sdram` execution layout, the same fast-flash backend, and an 1800-second
budget for the GA2D acceptance workload while LP instruction traffic shares
the SDRAM target. The broad smoke therefore does not execute from the serial
PSRAM model. The full serial XPI and PSRAM path remains covered by the Icarus
assembly self-test and directed memory-model tests. This application verifies
UART output,
archinfo APB readback, on-chip SRAM first/last-word and 8/16/32-bit access,
Fabric Monitor collection through the PCLK-to-HP APB path, truthful extension
capabilities, RNG integration, SDRAM 8/16/32-bit access in a reserved tail
rtl/mini/mk/formal.mk
+58 -58
View File
@@ -1,58 +1,58 @@
FORMAL_DIR := $(VARIANT_ROOT)/formal
FORMAL_SBY ?= sby
FORMAL_BITWUZLA ?= $(shell command -v bitwuzla)
FORMAL_SOLVER := bitwuzla
FORMAL_SOLVER_DIR := $(FORMAL_DIR)/bin
FORMAL_SOLVER_WRAPPER := $(FORMAL_SOLVER_DIR)/bitwuzla
FORMAL_DEPTH ?= 20
FORMAL_PLL_RCU_DEPTH ?= 32
FORMAL_WS2812_DEPTH ?= 120
FORMAL_I2C_DEPTH ?= 80
FORMAL_CLINT_DEPTH ?= 32
FORMAL_PSRAM_DEPTH ?= 32
FORMAL_OPIPSRAM_DEPTH ?= 40
FORMAL_OPIPSRAM_BMC_DEPTH ?= 40
FORMAL_DMA_DEPTH ?= 24
FORMAL_DMA_COVER_DEPTH ?= 32
FORMAL_GA2D_DEPTH ?= 36
FORMAL_GA2D_COVER_DEPTH ?= 199
FORMAL_APU_DEPTH ?= 24
FORMAL_APU_CODEC_DEPTH ?= 32
FORMAL_APU_LOADER_DEPTH ?= 128
FORMAL_APU_LOADER_COVER_DEPTH ?= 128
FORMAL_APU_P5_LOADER_DEPTH ?= 48
FORMAL_DIR := $(VARIANT_ROOT)/formal
FORMAL_SBY ?= sby
FORMAL_BITWUZLA ?= $(shell command -v bitwuzla)
FORMAL_SOLVER := bitwuzla
FORMAL_SOLVER_DIR := $(FORMAL_DIR)/bin
FORMAL_SOLVER_WRAPPER := $(FORMAL_SOLVER_DIR)/bitwuzla
FORMAL_DEPTH ?= 20
FORMAL_PLL_RCU_DEPTH ?= 32
FORMAL_WS2812_DEPTH ?= 120
FORMAL_I2C_DEPTH ?= 80
FORMAL_CLINT_DEPTH ?= 32
FORMAL_PSRAM_DEPTH ?= 32
FORMAL_OPIPSRAM_DEPTH ?= 40
FORMAL_OPIPSRAM_BMC_DEPTH ?= 40
FORMAL_DMA_DEPTH ?= 24
FORMAL_DMA_COVER_DEPTH ?= 32
FORMAL_GA2D_DEPTH ?= 36
FORMAL_GA2D_COVER_DEPTH ?= 199
FORMAL_APU_DEPTH ?= 24
FORMAL_APU_CODEC_DEPTH ?= 32
FORMAL_APU_LOADER_DEPTH ?= 128
FORMAL_APU_LOADER_COVER_DEPTH ?= 128
FORMAL_APU_P5_LOADER_DEPTH ?= 48
FORMAL_APU_P5_LOADER_COVER_DEPTH ?= 145
FORMAL_APU_P5_LOADER_COVER_SKIP = $(if $(filter apu_loader_p5_success,$*),120,$(if $(filter apu_loader_p5_bound,$*),107,$(if $(filter apu_loader_p5_memo_fallback,$*),105,30)))
FORMAL_APU_SEQUENCER_DEPTH ?= 38
FORMAL_APU_KWS_DEPTH ?= 32
FORMAL_GATEWAY_A_DEPTH ?= 20
FORMAL_SDIO_DEPTH ?= 20
FORMAL_SDIO_COVER_DEPTH ?= 24
FORMAL_TIMEOUT ?= 60
FORMAL_WS2812_TIMEOUT ?= 120
FORMAL_I2C_TIMEOUT ?= 300
FORMAL_OPIPSRAM_TIMEOUT ?= 300
FORMAL_OPIPSRAM_BMC_TIMEOUT ?= 600
FORMAL_DMA_TIMEOUT ?= 120
FORMAL_GA2D_TIMEOUT ?= 7200
FORMAL_APU_TIMEOUT ?= 300
FORMAL_GATEWAY_A_TIMEOUT ?= 120
FORMAL_SDIO_TIMEOUT ?= 120
FORMAL_APU_P5_LOADER_TARGETS := apu_loader_p5_success apu_loader_p5_bound apu_loader_p5_abort apu_loader_p5_resource_reset apu_loader_p5_memo_fallback
FORMAL_APU_LOADER_TARGETS := apu_loader_success apu_loader_header_range apu_loader_descriptor_range apu_loader_crc apu_loader_control_flow apu_loader_abort apu_loader_resource_reset $(FORMAL_APU_P5_LOADER_TARGETS)
FORMAL_APU_PRIMITIVE_TARGETS := apu_primitives_invalid_read apu_primitives_local apu_primitives_local_overflow apu_primitives_kernel apu_primitives_input_fifo apu_primitives_alignment apu_primitives_output_fifo
FORMAL_TARGET_TIMEOUT = $(if $(filter ga2d,$*),$(FORMAL_GA2D_TIMEOUT),$(if $(filter dma,$*),$(FORMAL_DMA_TIMEOUT),$(if $(filter apu apu_codec apu_kws apu_primitives apu_sequencer $(FORMAL_APU_LOADER_TARGETS) $(FORMAL_APU_PRIMITIVE_TARGETS),$*),$(FORMAL_APU_TIMEOUT),$(if $(filter gateway_a,$*),$(FORMAL_GATEWAY_A_TIMEOUT),$(if $(filter sdio,$*),$(FORMAL_SDIO_TIMEOUT),$(if $(filter opipsram,$*),$(FORMAL_OPIPSRAM_TIMEOUT),$(if $(filter ws2812,$*),$(FORMAL_WS2812_TIMEOUT),$(if $(filter i2c,$*),$(FORMAL_I2C_TIMEOUT),$(FORMAL_TIMEOUT)))))))))
FORMAL_APU_TARGET_DEPTH = $(if $(filter $(FORMAL_APU_P5_LOADER_TARGETS),$*),$(FORMAL_APU_P5_LOADER_DEPTH),$(if $(filter $(FORMAL_APU_LOADER_TARGETS),$*),$(FORMAL_APU_LOADER_DEPTH),$(if $(filter apu_kws,$*),$(FORMAL_APU_KWS_DEPTH),$(if $(filter apu_sequencer,$*),$(FORMAL_APU_SEQUENCER_DEPTH),$(if $(filter apu_codec,$*),$(FORMAL_APU_CODEC_DEPTH),$(FORMAL_APU_DEPTH))))))
FORMAL_APU_TARGET_COVER_DEPTH = $(if $(filter $(FORMAL_APU_P5_LOADER_TARGETS),$*),$(FORMAL_APU_P5_LOADER_COVER_DEPTH),$(if $(filter $(FORMAL_APU_LOADER_TARGETS),$*),$(FORMAL_APU_LOADER_COVER_DEPTH),$(FORMAL_APU_TARGET_DEPTH)))
FORMAL_TARGET_TOP = $(if $(filter $(FORMAL_APU_LOADER_TARGETS),$*),apu_loader,$(if $(filter $(FORMAL_APU_PRIMITIVE_TARGETS),$*),apu_primitives,$*))
FORMAL_PROPERTIES_SOURCE = $(if $(filter ga2d,$*),$(RTL_PATH)/formal/ga2d_formal.sv,$(RTL_PATH)/formal/$(FORMAL_TARGET_TOP)_formal_props.sv)
FORMAL_PROPERTIES_DEFINE = $(if $(filter ga2d,$*),--properties-define GA2D_FORMAL_PROPERTIES,)
FORMAL_COMPACT_COVER_TARGETS := i2c opipsram dma ga2d $(FORMAL_APU_LOADER_TARGETS) $(FORMAL_APU_PRIMITIVE_TARGETS)
FORMAL_TARGETS := bus rib_adapter rib2apb sysctrl pll_rcu gpio ws2812 uart i2c timer clint dvp i2s psram onchip_ram opipsram dma ga2d apu apu_codec apu_kws $(FORMAL_APU_PRIMITIVE_TARGETS) $(FORMAL_APU_LOADER_TARGETS) apu_sequencer gateway_a sdio
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
FORMAL_SOURCE_FILES := $(RTL_PATH)/formal/bus_formal.sv \
FORMAL_APU_P5_LOADER_COVER_SKIP = $(if $(filter apu_loader_p5_success,$*),120,$(if $(filter apu_loader_p5_bound,$*),107,$(if $(filter apu_loader_p5_memo_fallback,$*),105,30)))
FORMAL_APU_SEQUENCER_DEPTH ?= 38
FORMAL_APU_KWS_DEPTH ?= 32
FORMAL_GATEWAY_A_DEPTH ?= 20
FORMAL_SDIO_DEPTH ?= 20
FORMAL_SDIO_COVER_DEPTH ?= 24
FORMAL_TIMEOUT ?= 60
FORMAL_WS2812_TIMEOUT ?= 120
FORMAL_I2C_TIMEOUT ?= 300
FORMAL_OPIPSRAM_TIMEOUT ?= 300
FORMAL_OPIPSRAM_BMC_TIMEOUT ?= 600
FORMAL_DMA_TIMEOUT ?= 120
FORMAL_GA2D_TIMEOUT ?= 7200
FORMAL_APU_TIMEOUT ?= 300
FORMAL_GATEWAY_A_TIMEOUT ?= 120
FORMAL_SDIO_TIMEOUT ?= 120
FORMAL_APU_P5_LOADER_TARGETS := apu_loader_p5_success apu_loader_p5_bound apu_loader_p5_abort apu_loader_p5_resource_reset apu_loader_p5_memo_fallback
FORMAL_APU_LOADER_TARGETS := apu_loader_success apu_loader_header_range apu_loader_descriptor_range apu_loader_crc apu_loader_control_flow apu_loader_abort apu_loader_resource_reset $(FORMAL_APU_P5_LOADER_TARGETS)
FORMAL_APU_PRIMITIVE_TARGETS := apu_primitives_invalid_read apu_primitives_local apu_primitives_local_overflow apu_primitives_kernel apu_primitives_input_fifo apu_primitives_alignment apu_primitives_output_fifo
FORMAL_TARGET_TIMEOUT = $(if $(filter ga2d,$*),$(FORMAL_GA2D_TIMEOUT),$(if $(filter dma,$*),$(FORMAL_DMA_TIMEOUT),$(if $(filter apu apu_codec apu_kws apu_primitives apu_sequencer $(FORMAL_APU_LOADER_TARGETS) $(FORMAL_APU_PRIMITIVE_TARGETS),$*),$(FORMAL_APU_TIMEOUT),$(if $(filter gateway_a,$*),$(FORMAL_GATEWAY_A_TIMEOUT),$(if $(filter sdio,$*),$(FORMAL_SDIO_TIMEOUT),$(if $(filter opipsram,$*),$(FORMAL_OPIPSRAM_TIMEOUT),$(if $(filter ws2812,$*),$(FORMAL_WS2812_TIMEOUT),$(if $(filter i2c,$*),$(FORMAL_I2C_TIMEOUT),$(FORMAL_TIMEOUT)))))))))
FORMAL_APU_TARGET_DEPTH = $(if $(filter $(FORMAL_APU_P5_LOADER_TARGETS),$*),$(FORMAL_APU_P5_LOADER_DEPTH),$(if $(filter $(FORMAL_APU_LOADER_TARGETS),$*),$(FORMAL_APU_LOADER_DEPTH),$(if $(filter apu_kws,$*),$(FORMAL_APU_KWS_DEPTH),$(if $(filter apu_sequencer,$*),$(FORMAL_APU_SEQUENCER_DEPTH),$(if $(filter apu_codec,$*),$(FORMAL_APU_CODEC_DEPTH),$(FORMAL_APU_DEPTH))))))
FORMAL_APU_TARGET_COVER_DEPTH = $(if $(filter $(FORMAL_APU_P5_LOADER_TARGETS),$*),$(FORMAL_APU_P5_LOADER_COVER_DEPTH),$(if $(filter $(FORMAL_APU_LOADER_TARGETS),$*),$(FORMAL_APU_LOADER_COVER_DEPTH),$(FORMAL_APU_TARGET_DEPTH)))
FORMAL_TARGET_TOP = $(if $(filter $(FORMAL_APU_LOADER_TARGETS),$*),apu_loader,$(if $(filter $(FORMAL_APU_PRIMITIVE_TARGETS),$*),apu_primitives,$*))
FORMAL_PROPERTIES_SOURCE = $(if $(filter ga2d,$*),$(RTL_PATH)/formal/ga2d_formal.sv,$(RTL_PATH)/formal/$(FORMAL_TARGET_TOP)_formal_props.sv)
FORMAL_PROPERTIES_DEFINE = $(if $(filter ga2d,$*),--properties-define GA2D_FORMAL_PROPERTIES,)
FORMAL_COMPACT_COVER_TARGETS := i2c opipsram dma ga2d $(FORMAL_APU_LOADER_TARGETS) $(FORMAL_APU_PRIMITIVE_TARGETS)
FORMAL_TARGETS := bus rib_adapter rib2apb sysctrl pll_rcu gpio ws2812 uart i2c timer clint dvp i2s psram onchip_ram opipsram dma ga2d apu apu_codec apu_kws $(FORMAL_APU_PRIMITIVE_TARGETS) $(FORMAL_APU_LOADER_TARGETS) apu_sequencer gateway_a sdio
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
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 \
@@ -205,15 +205,15 @@ FORMAL_SOURCE_FILES := $(RTL_PATH)/formal/bus_formal.sv \
$(ROOT_PATH)/rtl/managed/clusterip/common/rtl/utils/fifo.sv \
$(ROOT_PATH)/rtl/managed/clusterip/common/rtl/stream/round_robin_arbiter.sv \
$(ROOT_PATH)/scripts/bitwuzla_smt2.py
FORMAL_STAMPS := $(addsuffix /.stamp,$(addprefix $(FORMAL_DIR)/,$(FORMAL_TARGETS)))
FORMAL_INTERMEDIATES := $(foreach target,$(FORMAL_TARGETS), \
FORMAL_STAMPS := $(addsuffix /.stamp,$(addprefix $(FORMAL_DIR)/,$(FORMAL_TARGETS)))
FORMAL_INTERMEDIATES := $(foreach target,$(FORMAL_TARGETS), \
$(FORMAL_DIR)/$(target)/formal.fl $(FORMAL_DIR)/$(target)/design.v \
$(FORMAL_DIR)/$(target)/prove.sby $(FORMAL_DIR)/$(target)/cover.sby \
$(FORMAL_DIR)/$(target)/prove.stamp \
$(FORMAL_DIR)/$(target)/cover.stamp) \
$(FORMAL_DIR)/opipsram/bmc.sby $(FORMAL_DIR)/opipsram/bmc.stamp \
$(FORMAL_SOLVER_WRAPPER)
FORMAL_RESULT := $(META_DIR)/formal.json
FORMAL_RESULT := $(META_DIR)/formal.json
.SECONDARY: $(FORMAL_INTERMEDIATES)
@@ -361,4 +361,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-rib2apb formal-sysctrl formal-pll-rcu formal-gpio formal-ws2812 formal-uart formal-i2c formal-timer formal-clint formal-dvp formal-i2s formal-psram formal-onchip-ram formal-opipsram formal-dma formal-ga2d formal-apu formal-apu-kws formal-apu-loader formal-apu-loader-p5 formal-apu-sequencer formal-gateway-a formal-sdio formal-doctor formal-clean
.PHONY: formal formal-bus formal-rib-adapter formal-rib2apb formal-sysctrl formal-pll-rcu formal-gpio formal-ws2812 formal-uart formal-i2c formal-timer formal-clint formal-dvp formal-i2s formal-psram formal-onchip-ram formal-opipsram formal-dma formal-ga2d formal-apu formal-apu-kws formal-apu-loader formal-apu-loader-p5 formal-apu-sequencer formal-gateway-a formal-sdio formal-doctor formal-clean
scripts/regress.py
+3 -1
View File
@@ -33,7 +33,9 @@ CI_SMOKE_SIM_VALUES = (
CI_SMOKE_SDRAM_SIM_VALUES = (
CI_SMOKE_APP_VALUE,
"LINK_TYPE=ld2_sdram",
"SOC_SIM_TIME=600",
# Hosted Verilator executes the expanded GA2D acceptance workload more
# slowly when LP code and accelerator traffic share the SDRAM target.
"SOC_SIM_TIME=1800",
*CI_SMOKE_VERILATOR_VALUES,
)
RTL_LINT_VALUES = ("SIMU=VERILATOR", "HAVE_SVA=YES", "rtl-lint")
tests/test_script_tools.py
+1 -1
View File
@@ -1397,7 +1397,7 @@ def test_pdk_pr_regressions_cover_firmware_rtl_and_selected_netlist_target() ->
else:
assert "LINK_TYPE=ld2_sdram" in verilator_values
assert "VERILATOR_SIM_ARGS=--fast-flash" in verilator_values
assert "SOC_SIM_TIME=600" in verilator_values
assert "SOC_SIM_TIME=1800" in verilator_values
assert "HAVE_CSR=YES" in verilator_values
assert any("SIMU=IVERILOG" in values and "sim-asm" in values for values in command_values)
assert any("SYNTH=YOSYS" in values and "synth" in values for values in command_values)
tests/test_sdram.py
+5 -1
View File
@@ -170,7 +170,11 @@ def test_ci_software_covers_sdram_mapped_window() -> None:
assert "rs_ci_smoke_sdram_access" in smoke
assert "RS_SOC_SDRAM_BASE" in smoke
assert "RS_SOC_SDRAM_END - RS_CI_SMOKE_SDRAM_SPAN" in smoke
assert "RS_CI_SMOKE_SDRAM_STACK_RESERVE_BYTES UINT32_C(65536)" in smoke
assert "RS_SOC_SDRAM_END - RS_CI_SMOKE_SDRAM_STACK_RESERVE_BYTES" in smoke
assert "RS_CI_SMOKE_SDRAM_SCRATCH_END - RS_CI_SMOKE_SDRAM_SPAN" in smoke
assert "RS_CI_SMOKE_SDRAM_SCRATCH_END - span" in smoke
assert "RS_CI_SMOKE_SDRAM_SCRATCH_END - RS_CI_SMOKE_GA2D_DMA_WINDOW_BACK" in smoke
assert "RS_SOC_SDRAM_BASE" in hello
assert "WAIT_SDRAM_READY" in hello