Synthesis and formal checks

Applies to SiliconForge 0.1.2 · Updated 2026-09-30. Check platform limits.

Before this task: Confirm engines, solvers and configuration →

Synthesis reveals a transformed implementation. Formal checks prove specified properties under assumptions. Neither automatically establishes a shippable chip.

Freeze the question and inputs#

Confirm source, top, parameters, toolchain and target. You need a supported Yosys flow for synthesis; formal additionally needs the configured SymbiYosys/solver flow and a reviewed harness. Keep the original RTL and prior evidence so comparisons use matched settings.

Create and inspect a current netlist#

1. Open the intended scope under Design → RTL Hierarchy or Connections.
2. Select Netlist. If no current source-bound artifact exists, read the blocked state and use Run synthesis when offered for that scope.
3. Inspect the job's command, diagnostics and result. A missing tool, unsupported construct or failed synthesis is not an empty but valid design.
4. Open the resulting Netlist and examine cells/nets. Return to the linked source where mapping exists; optimizations can merge or remove source-level objects.
5. Compare resource counts only under the same top, parameters, synthesis settings and tool identity.

Expected result: a current source-bound synthesis artifact, or a clear blocker. Generic-cell counts are not a target FPGA LUT budget, measured clock frequency, placement/routing result or power estimate. A device representation requires separate implementation evidence.

Run a reproducible synthesis example#

Use a disposable copy of stream_register.sv and a separately installed compatible Yosys on your terminal PATH. Save the following as stream-synth.ys beside the RTL, then run the command below in that directory. These are standalone tool commands. Use the reviewed tools recorded in your package inventory or a supported external installation. A shell result does not become native app evidence automatically.

read_verilog -sv stream_register.sv
hierarchy -check -top stream_register
synth -top stream_register
check -assert
stat
write_json stream-netlist.json

env TERM=dumb COLUMNS=32768 yosys -l stream-synth.log -s stream-synth.ys

This is the Linux terminal command. The terminal settings prevent Yosys/ABC from waiting indefinitely when a private temporary-directory path is long; they do not change synthesis or disable checks. SiliconForge sets these values automatically for its managed engineering jobs. In Windows PowerShell, run $env:TERM = 'dumb'; $env:COLUMNS = '32768', then yosys -l stream-synth.log -s stream-synth.ys. Keep private temporary directories private; do not work around a stalled run by relaxing their permissions.

Expected result: exit success, no hierarchy/check error, and a nonempty stream-netlist.json containing the stream_register module and its ports/cells. Preserve the log, source and tool version together. This is generic synthesis, not device mapping, physical implementation or timing closure. If Yosys reports an unknown module, unsupported construct or check failure, retain that diagnostic rather than opening an old JSON file as the new result.

Read a formal result#

1. Read the assertion itself and the environment assumptions. Identify clock/reset semantics, parameter values and permitted inputs.
2. Run the configured supported formal check through the appropriate verification/profile flow. The UI does not provide an unrestricted “prove any project” shortcut.
3. Inspect engine, mode, bound and terminal result. Distinguish bounded model checking, induction/prove, cover, timeout and tool error.
4. For a failure, preserve the counterexample and replay its input sequence in a compatible simulation where practical.
5. Use reachability/cover checks to challenge assumptions that could make the asserted behavior vacuous.

Expected result: an evidence-backed statement about the written properties and configuration—not a claim that unspecified application behavior has been proven.

Example: a stalled output#

For a ready/valid stream register, a useful requirement is: while output valid is asserted and output ready is low, the next cycle retains valid and the same data, unless reset takes effect. A meaningful harness must allow backpressure. Assuming output ready is always high would remove the situation the property is intended to check.

The first-project directed test exercises one such stall. Formal exploration can address more sequences only within its model and assumptions. A cover witness that actually reaches the stalled state helps distinguish a useful property from one that never activates.

Check stall stability and reachability#

For an external SymbiYosys exercise, use the unchanged first-project RTL and compatible sby, Yosys, yosys-smtbmc and Z3 executables on PATH. Save these two files beside the RTL. The first sampled cycle assumes reset; thereafter reset, data, valid and ready are unconstrained. The assertions check only retained valid/data after a stalled cycle when that cycle did not reset the design.

module stream_formal(input logic clk);
  (* anyseq *) logic rst;
  (* anyseq *) logic [7:0] in_data;
  (* anyseq *) logic in_valid, out_ready;
  wire in_ready, out_valid;
  wire [7:0] out_data;
  stream_register dut(.*);
  reg past_valid = 0;
  always @(posedge clk) begin
    past_valid <= 1;
    if (!past_valid) assume(rst);
    if (past_valid && !$past(rst) &&
        $past(out_valid && !out_ready)) begin
      assert(out_valid);
      assert(out_data == $past(out_data));
    end
    cover(past_valid && !rst && out_valid && !out_ready);
  end
endmodule

[tasks]
prove
cover

[options]
prove: mode prove
cover: mode cover
depth 12

[engines]
smtbmc z3

[script]
read -formal stream_register.sv stream_formal.sv
prep -top stream_formal

[files]
stream_register.sv
stream_formal.sv

sby -f stream-stall.sby prove
sby -f stream-stall.sby cover

Expected result: both tasks finish PASS. The prove task must establish its assertions, not merely run to a bounded depth; read the terminal engine result. The cover task must find a reachable stalled output and retain its witness. Inspect that trace to confirm the scenario is meaningful. These properties do not prove accepted-byte ordering, throughput, every reset requirement or the absence of every bug.

Check the checker: in a separate disposable copy change else if (in_ready) to else if (1'b1) in the DUT. Run the prove task again and expect FAIL with a counterexample because output can change while stalled. Restore the original before further work. Each -f run replaces its same-named task output directory; copy results elsewhere before rerunning if you need to retain them. Timeout, unknown or a missing solver is not a proof failure or pass. Never weaken the property to make the defective copy pass.

Equivalence and comparisons#

For equivalence, inspect both compared designs, interface correspondence, reset assumptions and allowed differences. Matching outputs under an overconstrained environment is not general equivalence. A refactor can preserve behavior and still miss the product's intended requirement; compare requirements and independent application checks too.

When the flow is blocked#

If no current artifact exists, rerun after fixing the reported inputs/tool issue; do not relabel an old netlist as current. If proof times out, retain that result and reconsider the harness or decomposition without weakening the requirement silently. If an assertion fails, preserve the witness and determine whether the DUT, harness or requirement is wrong before modifying any of them.

Related: tool authority, verification verdicts, representation boundaries, example contracts.

Need help? Report an issue. Include your application version; never include credentials.