System and process of extracting gate-level descriptions from simulation tables for formal verification

Abstract

A system and method for generating gate level descriptions tables from simulation for formal verification. Implementation libraries contain table-based descriptions of user defined primitives (UDPs), various-strength primitives, hierarchical structural cells and non-functional constructs, such as timing and simulation assertion checks. In order to use the library cells for use by test-generation (ATPG) and formal verification (FV), the present invention provides a library reader and a model builder that read in the library cells and construct gate-level models usable by ATPG processes. The present invention also provides a translator that accesses the ATPG models through an API (Application Programming Interface) interface and produces FV models that are usable by FV processes. Significantly, according to the present invention, the FV models are generated based on the ATPG models. Library cell complexities that would require different ATPG and FV models are automatically detected. Consequently, the single, common model is augmented with a few bits of extra information, or, in some cases, changed in a plurality of ways to accommodate different requirements of ATPG and FV.