From 62d03c928c4402821a2cda2a1fb6ed62c54f39ef Mon Sep 17 00:00:00 2001
From: Noam Cohen <noam.chn1@gmail.com>
Date: Wed, 12 Aug 2026 11:00:58 +0200
Subject: [PATCH] Document Xilinx examples

---
 examples/xilinx/README.md                | 12 ++++++++++++
 examples/xilinx/register_slice/README.md | 11 +++++++++++
 examples/xilinx/vexriscv/README.md       | 19 +++++++++++++++++++
 3 files changed, 42 insertions(+)
 create mode 100644 examples/xilinx/README.md
 create mode 100644 examples/xilinx/register_slice/README.md
 create mode 100644 examples/xilinx/vexriscv/README.md

diff --git a/examples/xilinx/README.md b/examples/xilinx/README.md
new file mode 100644
index 00000000..94805e28
--- /dev/null
+++ b/examples/xilinx/README.md
@@ -0,0 +1,12 @@
+# Xilinx Examples
+
+The Xilinx examples use the shared [`xilinx.py`](xilinx.py) formal primitive
+models through the YAML `py_tech_files` option.
+
+| Directory | Contents |
+| --- | --- |
+| [`register_slice`](register_slice) | Small mapped-versus-compact SEC equivalence example. |
+| [`vexriscv`](vexriscv) | Large VexRiscv GenFull LEC self-check and intentional-difference examples. |
+
+`xilinx.py` models the combinational, parameterized LUT, sequential, carry,
+DSP, distributed RAM, and block RAM primitives used by these netlists.
diff --git a/examples/xilinx/register_slice/README.md b/examples/xilinx/register_slice/README.md
new file mode 100644
index 00000000..5540f936
--- /dev/null
+++ b/examples/xilinx/register_slice/README.md
@@ -0,0 +1,11 @@
+# Xilinx Register-Slice SEC
+
+This compares a Xilinx-mapped register slice with a compact equivalent model.
+SEC is expected to prove equivalence.
+
+Run from `examples/xilinx/register_slice`:
+
+```bash
+../../../build/src/bin/kepler-formal \
+  --config test_config_verilog_xilinx_sec.yaml
+```
diff --git a/examples/xilinx/vexriscv/README.md b/examples/xilinx/vexriscv/README.md
new file mode 100644
index 00000000..98bcc27f
--- /dev/null
+++ b/examples/xilinx/vexriscv/README.md
@@ -0,0 +1,19 @@
+# Xilinx VexRiscv LEC
+
+Run these commands from `examples/xilinx/vexriscv`.
+
+The self-check compares the 4,995-cell VexRiscv GenFull netlist with itself and
+is expected to report no difference.
+
+```bash
+../../../build/src/bin/kepler-formal \
+  --config test_config_verilog_vexriscv_genfull_xilinx_lec.yaml
+```
+
+The negative case compares it with an intentionally changed netlist and is
+expected to report a difference.
+
+```bash
+../../../build/src/bin/kepler-formal \
+  --config test_config_verilog_vexriscv_genfull_xilinx_lec_different.yaml
+```