# rvsail RVFI BMC Makefile
#
# Runs riscv-formal bounded model checking against Ibex using
# Sail-derived instruction checkers from software/rvfi/insns/.
#
# Prerequisites:
#   - SymbiYosys (sby), Yosys, and a solver (boolector or z3)
#   - riscv-formal cloned to RISCV_FORMAL_DIR
#   - Ibex RTL at IBEX_DIR
#
# Usage:
#   make generate   # Generate SBY check files via genchecks.py
#   make run-all    # Run all BMC checks
#   make run-add    # Run a single check (e.g., insn_add)

RISCV_FORMAL_DIR ?= /tmp/riscv-formal
IBEX_DIR ?= $(shell pwd)/../../extern/ibex
PRIM_DIR ?= $(IBEX_DIR)/vendor/lowrisc_ip/ip/prim/rtl
PRIM_GEN_DIR ?= $(IBEX_DIR)/vendor/lowrisc_ip/ip/prim_generic/rtl
DV_DIR ?= $(IBEX_DIR)/vendor/lowrisc_ip/dv/sv/dv_utils
CHECKS_DIR ?= checks
RVFI_INSNS_DIR ?= $(shell pwd)/insns

# All RV32I instructions
RV32I_INSNS = add sub sll slt sltu xor srl sra or and \
              addi slti sltiu xori ori andi slli srli srai \
              lb lh lw lbu lhu \
              sb sh sw \
              beq bne blt bge bltu bgeu \
              lui auipc jal jalr

.PHONY: all generate setup run-all clean check-deps sv2v

all: check-deps generate

check-deps:
	@which sby >/dev/null 2>&1 || (echo "ERROR: sby (SymbiYosys) not found in PATH" && exit 1)
	@which yosys >/dev/null 2>&1 || (echo "ERROR: yosys not found in PATH" && exit 1)
	@test -d $(RISCV_FORMAL_DIR) || (echo "ERROR: riscv-formal not found at $(RISCV_FORMAL_DIR)" && exit 1)

# Regenerate sv2v output from Ibex RTL and patch hierarchical RVFI probes
# The RVFI logic in ibex_core.sv uses hierarchical references like
# id_stage_i.controller_i.exc_req_d that Yosys cannot resolve after sv2v.
# This target regenerates the conversion and replaces those refs with
# unconstrained wires (safe for BMC — they only affect RVFI trap metadata).
sv2v: check-deps
	@echo "=== Regenerating sv2v output ==="
	sv2v --define=RVFI --define=YOSYS --define=SYNTHESIS \
	  -I $(PRIM_DIR)/ \
	  -I $(DV_DIR)/ \
	  $(PRIM_GEN_DIR)/prim_ram_1p_pkg.sv \
	  $(PRIM_DIR)/prim_util_pkg.sv \
	  $(PRIM_DIR)/prim_secded_pkg.sv \
	  $(PRIM_DIR)/prim_mubi_pkg.sv \
	  $(PRIM_DIR)/prim_count_pkg.sv \
	  $(PRIM_DIR)/prim_cipher_pkg.sv \
	  $(PRIM_GEN_DIR)/prim_buf.sv \
	  $(PRIM_GEN_DIR)/prim_flop.sv \
	  $(PRIM_GEN_DIR)/prim_clock_gating.sv \
	  $(PRIM_GEN_DIR)/prim_clock_mux2.sv \
	  $(PRIM_DIR)/prim_secded_inv_39_32_enc.sv \
	  $(PRIM_DIR)/prim_secded_inv_39_32_dec.sv \
	  $(PRIM_DIR)/prim_secded_inv_28_22_enc.sv \
	  $(PRIM_DIR)/prim_secded_inv_28_22_dec.sv \
	  $(PRIM_DIR)/prim_lfsr.sv \
	  $(PRIM_DIR)/prim_count.sv \
	  $(PRIM_GEN_DIR)/prim_ram_1p.sv \
	  $(PRIM_DIR)/prim_ram_1p_scr.sv \
	  $(PRIM_DIR)/prim_ram_1p_adv.sv \
	  $(PRIM_DIR)/prim_prince.sv \
	  $(PRIM_DIR)/prim_subst_perm.sv \
	  $(IBEX_DIR)/rtl/ibex_pkg.sv \
	  $(IBEX_DIR)/rtl/ibex_alu.sv \
	  $(IBEX_DIR)/rtl/ibex_compressed_decoder.sv \
	  $(IBEX_DIR)/rtl/ibex_controller.sv \
	  $(IBEX_DIR)/rtl/ibex_core.sv \
	  $(IBEX_DIR)/rtl/ibex_counter.sv \
	  $(IBEX_DIR)/rtl/ibex_cs_registers.sv \
	  $(IBEX_DIR)/rtl/ibex_csr.sv \
	  $(IBEX_DIR)/rtl/ibex_decoder.sv \
	  $(IBEX_DIR)/rtl/ibex_ex_block.sv \
	  $(IBEX_DIR)/rtl/ibex_fetch_fifo.sv \
	  $(IBEX_DIR)/rtl/ibex_id_stage.sv \
	  $(IBEX_DIR)/rtl/ibex_if_stage.sv \
	  $(IBEX_DIR)/rtl/ibex_load_store_unit.sv \
	  $(IBEX_DIR)/rtl/ibex_multdiv_fast.sv \
	  $(IBEX_DIR)/rtl/ibex_multdiv_slow.sv \
	  $(IBEX_DIR)/rtl/ibex_prefetch_buffer.sv \
	  $(IBEX_DIR)/rtl/ibex_register_file_ff.sv \
	  $(IBEX_DIR)/rtl/ibex_wb_stage.sv \
	  $(IBEX_DIR)/rtl/ibex_top.sv \
	  > ibex_full_sv2v.v
	@echo "=== Patching hierarchical RVFI probes ==="
	python3 patch_rvfi_probes.py ibex_full_sv2v.v
	@echo "sv2v done. Verify with: yosys -p 'read -sv ibex_full_sv2v.v; prep -top ibex_top'"

