Method and Infrastructure for Providing a Comprehensive RTL-to-Gates Formal Verification Flow
Publication Date: 2005-Dec-22
The IP.com Prior Art Database
· Control the RTL-to-gates compilation flow such that the netlist is in a verifiable format. · Generate and extract valuable information during compilation. Process, update, and enhance this information appropriately. · Provide information to the verification tool to enable successful verification and improved verification coverage. · Provide information to the user to assist with debugging and identification of problem areas.
Method and Infrastructure for
Providing a Comprehensive RTL-to-Gates Formal Verification Flow
- Control the RTL-to-gates compilation flow such that the netlist is in a verifiable format.
- Generate and extract valuable information during compilation. Process, update, and enhance this information appropriately.
- Provide information to the verification tool to enable successful verification and improved verification coverage.
- Provide information to the user to assist with debugging and identification of problem areas.
Today’s FPGAs contain more logic than ever thanks to ever shrinking process technologies. This enables customers to implement bigger and bigger designs on those FPGAs. Simultaneously, the compilation process i.e. the transformation of a customer’s RTL description of a design into a format that can be used to program the FPGA, becomes increasingly complicated as more and more options and flows are made available to customers to address the increasing need of trading off speed, area and power. This in turn increases the demand for testing the implementation correctness.
Even though an FPGA can be re-programmed if an error is detected later in the design flow, this is not true for the Structured ASIC and Structured ASICII device families. A design that has been fabricated cannot be changed anymore. Therefore, it is even more important for those device families that implementation errors are caught early in the development phase.
For all those and other reasons, customers want to verify the functional correctness of their design implementation. Formal methods are increasingly used for this purpose as they have several advantages compared to traditionally used methods such as simulation. Those advantages include shorter runtime, better coverage and no need for test vectors.
Formal verification has limitations though. When comparing the RTL level description of a design to the gate level implementation of that same design, formal verification heavily relies on information provided by the compilation tool that was used to implement the RTL code. This information includes, but is not limited to, state machine encoding, register duplication and merging, combinational loop detection, and redundant register removal. It also relies on the fact that the compilation tool doesn’t execute certain flows such as register retiming. Hierarchies of non-verifiable entities and modules also need to be preserved. We have solved these and other problems by adding special code to the compilation tool.
During the compilation process, we also record and process data that we make available to customers for assisting in identifying problems in the design and its implementation, as well as for resolving issues that have been discovered by the formal verification tool.
This is presented in more detail in the next section.
We added special code to the EDA CAD Tools compilation flow to support the subsequent formal...