Connectivity

Turn a connection table into one property per row, find a swapped pad pair in one step, and meet the three ways a connectivity run can mislead.

Lesson: F5.3
Time: 15 min
Runs on: SymbiYosys
Check: 4 questions

A chip came back with its UART silent: a late edit had swapped two pad-select values. The loopback test passed, because both ends were wrong the same way. The pin list existed as a spreadsheet, and nobody had asked a tool to check the RTL against it.

One step after reset, the wrong pad

Measured with smtbmc yices at depth 20, RTL selects swapped. The solver needs one step out of reset and different values on uart_tx and spi_mosi. Sampled at step 1, reported at 2.

One Row, One Property

Row (src, dst, cond, delay)	Generated SVA	As this engine runs it
`src[3], dst[3], , 0`	`dst[3] == src[3]`	`assert(dst[3] == src[3]);`
`uart_tx, pad41, pad_sel == 1, 0`	`pad_sel == 2'd1 \|-> pad41 == uart_tx`	`if (pad_sel == 2'd1) assert(pad41 == uart_tx);`
`pipe_in, pipe_out, , 1`	`pipe_out == $past(pipe_in)`	`if (!rst_q) assert(pipe_out == pipe_in_q);`
every distinct condition	`cover property (pad_sel == 2'd1)`	`cover(pad_sel == 2'd1);`

The generator is a loop over rows: 19 asserts and 4 covers for this top. $past on an input is refused here, so the registered row reads a copy, pipe_in_q.

Connectivity is the simplest formal question: is pin A wired to pin B? Each row of the table names a source, a destination, a condition and a delay. A straight wire becomes an equality. A mux path adds its select as an antecedent. A registered path compares with last cycle's source.

The covers are the half people forget. A conditional row whose condition can never hold passes for nothing (F3.2). The generator writes one cover per distinct condition, and all 4 are reached at reported step 2.

The Swap in One Step

conn_top: What the Table DescribesTwelve straight wires, two pad muxes sharing one select, one registered path. Arrows mean "drives".

Read the diagram as text

src[11:0]: twelve block outputs
uart_tx, spi_mosi, gpio_o: functions that share two pads
pipe_in: a registered path
pad mux, pad_sel[1:0]: select 1: UART on pad41, SPI on pad42; select 2: the reverse
dst[11:0]: straight wires
pad41, pad42: the chip pins
pipe_out: one flop later

src[11:0] → dst[11:0]
uart_tx, spi_mosi, gpio_o → pad mux, pad_sel[1:0]
pad mux, pad_sel[1:0] → pad41, pad42
pipe_in → pipe_out: 1 cycle

A late edit swaps the UART and SPI select values on pad41. Every block-level test still passes; only the top level is wrong.

Run	Measured result	Failing row	Time
Table right, RTL right	BMC PASS to depth 20	none	580 ms
Table right, RTL selects swapped	FAIL at reported step 2	pad41 at select 2	516 ms
Table rows swapped, RTL right	FAIL at reported step 2	pad41 at select 2	515 ms

smtbmc yices, mode bmc, depth 20, 19 generated asserts, reset assumed in step 0.

A wiring bug needs no sequence, so the trace is one step long. That is why teams run connectivity first on a large SoC: trivial depth, properties from a table, a verdict in under a second here.

The two broken runs fail the same way. The trace cannot say whether the RTL or the table is wrong; only the spec can. Note too that bmc stops at the first counterexample: one row is reported, although both pad41 rows are wrong. Fix it and run again to find the next.

Three Ways It Misleads

Trap	Measured on conn_top	What to do
A registered row checked during reset	FAIL at reported step 2: step 1 compares `pipe_out`, still the reset value, with `pipe_in` from the reset step	gate the row on last cycle being out of reset (`rst_q`)
A row naming a pin that does not exist	`dst[12]` on a 12-bit bus: BMC PASS to depth 20; Yosys only warns "Range select out of bounds"	check every table name against the netlist before the run
A select written by a register	the row needs the register programmed first, which can make a shallow check deep	cut the register free and assume it constant per run

The second trap is the dangerous one: an out-of-range select reads undefined on both sides, and the row passes without comparing any wire.

Real top levels add pad cells written for electrical simulation, which formal tools cannot read, and mode pins such as scan that must be tied off by assumption. Each is a modelling task before the first run, not a property to write.

Asked in Interviews

