DFT logic verification through property based formal methods — SOC to IP

摘要

System On Chips (SOCs) are being increasingly deployed in large number of applications and systems as they allow automation to be implemented to render ease and convenience in many human activities, a prime example being smart mobile phones. This renders their design implementation a fairly difficult task — with larger product space and product revisions, comes the requirement for larger feature integration in smaller die-sizes, smaller design turnaround times and lower power consumption. To address these issues, SOCs are being designed by integrating existing in house Intellectual Properties (IPs), or third party IPs provided by external vendors. DFT logic integration is an important design activity in any SOC design implementation, which gets carried out almost as a background activity, while not being accorded the due importance given to the prominent front-end design activity related to implementing functional features in the design of any SOC. Integration of DFT logic and the verification of this integration to other functional sub-systems and IPs in a SOC constitutes a significant portion of the overall design and verification effort. Any savings in this component helps in reducing the overall chip design and verification time and therefore, the cost. This is achievable through automation. The predominantly canonical and regular nature of the structures and behavior of most DFT IPs facilitates this, leading to the kind of convergence presently seen towards standardized configurable DFT logic architectures. Such standardized configurable DFT logic architectures lend themselves to auto-generation of their RTLs with ease. In addition, this feature enables high re-usability at different levels of hierarchy in any SOC design because similar DFT functionalities are needed, whether it be at the IP level, subsystem level or at the SOC level, albeit with increasing complexities in their functionality. Re-use further reduces the complexity, time and cost associa--ted with verification. In this paper, while we emphasize the verification task of DFT logic in an SOC at the RTL level, which constitutes a significant portion of the entire DFT logic verification task, there are several gate level DFT Logic verification tasks which are better suited to simulation (through TDLs). Even for such gate level verification tasks, ensuring a clean DFT logic integration at the RTL level helps in reducing the overall effort, as many errors at this level of hierarchy, using earlier approaches, are attributable to RTL level integration errors. The principal objective of the proposed approach has been to 1). Reduce simulation based DFT logic integration verification at the RTL level, 2). Improve robustness of Silicon quality by complete elimination of any bugs related to DFT logic, and 3). Enable re-use of DFT logic verification infrastructure across different SOCs and across different hierarchies within each SOC. These objectives have been achieved by taking the formal verification route with auto-generation of formal properties and the formal tool set up, on which the proof of these properties are executed. In this paper we give several examples which highlight our contributions to the above objectives across different hierarchies within an SOC and across different SOCs.