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 One-Hot Multiplexer: why assumptions

SystemVerilog Formal Verification

An AND-OR multiplexer that is correct only for one-hot selects. Remove the assumption to see a false failure.

Open in IDE
design.sv
// SVA form (used by commercial formal tools):
//   always_comb m_sel: assume ($onehot(sel));
//   always_comb if (sel[0]) a_y0: assert (y == d0);   // and so on for d1..d3
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module onehot_mux (input [3:0] sel, input [7:0] d0, input [7:0] d1, input [7:0] d2, input [7:0] d3,
                   output [7:0] y);
  // AND-OR multiplexer: correct only when sel is one-hot
  assign y = ({8{sel[0]}} & d0) | ({8{sel[1]}} & d1) | ({8{sel[2]}} & d2) | ({8{sel[3]}} & d3);

`ifdef FORMAL
  // the block that drives sel always selects exactly one input
  always @(*) assume ($onehot(sel));
  // the output is the selected input
  always @(*) if (sel[0]) assert (y == d0);
  always @(*) if (sel[1]) assert (y == d1);
  always @(*) if (sel[2]) assert (y == d2);
  always @(*) if (sel[3]) assert (y == d3);
`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.