The ifdef FORMAL Block and the Formal Wrapper

Properties have to live somewhere. They can sit inside the design file, guarded by `ifdef FORMAL, or in a separate file that leaves the design untouched. Commercial tools usually attach a separate property module with bind. The open-source front end in ChipVerify Lab does not support bind, so the lab uses a formal wrapper instead. This article explains all three approaches and when to use each.

8 min read | Beginner to Intermediate

What You'll Learn

• Explain what `ifdef FORMAL does and why properties are placed inside it
• Start a formal run from reset with an assumption, in two different ways
• Attach a property module to a design with bind
• Use the lab's formal wrapper, formal_props.sv, to check a design without editing it

Two Places for the Properties

Both places are common. Properties inside the design are close to the logic they describe and can use every internal signal. A separate file keeps the design clean, can be owned by a different engineer, and can be added to a design you are not allowed to change.

Inside the Design: `ifdef FORMAL

SymbiYosys reads every design file with the Yosys command read -formal. That command defines the macro FORMAL before it reads the file. Everything between `ifdef FORMAL and `endif is therefore seen by the formal tool and skipped by simulators and synthesis tools, which do not define the macro.

module sat_counter (input clk, input rst, input en, output reg [3:0] q);
  always @(posedge clk)
    if (rst)                    q <= 4'd0;
    else if (en && q != 4'd12)  q <= q + 4'd1;

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(posedge clk) if (!init) assert (q <= 4'd12);
`endif
endmodule

There are two reasons for the guard. Helper logic such as the init register must not end up in the chip. And synthesis tools and some simulators reject, or simply ignore, the formal statements assume and cover. With the guard, the same file goes through every tool.

The name of the macro is a convention, not a rule of the language. Commercial flows often use their own name, such as `ifdef ASSERT_ON. In the lab the formal tool defines FORMAL, so use that one.

Starting From Reset: Two Ways

A formal tool lets every register start at any value unless you say otherwise. To start from a reset, you assume that the reset is active in the first cycle. The init register above is one way: it is 1 only in the first cycle, and assume (rst) applies while it is 1.

The other way is an assumption in an initial block. Yosys treats it as a constraint on the very first cycle:

initial assume (rst == 1'b1);   // start in reset

Both give the same result. The init register has a second use: the assertions skip the first cycle with if (!init), because the values in that cycle are still the unknown start values. With the initial form, assertions are usually written as if (!rst) assert (...), which skips every reset cycle. That matches disable iff (rst) in SVA closely.

Outside the Design: bind

In SystemVerilog the usual way to attach properties from outside is bind. You write the properties in their own module, whose ports have the same names as signals in the design, and a bind statement places an instance of that module inside every instance of the design:

module sat_counter_sva (input clk, input rst, input en, input [3:0] q);
  a_max:  assert property (@(posedge clk) disable iff (rst) q <= 4'd12);
  a_stay: assert property (@(posedge clk) disable iff (rst) (q == 4'd12) |=> (q == 4'd12));
endmodule

bind sat_counter sat_counter_sva u_sva (.*);

The design file is not edited at all. The bound module sees the signals of the design as if it were written inside it, including internal signals if you list them as ports. All commercial formal tools and simulators support this, and it is the standard way to deliver properties for a design.

In ChipVerify Lab: the Formal Wrapper

The open-source Yosys front end does not implement bind. Worse, it does not reject it either: the bound module is never instantiated, so its assertions are never checked, and the run can pass without checking anything. The lab therefore uses a wrapper. The wrapper is a new top module that instantiates the design and checks its ports from the outside.

In the formal panel, the button Generate formal_props.sv creates the wrapper for the selected top module. For the saturating counter it looks like this, with the placeholder replaced by the real assertion:

module sat_counter_formal_top (
    input clk,
    input rst,
    input en,
    output [3:0] q
);

    sat_counter u_dut (
        .clk(clk),
        .rst(rst),
        .en(en),
        .q(q)
    );

    initial assume (rst == 1'b1);   // start in reset

    always @(posedge clk) begin
        if (!rst) begin
            assert (q <= 4'd12);
        end
    end

endmodule

The rules of the lab wrapper:

• The file is called formal_props.sv, and the module is named after the top module with _formal_top added.
• Keep Top Module set to the design, here sat_counter. When formal_props.sv exists, the lab reads it after the design files and checks the wrapper as the top module automatically.
• Only edit the assumptions and assertions. Keep the module name and the instance of the design.

On the lab engine this wrapper passes at depth 20. With the assertion changed to q <= 4'd11, it fails at step 14, the step after the counter first reaches 12. So the wrapper really is checked, unlike a bind in the open-source flow.

Which One to Use

The examples in this tutorial mostly use `ifdef FORMAL, because it keeps the design and its rules in one file and reaches internal state. The wrapper is the better choice when you check a design you did not write, or when the rules are only about the interface.

Running It in ChipVerify Lab

The example below contains the saturating counter without any properties, plus the wrapper formal_props.sv. Run it as it is, then change the limit in the wrapper and watch the result change. You can also delete formal_props.sv and click Generate formal_props.sv to see the template the lab creates.

Common Mistakes

always @(posedge clk) begin
    if (!rst && !$past(rst) && !$past(en)) begin
        assert (q == $past(q));
    end
end