# 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
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

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)

# 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
