Connectivity and Reset Checks

A chip has thousands of connections that must be exactly right: every peripheral signal to the right pad through the pin multiplexer, every interrupt to the right controller input, test signals routed only in test mode. And every configuration register must come out of reset with its specified value. These checks are so regular that formal tools offer them as apps: you provide a table, the tool generates and proves the properties. This article writes such checks by hand for a pin multiplexer and finds a register that is missing from the reset.

8 min read | Intermediate

What You'll Learn

• Turn a connectivity table into properties
• Check every pad with one symbolic index
• Write reset-value checks for configuration registers
• Find a register that the reset does not cover

Connectivity as Properties

A connectivity specification is usually a table: "when pad 2 is configured as SPI MOSI, the pad carries spi_mosi". Each row becomes one implication: under the configuration condition, the destination equals the source. A connectivity app reads the table, often a spreadsheet, and generates these assertions automatically; a formal engine then proves them through all the multiplexers, test logic and debug logic in between.

The Design: a Pin Multiplexer

module pinmux (input clk, input rst,
               input cfg_we, input [1:0] cfg_pad, input [1:0] cfg_val,
               input test_mode, input scan_out,
               input uart_tx, input spi_mosi, input spi_sck, input [3:0] gpio_out,
               output [3:0] pad_out, output [3:0] pad_oe);
  // each pad has a 2-bit function select: 0 = GPIO, 1 = UART TX, 2 = SPI MOSI, 3 = SPI SCK
  reg [1:0] sel [0:3];
  reg [3:0] oe;
  integer i;
  always @(posedge clk)
    if (rst) begin
      for (i = 0; i < 3; i = i + 1) sel[i] <= 2'd0;     // bug: pad 3 is left out of the reset
      oe <= 4'b0000;
    end else if (cfg_we) begin
      sel[cfg_pad] <= cfg_val;
      oe[cfg_pad]  <= 1'b1;
    end
  genvar k;
  generate for (k = 0; k < 4; k = k + 1) begin : pads
    wire f = (sel[k] == 2'd0) ? gpio_out[k] :
             (sel[k] == 2'd1) ? uart_tx :
             (sel[k] == 2'd2) ? spi_mosi : spi_sck;
    assign pad_out[k] = test_mode ? (k == 0 ? scan_out : 1'b0) : f;
    assign pad_oe[k]  = test_mode ? (k == 0) : oe[k];
  end endgenerate
endmodule

The reset loop stops one pad short, a typical off-by-one in a loop bound. Pad 3 then comes out of reset with a random function, and when software enables it, it may drive SPI or UART signals where a GPIO was expected.

The Properties

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // connectivity table, checked for a symbolic pad
  (* anyconst *) reg [1:0] pd;
  always @(*) if (!init && !test_mode && sel[pd] == 2'd0) assert (pad_out[pd] == gpio_out[pd]);
  always @(*) if (!init && !test_mode && sel[pd] == 2'd1) assert (pad_out[pd] == uart_tx);
  always @(*) if (!init && !test_mode && sel[pd] == 2'd2) assert (pad_out[pd] == spi_mosi);
  always @(*) if (!init && !test_mode && sel[pd] == 2'd3) assert (pad_out[pd] == spi_sck);
  always @(*) if (!init && test_mode) assert (pad_out[0] == scan_out);
  // reset values: right after reset every pad is GPIO and every output driver is off
  always @(posedge clk) if (!init && $past(rst)) assert (sel[pd] == 2'd0 && pad_oe == 4'b0000 || test_mode);
`endif

The symbolic pad pd, from the symbolic values article, lets five assertions cover all four pads. The run fails at step 2, with pd = 3: right after reset, sel[3] is not 0. The connectivity rows pass: the multiplexer routes correctly for whatever sel holds. With the loop bound fixed to i < 4, everything passes.

Reset Checks

A reset app checks that every register listed in the specification has its reset value one cycle after reset, and often also lists registers without a reset, so a human can confirm each one is intentional. Written by hand, the rule is $fell(rst) |-> reg == RESET_VALUE, or in the lab form a check in the cycle after rst. The reset check here also covers the output enables: with all drivers off after reset, no pad fights an external signal before software has configured it.

If the connectivity table swapped two sources, for example SPI MOSI and SCK, the connectivity rows would fail instead, at step 2, with the pad configured to the swapped function.

Running It in ChipVerify Lab

The example below is the pin multiplexer with the reset bug and all properties. It fails at step 2 within the free depth.

Common Mistakes