mirror of
https://github.com/retroSoC/retroSoC.git
synced 2026-11-04 22:32:36 +00:00
maksyuki
3ac9e73ab9
- Updated mailbox purpose tests to reflect new write order and sequence handling. - Added tests to ensure Linux-ready values match LP contract and constants match Linux helper. - Introduced tests to verify that offset changes do not hide stale Linux helpers. - Enhanced environment tests to report current locked launcher and runtime versions. - Added checks for SBT launcher presence in environment labels. - Improved full diagram tests to validate storage geometry and RSA vector configurations. - Expanded register tests to ensure crypto interrupt registers publish all events and lifecycle annotations preserve security boundaries. - Modified script tools tests to include Vexii generation validation and updated workflow assertions.
393 lines
26 KiB
Makefile
393 lines
26 KiB
Makefile
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_NPU_DMA_DEPTH ?= 16
|
|
FORMAL_NPU_DMA_COVER_DEPTH ?= 32
|
|
FORMAL_NPU_CONTEXT_DEPTH ?= 160
|
|
FORMAL_NPU_CONTROL_DEPTH ?= 128
|
|
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 ?= 160
|
|
FORMAL_APU_P5_LOADER_COVER_SKIP = $(if $(filter apu_loader_p5_success,$*),130,$(if $(filter apu_loader_p5_bound,$*),110,$(if $(filter apu_loader_p5_memo_fallback,$*),115,30)))
|
|
FORMAL_APU_SEQUENCER_DEPTH ?= 38
|
|
FORMAL_APU_KWS_DEPTH ?= 32
|
|
FORMAL_APU_P9_DEPTH ?= 40
|
|
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_NPU_DMA_TIMEOUT ?= 7200
|
|
FORMAL_NPU_P6_TIMEOUT ?= 7200
|
|
FORMAL_APU_TIMEOUT ?= 300
|
|
FORMAL_APU_P5_LOADER_TIMEOUT ?= 600
|
|
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 npu_dma,$*),$(FORMAL_NPU_DMA_TIMEOUT),$(if $(filter npu_context npu_control,$*),$(FORMAL_NPU_P6_TIMEOUT),$(if $(filter $(FORMAL_APU_P5_LOADER_TARGETS),$*),$(FORMAL_APU_P5_LOADER_TIMEOUT),$(if $(filter dma,$*),$(FORMAL_DMA_TIMEOUT),$(if $(filter apu apu_codec apu_kws apu_p9 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_p9,$*),$(FORMAL_APU_P9_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 npu_context npu_control $(FORMAL_APU_LOADER_TARGETS) $(FORMAL_APU_PRIMITIVE_TARGETS)
|
|
FORMAL_P6_TARGETS := npu_context npu_control
|
|
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 apu_p9 $(FORMAL_APU_PRIMITIVE_TARGETS) $(FORMAL_APU_LOADER_TARGETS) apu_sequencer gateway_a sdio npu_dma
|
|
FORMAL_ALL_TARGETS := $(FORMAL_TARGETS) $(FORMAL_P6_TARGETS)
|
|
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 \
|
|
$(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 \
|
|
$(RTL_PATH)/formal/pll_rcu_formal_props.sv \
|
|
$(RTL_PATH)/formal/gpio_formal.sv \
|
|
$(RTL_PATH)/formal/gpio_formal_props.sv \
|
|
$(RTL_PATH)/formal/ws2812_formal.sv \
|
|
$(RTL_PATH)/formal/ws2812_formal_props.sv \
|
|
$(RTL_PATH)/formal/uart_formal.sv \
|
|
$(RTL_PATH)/formal/uart_formal_props.sv \
|
|
$(RTL_PATH)/formal/i2c_formal.sv \
|
|
$(RTL_PATH)/formal/i2c_formal_props.sv \
|
|
$(RTL_PATH)/formal/timer_formal.sv \
|
|
$(RTL_PATH)/formal/timer_formal_props.sv \
|
|
$(RTL_PATH)/formal/clint_formal.sv \
|
|
$(RTL_PATH)/formal/clint_formal_props.sv \
|
|
$(RTL_PATH)/formal/dvp_formal.sv \
|
|
$(RTL_PATH)/formal/dvp_formal_props.sv \
|
|
$(RTL_PATH)/formal/i2s_formal.sv \
|
|
$(RTL_PATH)/formal/i2s_formal_props.sv \
|
|
$(RTL_PATH)/formal/psram_formal.sv \
|
|
$(RTL_PATH)/formal/psram_formal_props.sv \
|
|
$(RTL_PATH)/formal/onchip_ram_formal.sv \
|
|
$(RTL_PATH)/formal/onchip_ram_formal_props.sv \
|
|
$(RTL_PATH)/formal/opipsram_formal.sv \
|
|
$(RTL_PATH)/formal/opipsram_formal_props.sv \
|
|
$(RTL_PATH)/formal/dma_formal.sv \
|
|
$(RTL_PATH)/formal/dma_formal_props.sv \
|
|
$(RTL_PATH)/formal/ga2d_formal.sv \
|
|
$(RTL_PATH)/formal/ga2d_formal_props.sv \
|
|
$(RTL_PATH)/formal/apu_formal.sv \
|
|
$(RTL_PATH)/formal/apu_formal_props.sv \
|
|
$(RTL_PATH)/formal/apu_codec_formal.sv \
|
|
$(RTL_PATH)/formal/apu_codec_formal_props.sv \
|
|
$(RTL_PATH)/formal/apu_kws_formal.sv \
|
|
$(RTL_PATH)/formal/apu_kws_formal_props.sv \
|
|
$(RTL_PATH)/formal/apu_p9_formal.sv \
|
|
$(RTL_PATH)/formal/apu_p9_formal_props.sv \
|
|
$(RTL_PATH)/formal/apu_primitives_formal.sv \
|
|
$(RTL_PATH)/formal/apu_primitives_formal_props.sv \
|
|
$(RTL_PATH)/formal/apu_loader_formal.sv \
|
|
$(RTL_PATH)/formal/apu_loader_formal_props.sv \
|
|
$(RTL_PATH)/formal/apu_sequencer_formal.sv \
|
|
$(RTL_PATH)/formal/apu_sequencer_formal_props.sv \
|
|
$(RTL_PATH)/formal/gateway_a_formal.sv \
|
|
$(RTL_PATH)/formal/gateway_a_formal_props.sv \
|
|
$(RTL_PATH)/formal/sdio_formal.sv \
|
|
$(RTL_PATH)/formal/sdio_formal_props.sv \
|
|
$(RTL_PATH)/formal/npu_dma_formal.sv \
|
|
$(RTL_PATH)/formal/npu_dma_formal_props.sv \
|
|
$(RTL_PATH)/formal/npu_context_formal.sv \
|
|
$(RTL_PATH)/formal/npu_context_formal_props.sv \
|
|
$(RTL_PATH)/formal/npu_control_formal.sv \
|
|
$(RTL_PATH)/formal/npu_control_formal_props.sv \
|
|
$(RTL_PATH)/top/rib_bus.sv \
|
|
$(RTL_PATH)/top/rib_error_slave.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/interconnect/ribp_regslice.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/gpio_if.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/user_gpio_if.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/gpio_core.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/gpio_reg.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/apb4_gpio.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/pll_ctrl_if.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/clock_ctrl_if.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/sysctrl_if.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/sysctrl_define.svh \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/sysctrl_reg.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/sysctrl_core.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/apb4_sysctrl.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/ws2812_if.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/ws2812_reg.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/ws2812_core.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/apb4_ws2812.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/uart_if.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/uart_baudgen.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/apb4_uart_tx.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/apb4_uart_rx.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/uart_flow_ctrl.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/uart_core.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/uart_reg.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/apb4_uart.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/i2c_filter.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/i2c_core.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/i2c_reg.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/apb4_i2c.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/i2s_define.svh \
|
|
$(ROOT_PATH)/rtl/ip/serial/i2s_pkg.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/i2s_reg.sv \
|
|
$(ROOT_PATH)/rtl/ip/serial/i2c_if.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/timer_core.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/timer_define.svh \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/timer_reg.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/apb4_timer.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/clint_define.svh \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/clint_if.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/clint_reg.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/clint_core.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/apb4_clint.sv \
|
|
$(ROOT_PATH)/rtl/ip/multimedia/dvp_define.svh \
|
|
$(ROOT_PATH)/rtl/ip/multimedia/dvp_core.sv \
|
|
$(ROOT_PATH)/rtl/ip/multimedia/dvp_reg.sv \
|
|
$(ROOT_PATH)/rtl/ip/multimedia/axi4s_dvp.sv \
|
|
$(ROOT_PATH)/rtl/ip/memory/psram_pkg.sv \
|
|
$(ROOT_PATH)/rtl/ip/memory/psram_axi4.sv \
|
|
$(ROOT_PATH)/rtl/ip/memory/psram_phy.sv \
|
|
$(ROOT_PATH)/rtl/ip/memory/onchip_ram_reg.sv \
|
|
$(ROOT_PATH)/rtl/ip/memory/onchip_ram.sv \
|
|
$(ROOT_PATH)/rtl/tech/tc_sram.sv \
|
|
$(ROOT_PATH)/rtl/managed/clusterip/common/rtl/utils/register.sv \
|
|
$(ROOT_PATH)/rtl/managed/clusterip/common/rtl/utils/xchecker.sv \
|
|
$(ROOT_PATH)/rtl/managed/clusterip/common/rtl/utils/gray2bin.sv \
|
|
$(ROOT_PATH)/rtl/ip/util/async_fifo.sv \
|
|
$(ROOT_PATH)/rtl/tech/tc_clk.sv \
|
|
$(ROOT_PATH)/rtl/tech/tc_opipsram_delay.sv \
|
|
$(ROOT_PATH)/rtl/ip/memory/opipsram_define.svh \
|
|
$(ROOT_PATH)/rtl/ip/memory/opipsram_pkg.sv \
|
|
$(ROOT_PATH)/rtl/ip/memory/opipsram_protocol.sv \
|
|
$(ROOT_PATH)/rtl/ip/memory/opipsram_trx.sv \
|
|
$(ROOT_PATH)/rtl/ip/memory/opipsram_axi4.sv \
|
|
$(ROOT_PATH)/rtl/ip/memory/opipsram_core.sv \
|
|
$(ROOT_PATH)/rtl/ip/memory/opipsram_phy.sv \
|
|
$(ROOT_PATH)/rtl/ip/memory/opipsram_reg.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/dma_pkg.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/dma_req_if.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/dma_axi4_master.sv \
|
|
$(ROOT_PATH)/rtl/ip/multimedia/apu_dma.sv \
|
|
$(ROOT_PATH)/rtl/ip/multimedia/apu_microcode_pkg.sv \
|
|
$(ROOT_PATH)/rtl/ip/multimedia/apu_microcode_loader.sv \
|
|
$(ROOT_PATH)/rtl/ip/multimedia/apu_codec_sequencer.sv \
|
|
$(ROOT_PATH)/rtl/ip/multimedia/apu_codec_transport.sv \
|
|
$(ROOT_PATH)/rtl/ip/multimedia/apu_codec_controller.sv \
|
|
$(ROOT_PATH)/rtl/ip/peripheral/dma_core.sv \
|
|
$(ROOT_PATH)/rtl/managed/clusterip/common/rtl/clkrst/counter.sv \
|
|
$(RTL_PATH)/top/rcu.sv \
|
|
$(RTL_PATH)/top/pll_rcu_controller.sv \
|
|
$(RTL_PATH)/top/hp_axi4_mux3.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/interface/axi4_if.sv \
|
|
$(ROOT_PATH)/rtl/managed/clusterip/common/rtl/interface/axi4_stream_if.sv \
|
|
$(ROOT_PATH)/rtl/managed/clusterip/common/rtl/cdc/cdc_sync.sv \
|
|
$(ROOT_PATH)/rtl/managed/clusterip/common/rtl/cdc/cdc_rst_ctrlr.sv \
|
|
$(ROOT_PATH)/rtl/managed/clusterip/common/rtl/cdc/cdc_2phase.sv \
|
|
$(ROOT_PATH)/rtl/managed/clusterip/common/rtl/clkrst/rst_sync.sv \
|
|
$(ROOT_PATH)/rtl/managed/clusterip/common/rtl/utils/edge_det.sv \
|
|
$(ROOT_PATH)/rtl/managed/clusterip/common/rtl/utils/spill_register.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_ALL_TARGETS)))
|
|
FORMAL_INTERMEDIATES := $(foreach target,$(FORMAL_ALL_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
|
|
|
|
.SECONDARY: $(FORMAL_INTERMEDIATES)
|
|
|
|
$(FORMAL_DIR)/%/formal.fl: $(FORMAL_FILELIST_GENERATOR) $(FORMAL_SOURCE_FILES) \
|
|
$(MEMORY_MAP_STAMP) $(SOC_TOPOLOGY_STAMP) $(USER_EXTENSIONS_STAMP)
|
|
@mkdir -p $(@D)
|
|
python3 $(FORMAL_FILELIST_GENERATOR) --target $* --output $@ \
|
|
--memory-map-dir $(MEMORY_MAP_DIR) --soc-topology-dir $(SOC_TOPOLOGY_DIR) \
|
|
--user-extensions-dir $(USER_EXTENSIONS_DIR)
|
|
|
|
$(FORMAL_DIR)/%/design.v: $(FORMAL_DIR)/%/formal.fl $(ROOT_PATH)/scripts/rtl/convt_sv2v.py \
|
|
$(ROOT_PATH)/scripts/rtl/filelist.py $(FORMAL_SOURCE_FILES)
|
|
python3 $(ROOT_PATH)/scripts/run_flow.py --tool formal-sv2v \
|
|
--log $(@D)/sv2v.log --result $(@D)/result-sv2v.json \
|
|
-- python3 $(ROOT_PATH)/scripts/rtl/convt_sv2v.py -f $< --output $@
|
|
|
|
$(FORMAL_DIR)/%/prove.sby: $(FORMAL_DIR)/%/design.v \
|
|
$(FORMAL_SBY_GENERATOR)
|
|
python3 $(FORMAL_SBY_GENERATOR) --top $(FORMAL_TARGET_TOP)_formal --input $< \
|
|
--properties $(FORMAL_PROPERTIES_SOURCE) $(FORMAL_PROPERTIES_DEFINE) --solver $(FORMAL_SOLVER) \
|
|
--mode $(if $(filter ga2d,$*),bmc,$(if $(filter dma npu_dma npu_context npu_control apu apu_codec apu_kws apu_p9 apu_primitives apu_sequencer $(FORMAL_APU_LOADER_TARGETS) $(FORMAL_APU_PRIMITIVE_TARGETS) gateway_a sdio onchip_ram,$*),bmc,prove)) --depth $(if $(filter ga2d,$*),$(FORMAL_GA2D_DEPTH),$(if $(filter pll_rcu,$*),$(FORMAL_PLL_RCU_DEPTH),$(if $(filter npu_dma,$*),$(FORMAL_NPU_DMA_DEPTH),$(if $(filter npu_context,$*),$(FORMAL_NPU_CONTEXT_DEPTH),$(if $(filter npu_control,$*),$(FORMAL_NPU_CONTROL_DEPTH),$(if $(filter dma,$*),$(FORMAL_DMA_DEPTH),$(if $(filter apu apu_codec apu_kws apu_p9 apu_primitives apu_sequencer $(FORMAL_APU_LOADER_TARGETS) $(FORMAL_APU_PRIMITIVE_TARGETS),$*),$(FORMAL_APU_TARGET_DEPTH),$(if $(filter gateway_a,$*),$(FORMAL_GATEWAY_A_DEPTH),$(if $(filter sdio,$*),$(FORMAL_SDIO_DEPTH),$(if $(filter opipsram,$*),$(FORMAL_OPIPSRAM_DEPTH),$(if $(filter ws2812,$*),$(FORMAL_WS2812_DEPTH),$(if $(filter i2c,$*),$(FORMAL_I2C_DEPTH),$(if $(filter clint,$*),$(FORMAL_CLINT_DEPTH),$(if $(filter psram,$*),$(FORMAL_PSRAM_DEPTH),$(FORMAL_DEPTH))))))))))))))) --output $@
|
|
@if [ "$*" = opipsram ]; then sed -i '/^async2sync/i clk2fflogic' $@; fi
|
|
|
|
$(FORMAL_DIR)/%/cover.sby: $(FORMAL_DIR)/%/design.v \
|
|
$(FORMAL_SBY_GENERATOR)
|
|
python3 $(FORMAL_SBY_GENERATOR) --top $(FORMAL_TARGET_TOP)_formal --input $< \
|
|
--properties $(FORMAL_PROPERTIES_SOURCE) $(FORMAL_PROPERTIES_DEFINE) --solver $(FORMAL_SOLVER) \
|
|
--mode cover --depth $(if $(filter ga2d,$*),$(FORMAL_GA2D_COVER_DEPTH),$(if $(filter pll_rcu,$*),$(FORMAL_PLL_RCU_DEPTH),$(if $(filter npu_dma,$*),$(FORMAL_NPU_DMA_COVER_DEPTH),$(if $(filter npu_context,$*),$(FORMAL_NPU_CONTEXT_DEPTH),$(if $(filter npu_control,$*),$(FORMAL_NPU_CONTROL_DEPTH),$(if $(filter dma,$*),$(FORMAL_DMA_COVER_DEPTH),$(if $(filter apu apu_codec apu_kws apu_p9 apu_primitives apu_sequencer $(FORMAL_APU_LOADER_TARGETS) $(FORMAL_APU_PRIMITIVE_TARGETS),$*),$(FORMAL_APU_TARGET_COVER_DEPTH),$(if $(filter gateway_a,$*),$(FORMAL_GATEWAY_A_DEPTH),$(if $(filter sdio,$*),$(FORMAL_SDIO_COVER_DEPTH),$(if $(filter opipsram,$*),$(FORMAL_OPIPSRAM_DEPTH),$(if $(filter ws2812,$*),$(FORMAL_WS2812_DEPTH),$(if $(filter i2c,$*),$(FORMAL_I2C_DEPTH),$(if $(filter clint,$*),$(FORMAL_CLINT_DEPTH),$(if $(filter psram,$*),$(FORMAL_PSRAM_DEPTH),$(FORMAL_DEPTH))))))))))))))) \
|
|
$(if $(filter $(FORMAL_APU_P5_LOADER_TARGETS),$*),--skip $(FORMAL_APU_P5_LOADER_COVER_SKIP)) \
|
|
$(if $(filter $(FORMAL_COMPACT_COVER_TARGETS),$*),--no-vcd) --output $@
|
|
@if [ "$*" = opipsram ]; then sed -i '/^async2sync/i clk2fflogic' $@; fi
|
|
|
|
$(FORMAL_DIR)/opipsram/bmc.sby: $(FORMAL_DIR)/opipsram/design.v \
|
|
$(RTL_PATH)/formal/opipsram_formal_props.sv $(FORMAL_SBY_GENERATOR)
|
|
python3 $(FORMAL_SBY_GENERATOR) --top opipsram_formal \
|
|
--input $(FORMAL_DIR)/opipsram/design.v \
|
|
--properties $(RTL_PATH)/formal/opipsram_formal_props.sv \
|
|
--solver $(FORMAL_SOLVER) --mode bmc --depth $(FORMAL_OPIPSRAM_BMC_DEPTH) \
|
|
--output $@
|
|
@sed -i 's/^read_verilog -formal -sv properties.v$$/read_verilog -formal -sv -DOPIPSRAM_BMC properties.v/' $@
|
|
@sed -i '/^async2sync/i clk2fflogic' $@
|
|
|
|
$(FORMAL_SOLVER_WRAPPER): $(ROOT_PATH)/scripts/bitwuzla_smt2.py
|
|
@mkdir -p $(@D)
|
|
cp $< $@
|
|
chmod +x $@
|
|
|
|
$(FORMAL_DIR)/%/prove.stamp: $(FORMAL_DIR)/%/prove.sby $(FORMAL_SOLVER_WRAPPER)
|
|
python3 $(ROOT_PATH)/scripts/run_flow.py --tool formal-sby-prove \
|
|
--log $(@D)/prove.log --result $(@D)/result-prove.json \
|
|
--env RETROSOC_BITWUZLA=$(FORMAL_BITWUZLA) \
|
|
--env PATH=$(FORMAL_SOLVER_DIR):$(PATH) \
|
|
-- timeout --foreground --kill-after=5s $(FORMAL_TARGET_TIMEOUT)s $(FORMAL_SBY) \
|
|
-f -d $(@D)/prove $<
|
|
@test "$$(awk '{print $$1}' $(@D)/prove/status)" = PASS
|
|
@touch $@
|
|
|
|
$(FORMAL_DIR)/%/cover.stamp: $(FORMAL_DIR)/%/cover.sby $(FORMAL_SOLVER_WRAPPER)
|
|
python3 $(ROOT_PATH)/scripts/run_flow.py --tool formal-sby-cover \
|
|
--log $(@D)/cover.log --result $(@D)/result-cover.json \
|
|
--env RETROSOC_BITWUZLA=$(FORMAL_BITWUZLA) \
|
|
--env PATH=$(FORMAL_SOLVER_DIR):$(PATH) \
|
|
-- timeout --foreground --kill-after=5s $(FORMAL_TARGET_TIMEOUT)s $(FORMAL_SBY) \
|
|
-f -d $(@D)/cover $<
|
|
@test "$$(awk '{print $$1}' $(@D)/cover/status)" = PASS
|
|
@touch $@
|
|
|
|
$(FORMAL_DIR)/opipsram/bmc.stamp: $(FORMAL_DIR)/opipsram/bmc.sby \
|
|
$(FORMAL_SOLVER_WRAPPER)
|
|
python3 $(ROOT_PATH)/scripts/run_flow.py --tool formal-sby-bmc \
|
|
--log $(@D)/bmc.log --result $(@D)/result-bmc.json \
|
|
--env RETROSOC_BITWUZLA=$(FORMAL_BITWUZLA) \
|
|
--env PATH=$(FORMAL_SOLVER_DIR):$(PATH) \
|
|
-- timeout --foreground --kill-after=5s $(FORMAL_OPIPSRAM_BMC_TIMEOUT)s $(FORMAL_SBY) \
|
|
-f -d $(@D)/bmc $<
|
|
@test "$$(awk '{print $$1}' $(@D)/bmc/status)" = PASS
|
|
@touch $@
|
|
|
|
$(FORMAL_DIR)/opipsram/.stamp: $(FORMAL_DIR)/opipsram/prove.stamp \
|
|
$(FORMAL_DIR)/opipsram/cover.stamp $(FORMAL_DIR)/opipsram/bmc.stamp
|
|
@touch $@
|
|
|
|
$(FORMAL_DIR)/%/.stamp: $(FORMAL_DIR)/%/prove.stamp $(FORMAL_DIR)/%/cover.stamp
|
|
@touch $@
|
|
|
|
$(FORMAL_RESULT): $(FORMAL_STAMPS) $(FORMAL_RESULT_GENERATOR)
|
|
python3 $(FORMAL_RESULT_GENERATOR) --output $@ \
|
|
$(foreach target,$(FORMAL_ALL_TARGETS),--proof $(target)=$(FORMAL_DIR)/$(target))
|
|
|
|
formal: $(FORMAL_RESULT) | manifest
|
|
|
|
formal-apu-kws: $(FORMAL_DIR)/apu_kws/.stamp | manifest
|
|
|
|
formal-apu-p9: $(FORMAL_DIR)/apu_p9/.stamp | manifest
|
|
|
|
formal-bus: $(FORMAL_DIR)/bus/.stamp | manifest
|
|
|
|
formal-rib-adapter: $(FORMAL_DIR)/rib_adapter/.stamp | manifest
|
|
|
|
formal-rib2apb: $(FORMAL_DIR)/rib2apb/.stamp | manifest
|
|
|
|
formal-sysctrl: $(FORMAL_DIR)/sysctrl/.stamp | manifest
|
|
|
|
formal-pll-rcu: $(FORMAL_DIR)/pll_rcu/.stamp | manifest
|
|
|
|
formal-gpio: $(FORMAL_DIR)/gpio/.stamp | manifest
|
|
|
|
formal-ws2812: $(FORMAL_DIR)/ws2812/.stamp | manifest
|
|
|
|
formal-uart: $(FORMAL_DIR)/uart/.stamp | manifest
|
|
|
|
formal-i2c: $(FORMAL_DIR)/i2c/.stamp | manifest
|
|
|
|
formal-timer: $(FORMAL_DIR)/timer/.stamp | manifest
|
|
|
|
formal-clint: $(FORMAL_DIR)/clint/.stamp | manifest
|
|
|
|
formal-dvp: $(FORMAL_DIR)/dvp/.stamp | manifest
|
|
|
|
formal-i2s: $(FORMAL_DIR)/i2s/.stamp | manifest
|
|
|
|
formal-psram: $(FORMAL_DIR)/psram/.stamp | manifest
|
|
|
|
formal-onchip-ram: $(FORMAL_DIR)/onchip_ram/.stamp | manifest
|
|
|
|
formal-opipsram: $(FORMAL_DIR)/opipsram/.stamp | manifest
|
|
|
|
formal-dma: $(FORMAL_DIR)/dma/.stamp | manifest
|
|
|
|
formal-ga2d: $(FORMAL_DIR)/ga2d/.stamp | manifest
|
|
|
|
formal-apu: $(FORMAL_DIR)/apu/.stamp $(FORMAL_DIR)/apu_codec/.stamp $(addsuffix /.stamp,$(addprefix $(FORMAL_DIR)/,$(FORMAL_APU_PRIMITIVE_TARGETS))) | manifest
|
|
|
|
formal-apu-loader: $(addsuffix /.stamp,$(addprefix $(FORMAL_DIR)/,$(FORMAL_APU_LOADER_TARGETS))) | manifest
|
|
|
|
formal-apu-loader-p5: $(addsuffix /.stamp,$(addprefix $(FORMAL_DIR)/,$(FORMAL_APU_P5_LOADER_TARGETS))) | manifest
|
|
|
|
formal-apu-sequencer: $(FORMAL_DIR)/apu_sequencer/.stamp | manifest
|
|
|
|
formal-gateway-a: $(FORMAL_DIR)/gateway_a/.stamp | manifest
|
|
|
|
formal-sdio: $(FORMAL_DIR)/sdio/.stamp | manifest
|
|
|
|
formal-npu_dma: $(FORMAL_DIR)/npu_dma/.stamp | manifest
|
|
|
|
formal-npu-context: $(FORMAL_DIR)/npu_context/.stamp | manifest
|
|
|
|
formal-npu-control: $(FORMAL_DIR)/npu_control/.stamp | manifest
|
|
|
|
formal-npu-p6: $(FORMAL_DIR)/npu_dma/.stamp $(FORMAL_DIR)/npu_context/.stamp \
|
|
$(FORMAL_DIR)/npu_control/.stamp | manifest
|
|
|
|
formal-doctor:
|
|
$(MAKE) FORMAL=YES SIMU=IVERILOG SYNTH=YOSYS STA=NONE 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-p9 formal-apu-loader formal-apu-loader-p5 formal-apu-sequencer formal-gateway-a formal-sdio formal-npu_dma formal-npu-context formal-npu-control formal-npu-p6 formal-doctor formal-clean |