Given the size and complexity of today’s FPGA designs, it is increasingly common for some form of design verification to be performed throughout the FPGA design process. While simulation and prototyping remain the standards for validating design functionality, verifying the FPGA netlist at various stages in the design flow has become increasingly important because of the logic manipulations that occur during FPGA synthesis. For this reason, formal verification (FV), a process by which the integrity of a design netlist is verified, has become a critical element in a FPGA design flow.

 

FPGA designers historically used ASIC design verification processes such as simulation to verify a design. While simulation is a valuable tool for verifying FPGA design functionality, it is time consuming and limited in its ability to fully test a design, depending upon the test stimulus supplied for the design. Because FPGAs are reprogrammable, though, designers historically did not simulate a synthesized FPGA netlist, and instead verified the design by testing it in the system board. As long as designs were relatively small in size, this “trial and error” methodology was fairly low risk.

 

With FPGA design complexity and size increasing into the multi-million gate range, synthesis is becoming much more complex, and verifying a synthesized FPGA netlist is increasingly important, particularly after synthesis, placement and routing. Though an FPGA design flow closely parallels that of an ASIC, the need for formal verification is substantially greater for a complex FPGA.

 

An ASIC netlist remains practically unchanged during synthesis. There is far less mapping involved in synthesizing an ASIC design -- sequential optimizations are limited in an ASIC flow because the mapping to flip-flops and primitives in the ASIC library must be retained, making an ASIC formal verification flow cleaner and more likely to converge that that of an FPGA. By contrast, implementing very specialized blocks such as DSP functions or a memory blocks in an FPGA gives the FPGA synthesis tool more latitude to perform extensive optimization when mapping those functions to primitives. The result is a highly optimized design, but with a gate-level netlist that can differ significantly from an equivalent ASIC gate netlist.

 

Thus, verifying an FPGA netlist at different stages of the design flow has become an imperative.   Compared to simulation and other functional verification methods, formal verification is significantly faster and provides complete netlist coverage. Formal verification uses formal techniques and static verification methods to prove netlist equivalence to the “golden” RTL representation of the design, and is a highly effective means to verify design integrity after synthesis and/or place and route. Formal verification simply verifies whether two netlists are equivalent, so it does not replace function verification performed by simulation in a design flow.

 

 
 

 

Post-synthesis logic equivalence checking can be described in terms of the three formal verification steps shown in Figure 1.

 

Parsing during formal verification involves reading the reference (post-synthesis) and the golden (RTL) netlists and generating key points for both netlists. Key points are the inputs, outputs, flip-flops, and black boxes in the design.

 

Mapping involves establishing a one-to-one correspondence between the pre- and post-synthesis netlists. This one-to-one mapping ensures that each key point in netlist A has an equivalent key point in netlist B. Once this correspondence is accomplished for all design key points, the design is considered completely mapped. It is very important for the design to be completely and correctly mapped before advancing to the comparison phase of the process.

 

This final stage of formal verification involves comparing whether the input cones to each key point are the same in both netlists. The input cone (combinatorial) for each key point in a design is compared to the corresponding input logic cone and key point in the equivalent design. If all the logic cones are equal, the design is considered equivalent.

During post-synthesis FPGA formal verification, though, problems can arise in the mapping and the comparison stages of the process. Once identified, however, these problems can be remedied by applying some simple techniques and best practices. Common mapping convergence issues are discussed below.

 

Most mapping issues are the result of a mismatch between names of instances/registers in RTL and the synthesized netlist. The primary sources of mismatch are register/instance names associated with VHDL record types, generated instance/register names, Verilog, arrays of instances, recursive instances, and multidimensional array ports.

 

Consider the following VHDL record type example:

 

 

In this example, synthesis instance mydata of record type can be named mydata (19 downto 0), where the MSB corresponds to Addr and lower (15:0) bits correspond to Data. The formal verification instance mydata of record type can be named mydata_rec (19 downto 0) with the MSB (15:0) corresponding to Data and the lower bits (3:0) corresponding to Addr.

 

Such naming conventions must be recognized and mapped correctly using naming rules for unmapped points in the FV environment. Most synthesis tools maintain a reference file that shows the mapping of buses in such cases, and this can be used as a guideline for the FV tool.

 

Naming rules can apply to a register/instance. Alternatively, a generic naming rule using regular expressions to encompass all instances in that group can be applied. Usually, generic naming rules yield better runtimes in FV tools than individual naming rules.