# Set up the riscv-formal core directory for Ibex
setup: check-deps
	@echo "=== Setting up riscv-formal Ibex core ==="
	mkdir -p $(RISCV_FORMAL_DIR)/cores/rvsail-ibex
	# Copy wrapper
	cp ibex_wrapper.sv $(RISCV_FORMAL_DIR)/cores/rvsail-ibex/wrapper.sv
	# Copy checks config
	cp ibex_checks.cfg $(RISCV_FORMAL_DIR)/cores/rvsail-ibex/checks.cfg
	# Symlink our insns directory into riscv-formal
	ln -sfn $(RVFI_INSNS_DIR) $(RISCV_FORMAL_DIR)/insns/rvsail
	@echo "Setup complete."

# Generate SBY files using riscv-formal's genchecks.py
generate: setup
	@echo "=== Generating SBY check files ==="
	cd $(RISCV_FORMAL_DIR)/cores/rvsail-ibex && \
		python3 $(RISCV_FORMAL_DIR)/checks/genchecks.py
	@echo "Generated SBY files in $(RISCV_FORMAL_DIR)/cores/rvsail-ibex/checks/"

# Run all instruction checks
run-all: generate
	@echo "=== Running all RV32I BMC checks ==="
	@cd $(RISCV_FORMAL_DIR)/cores/rvsail-ibex/checks && \
		for insn in $(RV32I_INSNS); do \
			echo "--- Running insn_$${insn}_ch0 ---"; \
			sby -f insn_$${insn}_ch0.sby 2>&1 | tail -1 || true; \
		done

# Run a single instruction check
run-%:
	@echo "=== Running insn_$*_ch0 ==="
	cd $(RISCV_FORMAL_DIR)/cores/rvsail-ibex/checks && \
		sby -f insn_$*_ch0.sby

# Clean generated artifacts
clean:
	rm -rf $(RISCV_FORMAL_DIR)/cores/rvsail-ibex/checks/
	rm -rf $(CHECKS_DIR)

# Quick summary of all results
summary:
	@echo "=== BMC Results Summary ==="
	@cd $(RISCV_FORMAL_DIR)/cores/rvsail-ibex/checks && \
		for insn in $(RV32I_INSNS); do \
			if [ -f insn_$${insn}_ch0/PASS ]; then \
				echo "PASS: insn_$${insn}"; \
			elif [ -f insn_$${insn}_ch0/FAIL ]; then \
				echo "FAIL: insn_$${insn}"; \
			else \
				echo "  ??: insn_$${insn}"; \
			fi; \
		done
