The App Map

One Narrow Question per App

A formal app is the three verbs (F1.3) packaged around one narrow question. Because the question is fixed, the tool can write the properties from a table, from the RTL itself or from a second design. The design can then be far larger than a hand-written proof could handle.

Each row of the map is built by hand in this module on the open engine, so you see exactly what the app generates and where it stops.

Who Writes the Rule

The generated group is where a team without a formal specialist starts: connectivity and registers turn an existing spreadsheet into a verdict. The hand-written group needs someone who can state the rule: which crossing protocol, which secret and sink, which symptom.

The trace above shows the difference. Two hand-written rows found the swapped pad: FAIL at reported step 2. In F5.3 a generator writes those rows from the pin table, along with the other seventeen.

Which App Catches Which Bug

An app proves its generated properties and nothing else. A narrow, fixed property set means a wrong spec stays wrong, and a bug outside the question is invisible. Use the apps for what they are good at, then write the properties only you can write.

Asked in Interviews

Try It

  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
    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);
  end

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

1. Run it

   Run as it is: FAIL at reported step 2. Which select value does the trace use?

2. Fix the mux

   Swap the two pad41 selects back in the RTL: BMC PASS to depth 20.

3. Count the rows

   How many rows like these would a 200-pin pad ring need? That is the case for a generator.

Check Yourself

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
    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);
  end
`endif
endmodule