Examples docs

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.

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
+```

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
+```