Lesson 7.2 · Formal Apps for Everyday Problems

Connectivity verification

Chips contain thousands of top-level connections: pads multiplexed between functions, debug buses, interrupts, clock and reset distribution, power-management signals. Simulating every connection in every mode is tedious and easy to get wrong. Formal checks them exhaustively — and they are usually trivial proofs.

Example: a small pin multiplexer

pinmux.sv

// pinmux.sv — two pads shared between GPIO, UART, SPI and test functions
module pinmux (
  input  logic [1:0] mode,          // 0 GPIO, 1 UART, 2 SPI, 3 test
  input  logic       gpio_out0, gpio_out1,
  input  logic       uart_tx,
  input  logic       spi_sclk, spi_mosi,
  input  logic       test_obs0, test_obs1,
  output logic       pad0, pad1
);
  always_comb begin
    case (mode)
      2'd0:    begin pad0 = gpio_out0; pad1 = gpio_out1; end
      2'd1:    begin pad0 = uart_tx;   pad1 = 1'b1;      end  // pad1 idles high in UART mode
      2'd2:    begin pad0 = spi_sclk;  pad1 = spi_mosi;  end
      default: begin pad0 = test_obs0; pad1 = test_obs1; end
    endcase
  end
endmodule

The connectivity table

The integration team keeps the intended connections in a table. Each row: a condition, a source and a destination.

conn_spec.csv

# conn_spec.csv — condition, source, destination
mode == 2'd0, gpio_out0, pad0
mode == 2'd0, gpio_out1, pad1
mode == 2'd1, uart_tx,   pad0
mode == 2'd1, 1'b1,      pad1
mode == 2'd2, spi_sclk,  pad0
mode == 2'd2, spi_mosi,  pad1
mode == 2'd3, test_obs0, pad0
mode == 2'd3, test_obs1, pad1

A few lines of script turn the table into assertions. Real connectivity apps do the same, and also handle hierarchy paths and pipeline latency:

gen_conn.py

#!/usr/bin/env python3
"""gen_conn.py - generate SVA connectivity checks from conn_spec.csv
usage: python3 gen_conn.py conn_spec.csv > pinmux_conn_fv.sv"""
import csv, re, sys

rows = [r for r in csv.reader(open(sys.argv[1]))
        if r and not r[0].lstrip().startswith('#')]
out = ['// AUTO-GENERATED by gen_conn.py - do not edit by hand',
       'module pinmux_conn_fv (',
       '  input logic [1:0] mode,',
       '  input logic gpio_out0, gpio_out1, uart_tx, spi_sclk, spi_mosi, test_obs0, test_obs1',
       ');',
       '  logic pad0, pad1;',
       '  pinmux dut (.*);',
       '  always_comb begin']
for n, (cond, src, dst) in enumerate(rows):
    cond, src, dst = cond.strip(), src.strip(), dst.strip()
    label = 'a_conn_%d_%s_%s' % (n, re.sub(r'\W', '', src), dst)
    out.append('    if (%s) %s: assert (%s == %s);' % (cond, label, dst, src))
out += ['  end', 'endmodule']
print('\n'.join(out))

The generated wrapper looks like this (shortened):

pinmux_conn_fv.sv

// pinmux_conn_fv.sv - AUTO-GENERATED by gen_conn.py
module pinmux_conn_fv (
  input logic [1:0] mode,
  input logic gpio_out0, gpio_out1, uart_tx, spi_sclk, spi_mosi, test_obs0, test_obs1
);
  logic pad0, pad1;
  pinmux dut (.*);
  always_comb begin
    if (mode == 2'd0) a_conn_0_gpio_out0_pad0: assert (pad0 == gpio_out0);
    if (mode == 2'd0) a_conn_1_gpio_out1_pad1: assert (pad1 == gpio_out1);
    if (mode == 2'd1) a_conn_2_uart_tx_pad0:   assert (pad0 == uart_tx);
    if (mode == 2'd1) a_conn_3_1b1_pad1:       assert (pad1 == 1'b1);
    if (mode == 2'd2) a_conn_4_spi_sclk_pad0:  assert (pad0 == spi_sclk);
    if (mode == 2'd2) a_conn_5_spi_mosi_pad1:  assert (pad1 == spi_mosi);
    if (mode == 2'd3) a_conn_6_test_obs0_pad0: assert (pad0 == test_obs0);
    if (mode == 2'd3) a_conn_7_test_obs1_pad1: assert (pad1 == test_obs1);
  end
endmodule