Question	Answer
How is connectivity verified formally?	A table of source, destination, condition and delay; one generated property per row, a cover per condition, and a shallow bmc.
What goes wrong?	Rows checked during reset, names that do not exist, selects behind registers, unreachable conditions, and pad cells or mode pins the model cannot read.
Why first on an SoC?	No properties to write, trivial depth, and it catches integration bugs that block-level verification cannot see.

Try It

The table (CSV)

src,dst,cond,delay
src[0],dst[0],,0
src[1],dst[1],,0
gpio_o[0],pad41,pad_sel == 2'd0,0
uart_tx,pad41,pad_sel == 2'd1,0
spi_mosi,pad41,pad_sel == 2'd2,0
gpio_o[1],pad42,pad_sel == 2'd0,0
spi_mosi,pad42,pad_sel == 2'd1,0
uart_tx,pad42,pad_sel == 2'd2,0
pipe_in,pipe_out,,1

Two of the twelve straight rows shown; the generator reads all of them.

The generator

rows.map(([src, dst, cond, delay]) =>
  delay ? `if (!rst_q) assert(${dst} == ${src}_q);`
  : cond ? `if (${cond}) assert(${dst} == ${src});`
  : `assert(${dst} == ${src});`)

A loop over rows; the covers are one more loop over the conditions.

