Readme update

README.md

@@ -49,30 +49,11 @@ in [docs/sec-flags-spec.md](docs/sec-flags-spec.md).
 The Kepler‑Formal Naja IF flow is intended to verify incremental modifications generated by the najaeda Python package(https://pypi.org/project/najaeda/) or by any process that maintains stable indices across edits, ensuring that corresponding design elements retain consistent identifiers.
 The property of stable indices is employed to localize the scopes affected by edits and helps the Naja IF flow to achieve superior performance relative to the Verilog flow when handling incremental modifications.
 
-## Dependencies
+## Build Instructions
 
-### Option A: hermetic, via Bazel (any Linux distro)
+### CMake
 
-Let Bazel provide the compiler (hermetic clang/libc++) and pinned library
-dependencies (Boost, Cap'n Proto, TBB, zlib, FlexLexer.h) for the CMake
-build — no compiler or library packages needed, only build tools:
-
-```bash
-sudo apt-get install cmake make pkg-config bison flex python3-dev
-bazelisk run //:deps
-cmake -B build -DCMAKE_TOOLCHAIN_FILE=$PWD/deps/toolchain.cmake
-```
-
-The exported `deps/` tree (~450 MB, mostly the clang distribution) is
-git-ignored and regenerated on each run; the compiler and library versions
-are byte-identical to the ones the Bazel build uses.
-
-Note: cadical and kissat build in-source (`thirdparty/{cadical,kissat}`).
-When switching between the system toolchain and `deps/toolchain.cmake`,
-clean those build directories first (`git -C thirdparty/cadical clean -dfx`
-and likewise for kissat) so no objects from the other compiler linger.
-
-### Option B: system packages
+#### Dependencies
 
 On Ubuntu:
 
@@ -91,9 +72,8 @@ Ensure the versions of `bison` and `flex` installed via Homebrew take precedence
 ```bash
 export PATH="/opt/homebrew/opt/flex/bin:/opt/homebrew/opt/bison/bin:$PATH"
 ```
-## Build
 
-### CMake (primary)
+#### Build
 
 ```bash
 git clone --recurse-submodules https://github.com/keplertech/kepler-formal.git
@@ -117,21 +97,32 @@ cmake .. \
 
 ### Bazel (experimental)
 
-Bazel build notes, dependency details, release flow, and the BCR publication roadmap are tracked in [docs/bcr-roadmap.md](docs/bcr-roadmap.md).
+On Ubuntu, install the required host tools:
+
+```bash
+sudo apt-get install build-essential pkg-config bison flex python3-dev
+```
+
+Build and test with Bazelisk:
+
+```bash
+bazelisk build //src/bin:kepler-formal
+bazelisk test //test/...
+```
+
+Additional notes and the BCR publication roadmap are tracked in
+[docs/bcr-roadmap.md](docs/bcr-roadmap.md).
 
 ## Usage
 
 The full binary and YAML flag reference is tracked in [docs/flags-spec.md](docs/flags-spec.md). SEC-specific flags, engine behavior, encoding defaults, and skipped-output reports are documented in [docs/sec-flags-spec.md](docs/sec-flags-spec.md).
 
 ### Custom Python Primitives
 
-Custom technology primitives can be defined in Python and loaded with the YAML
-`py_tech_files` option. Kepler-formal automatically makes an adjacent `naja.so`
-available while preserving the user's existing `PYTHONPATH`. When relocating
-the executable, copy its complete directory, including `naja.so`, or set
-`PYTHONPATH` to another compatible module. See
-[Custom Python Primitives](docs/python-primitives.md) for the file format,
-lookup behavior, and deployment instructions.
+Custom technology primitives can be defined in Python and loaded through the
+YAML `py_tech_files` option. See
+[Custom Python Primitives](docs/python-primitives.md) for setup and deployment
+and the [Xilinx FPGA example](examples/xilinx) for the use model.
 
 ### SEC Result Codes