Replace efabless Docker CI with Yosys synthesis check; document upstream OpenLane flow

.github/workflows/sky130-smoke.yml

@@ -0,0 +1,32 @@
+name: sky130-smoke
+
+on:
+  push:
+  pull_request:
+
+jobs:
+  sim:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - run: sudo apt-get update && sudo apt-get install -y iverilog
+      - run: make sim
+
+  formal:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - run: sudo apt-get update && sudo apt-get install -y yosys
+      - name: Install SymbiYosys and solver
+        run: |
+          sudo apt-get install -y python3-pip z3 boolector || true
+          pip3 install --user sby 2>/dev/null || true
+      - run: make formal
+
+  synthesis-check:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - run: sudo apt-get update && sudo apt-get install -y yosys
+      - name: Yosys synthesis (no Docker, PDK-agnostic)
+        run: make sky130-synth-yosys-only

Makefile

@@ -1,6 +1,15 @@
 SIM_OUT := simv
 
-.PHONY: sim clean formal
+.PHONY: sim clean formal sky130-synth sky130-synth-local sky130-synth-yosys-only
+
+# Frozen tile configuration
+DATA_W ?= 8
+ACC_W  ?= 16
+LEN_W  ?= 6
+PDK_ROOT ?= $(HOME)/.volare
+SKY130_LIB ?= $(PDK_ROOT)/sky130A/libs.ref/sky130_fd_sc_hd/lib/sky130_fd_sc_hd__tt_025C_1v80.lib
+SYNTH_DIR := build/synth
+YOSYS_READ := read_verilog -sv rtl/dpu_tile.sv; chparam -set DATA_W $(DATA_W) -set ACC_W $(ACC_W) -set LEN_W $(LEN_W) dpu_tile; hierarchy -top dpu_tile
 
 sim:
 	iverilog -g2012 -Wall -o $(SIM_OUT) rtl/dpu_tile.sv tb/dpu_tile_tb.sv
@@ -13,7 +22,28 @@ formal:
 	fi
 	sby -f formal/dpu_tile.sby
 
+# Requires Docker + OpenLane (see openlane/README.md); runs the full flow.
+sky130-synth:
+	@if ! command -v docker >/dev/null 2>&1 && [ -z "$$OPENLANE_ROOT" ]; then \
+		echo "Requires Docker and an upstream OpenLane checkout (OPENLANE_ROOT). See openlane/README.md."; \
+		exit 1; \
+	fi
+	cd $${OPENLANE_ROOT:-.} && make mount MOUNT_CMD='./flow.tcl -design $(CURDIR)/openlane'
+
+# Lightweight, PDK-agnostic synthesis check (used in CI); no Docker, no liberty.
+sky130-synth-yosys-only:
+	@command -v yosys >/dev/null 2>&1 || { echo "yosys is not installed"; exit 1; }
+	@mkdir -p $(SYNTH_DIR)
+	yosys -p "$(YOSYS_READ); synth -top dpu_tile -flatten; check -assert; stat; write_verilog -noattr $(SYNTH_DIR)/dpu_tile_generic.v"
+
+# Maps to sky130_fd_sc_hd cells; needs the sky130 liberty (set SKY130_LIB or PDK_ROOT).
+sky130-synth-local:
+	@command -v yosys >/dev/null 2>&1 || { echo "yosys is not installed"; exit 1; }
+	@test -f "$(SKY130_LIB)" || { echo "Liberty not found: $(SKY130_LIB). Set SKY130_LIB or PDK_ROOT."; exit 1; }
+	@mkdir -p $(SYNTH_DIR)
+	yosys -q -p "$(YOSYS_READ); synth -top dpu_tile -flatten; dfflibmap -liberty $(SKY130_LIB); abc -liberty $(SKY130_LIB); opt_clean -purge; check -assert; tee -o $(SYNTH_DIR)/stat.txt stat -liberty $(SKY130_LIB); write_verilog -noattr $(SYNTH_DIR)/dpu_tile_sky130.v"
+
 clean:
 	rm -f $(SIM_OUT) *.vcd
-	rm -rf formal/output
+	rm -rf formal/output build
 

README.md

@@ -22,7 +22,9 @@ The design here is intentionally narrow: a signed `int8` dot-product tile with s
 - `docs/architecture.md` — architecture intent and scaling path
 - `docs/verification.md` — verification strategy
 - `docs/roadmap.md` — longer-term scaling notes
-- `Makefile` — simulation and formal entry points
+- `docs/SYNTHESIS.md` — sky130 synthesis flow
+- `openlane/README.md` — full P&R with upstream OpenLane
+- `Makefile` — simulation, formal, and synthesis entry points
 
 ## Why this is the right first silicon
 