The bench the generator writes: reset assumption, two history flops, nineteen rows.

  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg pipe_in_q=0, rst_q=1;   // last cycle's pipe_in and rst
  always @(posedge clk) begin pipe_in_q <= pipe_in; rst_q <= rst; end
  // generated from the connection table
  always @(posedge clk) if (!rst) begin
    assert(dst[0] == src[0]);
    assert(dst[1] == src[1]);
    assert(dst[2] == src[2]);
    assert(dst[3] == src[3]);
    assert(dst[4] == src[4]);
    assert(dst[5] == src[5]);
    assert(dst[6] == src[6]);
    assert(dst[7] == src[7]);
    assert(dst[8] == src[8]);
    assert(dst[9] == src[9]);
    assert(dst[10] == src[10]);
    assert(dst[11] == src[11]);
    if (pad_sel == 2'd0) assert(pad41 == gpio_o[0]);
    if (pad_sel == 2'd1) assert(pad41 == uart_tx);
    if (pad_sel == 2'd2) assert(pad41 == spi_mosi);
    if (pad_sel == 2'd0) assert(pad42 == gpio_o[1]);
    if (pad_sel == 2'd1) assert(pad42 == spi_mosi);
    if (pad_sel == 2'd2) assert(pad42 == uart_tx);
    if (!rst_q) assert(pipe_out == pipe_in_q);
  end

The whole task. Run the covers with mode cover.

[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top conn_top
[files]
design.sv

Run the swap
Run as it is: FAIL at reported step 2. Read the select value in the trace and the pad that carries uart_tx.
Blame the table instead
Fix the RTL, then swap the two pad41 rows in the generated block. Run. Could the trace alone tell you which was wrong?
Add a row
Add assert(dst[12] == src[12]); and run. Then read the elaboration warning in the log.
Remove the guard
Delete if (!rst_q) from the registered row and run: FAIL at reported step 2. Is that an RTL bug?

Top moduleModeDepthEngine

design.sv

props.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

Enable JavaScript to edit and run. The original design and properties follow.

module conn_top(input clk, rst, input [11:0] src, input uart_tx, spi_mosi, input [1:0] gpio_o,
  input [1:0] pad_sel, input pipe_in, output [11:0] dst, output pad41, pad42, output reg pipe_out=0);
  assign dst = src;
  assign pad41 = pad_sel == 2'd0 ? gpio_o[0] : pad_sel == 2'd1 ? spi_mosi : pad_sel == 2'd2 ? uart_tx : 1'b0;   // bug: 1 and 2 swapped
  assign pad42 = pad_sel == 2'd0 ? gpio_o[1] : pad_sel == 2'd1 ? spi_mosi : pad_sel == 2'd2 ? uart_tx : 1'b0;
  always @(posedge clk) pipe_out <= rst ? 1'b0 : pipe_in;
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg pipe_in_q=0, rst_q=1;   // last cycle's pipe_in and rst
  always @(posedge clk) begin pipe_in_q <= pipe_in; rst_q <= rst; end
  // generated from the connection table
  always @(posedge clk) if (!rst) begin
    assert(dst[0] == src[0]);
    assert(dst[1] == src[1]);
    assert(dst[2] == src[2]);
    assert(dst[3] == src[3]);
    assert(dst[4] == src[4]);
    assert(dst[5] == src[5]);
    assert(dst[6] == src[6]);
    assert(dst[7] == src[7]);
    assert(dst[8] == src[8]);
    assert(dst[9] == src[9]);
    assert(dst[10] == src[10]);
    assert(dst[11] == src[11]);
    if (pad_sel == 2'd0) assert(pad41 == gpio_o[0]);
    if (pad_sel == 2'd1) assert(pad41 == uart_tx);
    if (pad_sel == 2'd2) assert(pad41 == spi_mosi);
    if (pad_sel == 2'd0) assert(pad42 == gpio_o[1]);
    if (pad_sel == 2'd1) assert(pad42 == spi_mosi);
    if (pad_sel == 2'd2) assert(pad42 == uart_tx);
    if (!rst_q) assert(pipe_out == pipe_in_q);
  end
`endif
endmodule

Check Yourself

Predict the outputconn_top with the RTL selects swapped on pad41, mode bmc, default depth 20, smtbmc yices, reset assumed in step 0, the nineteen generated asserts. At which reported step does it fail?

module conn_top(input clk, rst, input [11:0] src, input uart_tx, spi_mosi, input [1:0] gpio_o,
  input [1:0] pad_sel, input pipe_in, output [11:0] dst, output pad41, pad42, output reg pipe_out=0);
  assign dst = src;
  assign pad41 = pad_sel == 2'd0 ? gpio_o[0] : pad_sel == 2'd1 ? spi_mosi : pad_sel == 2'd2 ? uart_tx : 1'b0;   // bug: 1 and 2 swapped
  assign pad42 = pad_sel == 2'd0 ? gpio_o[1] : pad_sel == 2'd1 ? spi_mosi : pad_sel == 2'd2 ? uart_tx : 1'b0;
  always @(posedge clk) pipe_out <= rst ? 1'b0 : pipe_in;
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg pipe_in_q=0, rst_q=1;   // last cycle's pipe_in and rst
  always @(posedge clk) begin pipe_in_q <= pipe_in; rst_q <= rst; end
  // generated from the connection table
  always @(posedge clk) if (!rst) begin
    assert(dst[0] == src[0]);
    assert(dst[1] == src[1]);
    assert(dst[2] == src[2]);
    assert(dst[3] == src[3]);
    assert(dst[4] == src[4]);
    assert(dst[5] == src[5]);
    assert(dst[6] == src[6]);
    assert(dst[7] == src[7]);
    assert(dst[8] == src[8]);
    assert(dst[9] == src[9]);
    assert(dst[10] == src[10]);
    assert(dst[11] == src[11]);
    if (pad_sel == 2'd0) assert(pad41 == gpio_o[0]);
    if (pad_sel == 2'd1) assert(pad41 == uart_tx);
    if (pad_sel == 2'd2) assert(pad41 == spi_mosi);
    if (pad_sel == 2'd0) assert(pad42 == gpio_o[1]);
    if (pad_sel == 2'd1) assert(pad42 == spi_mosi);
    if (pad_sel == 2'd2) assert(pad42 == uart_tx);
    if (!rst_q) assert(pipe_out == pipe_in_q);
  end
`endif
endmodule

ConceptWhy is a top-level pin table checked by formal rather than by simulation?

Simulation cannot drive or read the chip pads at all.Rows become properties, depth is one step, every select at once.Formal is faster than simulation on any large design.The pads are asynchronous, so simulation cannot sample them.

ConceptA row for dst[12] on a 12-bit bus passed. What happened?

The RTL has a hidden thirteenth wire that matches.The cover for that row was reached, so the row is proven.Both sides read out of range, so no wire was compared.bmc stopped at the first failure on another row.

Read the waveformIn the swap trace, at the sampled failing step, which function is on pad41?

One step after reset, the wrong pad

Measured with smtbmc yices at depth 20, RTL selects swapped. The solver needs one step out of reset and different values on uart_tx and spi_mosi. Sampled at step 1, reported at 2.

gpio_o[0], the select-0 functionConstant 0, the select-3 valuespi_mosi, as the table saysuart_tx, meant for select 1

Remember

Connectivity turns each table row into one property: equality, conditional equality, or equality with last cycle.
A wiring bug fails one step out of reset; depth does not matter when the cone is a wire.
Write a cover per condition, gate registered rows on reset, and check every table name against the netlist.
The trace shows the RTL and the table disagree; only the spec says which is wrong.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.