Ready-to-run snippets

Code Examples

Ready-to-run Verilog, SystemVerilog, and UVM examples. Click any to open it live in the IDE.

← All examples

FV Pin Multiplexer: connectivity and reset (with a bug)

SystemVerilog Formal Verification

A 4-pad pin multiplexer checked against its connectivity table and reset values. One pad is missing from the reset.

Open in IDE
design.sv
// SVA form of one connectivity row and the reset check:
//   a_uart: assert property (@(posedge clk) disable iff (rst) !test_mode && sel[pd] == 2'd1 |-> pad_out[pd] == uart_tx);
//   a_rst:  assert property (@(posedge clk) $fell(rst) |-> sel[pd] == 2'd0 && pad_oe == 4'b0000);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
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

`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
endmodule
Admin mode — edit and delete controls are visible on each row. Use the IDE to add new snippets via File → Save as Snippet.