@@ -69,6 +71,13 @@ The cleanest way to get this design to silicon is a single, disciplined sequence
 
 This is the real roadmap: behavior first, proof next, physical estimate third, then manufacturing based on real learning and demand.
 
+## Physical Design Flow
+
+Two tiers:
+
+- **Lightweight:** Yosys synthesis in CI (`make sky130-synth-yosys-only`) for fast validation, no Docker.
+- **Full signoff:** OpenLane P&R run locally with upstream [OpenLane](https://github.com/The-OpenROAD-Project/OpenLane) (see `openlane/README.md` and `docs/SYNTHESIS.md`).
+
 ## Supply chain tradeoffs
 
 The manufacturing decision is not about picking a single best path; it is about choosing the right tradeoff at the right maturity stage.

docs/SYNTHESIS.md

@@ -0,0 +1,32 @@
+# SKY130 synthesis flow
+
+Target configuration: `DATA_W=8`, `ACC_W=16`, `LEN_W=6`, sky130 (`sky130_fd_sc_hd`), 100 MHz (10 ns).
+The Makefile overrides the RTL defaults via `chparam`.
+
+## Targets
+
+| Target | Needs | Description |
+| --- | --- | --- |
+| `make sky130-synth-yosys-only` | yosys | PDK-agnostic synthesis + `check -assert`; used in CI |
+| `make sky130-synth-local` | yosys + sky130 liberty | Maps flops (`dfflibmap`) and logic (`abc`) to `sky130_fd_sc_hd` cells, writes `build/synth/stat.txt` and `build/synth/dpu_tile_sky130.v` |
+| `make sky130-synth` | Docker + upstream OpenLane | Full OpenLane flow; see `openlane/README.md` |
+
+## Yosys with sky130 libraries
+
+`sky130-synth-local` uses the liberty file
+`$(PDK_ROOT)/sky130A/libs.ref/sky130_fd_sc_hd/lib/sky130_fd_sc_hd__tt_025C_1v80.lib`
+(override with `SKY130_LIB=...`). The PDK can be installed with the upstream OpenLane
+`make` or with [volare](https://github.com/efabless/volare). `.lef` files
+(`.../sky130_fd_sc_hd/lef/`) are not used by Yosys; they are consumed by OpenROAD
+during P&R in OpenLane.
+
+```sh
+make sky130-synth-local PDK_ROOT=$HOME/.volare
+```
+
+## Expected mappings and constraints
+
+- Registers map to `sky130_fd_sc_hd__dfxtp_*` (or `dfrtp_*` with async reset).
+- Combinational logic (multiplier, adder, saturation) maps to `nand/nor/a21oi/xor/xnor/mux2` cells via ABC.
+- `check -assert` must pass: no combinational loops, no undriven/multi-driven wires.
+- Timing: 100 MHz target; timing closure is evaluated by STA in OpenLane, not in the Yosys check.

openlane/README.md

@@ -0,0 +1,38 @@
+# OpenLane (full P&R, local/manual)
+
+CI only runs a lightweight Yosys synthesis check (`make sky130-synth-yosys-only`).
+Full place-and-route and signoff is run locally with **upstream OpenLane**
+([The-OpenROAD-Project/OpenLane](https://github.com/The-OpenROAD-Project/OpenLane)).
+We do not depend on the `efabless/openlane` Docker image in CI, which keeps the
+repo independent of any single maintained fork and CI fast and reliable.
+
+## Why two tiers
+
+| Tier | Where | Purpose |
+| --- | --- | --- |
+| Yosys synthesis | CI | Fast check that RTL synthesizes cleanly (no Docker, PDK-agnostic) |
+| OpenLane P&R | Local/manual | Floorplan, placement, CTS, routing, STA, DRC/LVS for MPW signoff |
+
+## Running upstream OpenLane locally
+
+Prerequisites: Docker, git, make, Python 3.
+
+```sh
+git clone https://github.com/The-OpenROAD-Project/OpenLane.git
+cd OpenLane
+make            # installs the PDK (sky130A) and pulls the tooling image
+make test       # sanity check of the install
+```
+
+Then, from this repo, point OpenLane at a design directory containing `config.json`
+(top `dpu_tile`, `DATA_W=8`, `ACC_W=16`, `LEN_W=6`, 100 MHz i.e. `CLOCK_PERIOD=10` ns,
+SDC from the existing constraints) and run:
+
+```sh
+export OPENLANE_ROOT=/path/to/OpenLane
+make sky130-synth        # requires Docker + OpenLane
+```
+
+or directly inside the OpenLane checkout: `make mount` then `./flow.tcl -design /path/to/dpu/openlane`.
+
+See `docs/SYNTHESIS.md` for the synthesis-only flow.