Silicon Architect

Search GitHub for existing open-source Verilog/VHDL IP cores before writing RTL from scratch. Use this FIRST when the spec names a standard block (UART, SPI, I2C, FIFO, AXI), so the design can reference proven prior art. Returns repositories ranked by stars.

Submit Verilog/SystemVerilog for a design and elaborate it with Yosys (read_verilog + hierarchy -check). Creates a new design, or revises an existing one when design_id is given. Returns the elaboration verdict and the parsed module interfaces. If ok is false, read elaboration_log, fix the RTL, and call this again with the same design_id.

Formally verify a design by proving its assertions with bounded model checking (Yosys `sat -prove-asserts`). This does NOT simulate a stimulus: each assertion is proved against ALL possible inputs for `depth` clock cycles, and a failure returns a concrete counterexample. The testbench must be a MODULE with clk/rst inputs that instantiates the DUT and contains IMMEDIATE assertions inside a clocked always block: always @(posedge clk) if (!rst) a_name: assert (<expr>); Concurrent SVA — `assert property (@(posedge clk) ... |-> ...)` — is a SYNTAX ERROR here (it needs Verific, which the open-source Yosys does not ship). Express implication with a plain if, not |-> or |=>. An initial block will not work and $display is not captured. Returns ok:false plus per-assertion results with source locations when a proof fails. On failure it also returns `trace`: the concrete per-cycle counterexample (signals x cycles) the solver proved exists. `trace` is NULL when the proof succeeds — a proved design has no counterexample.

Synthesize the design with Yosys. For target sky130 this returns REAL cell area in µm² from the vendored liberty file (the input the cost model needs). For artix7/ecp5/ice40 it returns resource counts, and for artix7 a part fit against the XC7A35T. Note: Artix-7 synthesis reports utilization only — it cannot produce Fmax.

Run real place-and-route with nextpnr and report the ACHIEVED Fmax. This is the only tool that produces a genuine timing number. ECP5 and iCE40 only — nextpnr has no Artix-7 support, so Fmax cannot be obtained for Xilinx parts with this toolchain.

Return the design's netlist as a node/edge graph for a schematic/chip visualisation. level 'rtl' gives ~10-30 generic cells ($add/$dff/$mux) — one node per RTL construct, readable. level 'gate' gives the mapped sky130 standard cells (~100+). Every cell node carries `src` (file:line) for click-to-source. Edges are real bit-level nets between ports.

Convert real synthesized cell area into a fabrication cost using IHP SG13G2 MPW pricing (€7,300/mm²), with a TinyTapeout cross-check. Requires a prior sky130 synthesis — this tool will not invent an area figure.

Produce the final engineering report for a design: RTL, Verification, Synthesis, Design Summary, and Cost Analysis. Use kind="all" for the complete costed report. Sections whose stage has not run are reported as "not run" rather than estimated.

List every design in this session with its pipeline status.