diff --git a/formal/.gitignore b/formal/.gitignore
new file mode 100644
index 00000000..4a1cec9c
--- /dev/null
+++ b/formal/.gitignore
@@ -0,0 +1,2 @@
+build/
+ibex.v
diff --git a/formal/Makefile b/formal/Makefile
new file mode 100644
index 00000000..dc8e4761
--- /dev/null
+++ b/formal/Makefile
@@ -0,0 +1,67 @@
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+# Provide a convenient way to create a Verilog source of Ibex.
+# This is used by riscv-formal. See README.md for more details.
+
+IBEX_ENABLE_WB ?= 0
+
+# Name of the output file
+IBEX_OUT := ibex.v
+# Build folder name
+OUTDIR   := build
+# Source directory relative to this Makefile
+SRC_DIR  := ../rtl
+# Include directory relative to this Makefile
+INC_DIR  := ../shared/rtl
+
+# SystemVerilog sources of Ibex
+SRCS_SV ?= $(SRC_DIR)/ibex_alu.sv 		\
+        $(SRC_DIR)/ibex_compressed_decoder.sv 	\
+        $(SRC_DIR)/ibex_controller.sv 		\
+        $(SRC_DIR)/ibex_counters.sv     	\
+        $(SRC_DIR)/ibex_cs_registers.sv 	\
+        $(SRC_DIR)/ibex_decoder.sv 		\
+        $(SRC_DIR)/ibex_ex_block.sv 		\
+        $(SRC_DIR)/ibex_fetch_fifo.sv 		\
+        $(SRC_DIR)/ibex_id_stage.sv 		\
+        $(SRC_DIR)/ibex_if_stage.sv 		\
+        $(SRC_DIR)/ibex_load_store_unit.sv 	\
+        $(SRC_DIR)/ibex_multdiv_fast.sv 	\
+        $(SRC_DIR)/ibex_multdiv_slow.sv 	\
+        $(SRC_DIR)/ibex_prefetch_buffer.sv 	\
+        $(SRC_DIR)/ibex_pmp.sv 			\
+        $(SRC_DIR)/ibex_register_file_ff.sv 	\
+        $(SRC_DIR)/ibex_wb_stage.sv             \
+        $(SRC_DIR)/ibex_core.sv
+
+PKG ?= $(SRC_DIR)/ibex_pkg.sv
+PRIM ?= ../syn/rtl/prim_clock_gating.v
+
+GEN_V := $(patsubst %.sv,%.v,$(patsubst $(SRC_DIR)%,$(OUTDIR)%,$(SRCS_SV)))
+
+all: $(IBEX_OUT)
+
+verilog: $(GEN_V)
+
+$(OUTDIR):
+	mkdir -p $(OUTDIR)
+
+# Convert each SystemVerilog source into a Verilog file
+$(GEN_V): $(OUTDIR)%.v: $(SRC_DIR)%.sv $(PKG) $(INC_DIR) | $(OUTDIR)
+	sv2v --define=RISCV_FORMAL -I$(INC_DIR) $(PKG) \
+		$< > $@
+
+# Combine multiple Verilog sources into one Ibex Verilog file
+# Disable "M" extension
+$(IBEX_OUT): $(GEN_V) $(PRIM)
+	yosys -p "read_verilog -sv $(PRIM) $(GEN_V)"                          \
+                -p "chparam -set RV32M 0 ibex_core"                           \
+                -p "chparam -set WritebackStage $(IBEX_ENABLE_WB) ibex_core"  \
+                -p "synth -top ibex_core"                                     \
+                -p "write_verilog $(IBEX_OUT)"
+
+.PHONY: clean
+clean:
+	-rm -rf $(IBEX_OUT) $(OUTDIR)
diff --git a/formal/README.md b/formal/README.md
new file mode 100644
index 00000000..b19988e4
--- /dev/null
+++ b/formal/README.md
@@ -0,0 +1,36 @@
+# Formal
+
+**Unsupported Verilog source creation for RISC-V Formal Verification.**
+
+The Verilog source created here is used by [riscv-formal](https://github.com/SymbioticEDA/riscv-formal).
+
+Riscv-formal uses Yosys, but the SystemVerilog front-end of Yosys does not support all the language features used by Ibex.
+The `Makefile` provided here uses sv2v and Yosys to create a single Verilog source of Ibex.
+
+This flow has some similarities to [syn](../syn/README.md), but uses only a simplified subset.
+
+In order to make it easier to use with riscv-formal, the conversion is done with a simple `Makefile`.
+
+## Prerequisites
+
+Install the following, if not used with the container flow described in riscv-formal.
+
+  - [sv2v](https://github.com/zachjs/sv2v), best option is to use the latest version, but [packed arrays](https://github.com/zachjs/sv2v/commit/aea64e903cd0ff8e8437cae7f989e8bc29ac01a2) is required
+  - [Yosys](https://github.com/YosysHQ/yosys)
+
+## Limitations
+
+The "M" extension is currently disabled.
+
+## Usage
+
+It should not be necessary to create the Verilog source manually as it is used by the riscv-formal Ibex build system.
+
+Run the following command from the top level directory of Ibex to create the Verilog source.
+
+```console
+make -C formal
+```
+
+This will create a directory *formal/build* which contains an equivalent Verilog file for each SystemVerilog source.
+The single output file *formal/ibex.v* contains the complete Ibex source, which can then be imported by riscv-formal.