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: ensure consistent formatting and newline handling in Makefiles and documentation

Browse Source
This commit is contained in:
maksyuki committed 2026-08-20 21:09:50 +08:00
1 parent ef84c818b0
commit 7df897b038
6 files changed
+41 -41
Download Patch File Download Diff File Expand all files Collapse all files

No files matched your search

Makefile
+1 -1
View File
@@ -491,4 +491,4 @@ regress-nightly:
python3 $(ROOT_PATH)/scripts/regress.py --root $(ROOT_PATH) --suite nightly
sim-asm: asm
$(MAKE) SIM_FIRMWARE_NAME=$(ASM_FIRMWARE_NAME) sim
$(MAKE) SIM_FIRMWARE_NAME=$(ASM_FIRMWARE_NAME) sim
app/apps/xpi_flash_loader/app.mk
+1 -1
View File
@@ -1,2 +1,2 @@
APP_SRCS += $(ROOT_PATH)/app/apps/xpi_flash_loader/main.c
APP_CRT_SRCS += $(ROOT_PATH)/app/apps/xpi_flash_loader/startup.S
APP_CRT_SRCS += $(ROOT_PATH)/app/apps/xpi_flash_loader/startup.S
configs/ci/ihp130-xpi-flash-loader.mk
+1 -1
View File
@@ -12,4 +12,4 @@ ISA := RV32IM
HAVE_CSR := NO
APP := xpi_flash_loader
FIRMWARE_NAME := retrosoc_xpi_flash_loader
LINK_TYPE := jtag_sram
LINK_TYPE := jtag_sram
docs/engineering.md
+5 -5
View File
@@ -210,11 +210,11 @@ are maintained in the Common repository.
wall-clock limit. Use `make CONFIG=<profile> formal-doctor` before a local
proof to verify that the required tools are available.
The I2C cover task stores the compact Yosys witness, constraints, and Verilog
testbench but disables direct VCD output. Expanding the 70-cycle receive cover
to VCD produces hundreds of MiB and can exceed the task limit on networked
filesystems; the witness remains available for an explicit trace conversion
when waveform inspection is required.
The I2C and DMA cover tasks store the compact Yosys witness, constraints, and
Verilog testbench but disable direct VCD output. Expanding the longer I2C
receive or DMA burst covers to VCD produces large artifacts and can exceed the
task limit on networked filesystems; the witness remains available for an
explicit trace conversion when waveform inspection is required.
The locked Bitwuzla 0.9.1 CLI uses `--lang smt2`, while the selected Yosys
version invokes legacy Bitwuzla options. `scripts/bitwuzla_smt2.py` is the
rtl/mini/mk/formal.mk
+32 -32
View File
@@ -1,32 +1,32 @@
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_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_SDIO_DEPTH ?= 20
FORMAL_SDIO_COVER_DEPTH ?= 24
FORMAL_TIMEOUT ?= 60
FORMAL_WS2812_TIMEOUT ?= 120
FORMAL_I2C_TIMEOUT ?= 300
FORMAL_OPIPSRAM_TIMEOUT ?= 300
FORMAL_DMA_TIMEOUT ?= 120
FORMAL_SDIO_TIMEOUT ?= 120
FORMAL_COMPACT_COVER_TARGETS := i2c opipsram
FORMAL_TARGETS := bus rib_adapter rib2apb sysctrl pll_rcu gpio ws2812 uart i2c timer clint dvp i2s psram opipsram dma 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_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_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_SDIO_DEPTH ?= 20
FORMAL_SDIO_COVER_DEPTH ?= 24
FORMAL_TIMEOUT ?= 60
FORMAL_WS2812_TIMEOUT ?= 120
FORMAL_I2C_TIMEOUT ?= 300
FORMAL_OPIPSRAM_TIMEOUT ?= 300
FORMAL_DMA_TIMEOUT ?= 120
FORMAL_SDIO_TIMEOUT ?= 120
FORMAL_COMPACT_COVER_TARGETS := i2c opipsram dma
FORMAL_TARGETS := bus rib_adapter rib2apb sysctrl pll_rcu gpio ws2812 uart i2c timer clint dvp i2s psram opipsram dma 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 \
@@ -150,15 +150,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)
rtl/mini/mk/software.mk
+1 -1
View File
@@ -211,4 +211,4 @@ firmware: $(FIRMWARE_ELF)
firmware asm: | manifest
.PHONY: FORCE_VERSION
.PHONY: FORCE_VERSION