Advances in Engineering Advances in Engineering features breaking research judged by Advances in Engineering advisory team to be of key importance in the Engineering field. Papers are selected from over 10,000 published each week from most peer reviewed journals.
Journal of Electronic Testing, 2013, Volume 29, Issue 5, pp 715-740.
Kusum Lata, Subir K. Roy.
Indian Institute of Information Technology (IIIT), Allahabad, Uttar Pradesh, India and
International Institute of Information Technology (IIIT), Bangalore, Karnataka, India.
Abstract
Analog and Mixed Signal (AMS) designs can be formally modeled as hybrid systems [45] and therefore formal verification techniques applicable to hybrid systems can be deployed to verify them. An extension to a formal verification approach applicable to hybrid systems is proposed to verify AMS designs [31]. In this approach formal verification (FV) is carried out on an AMS block using simulation traces from SPICE, a simulator widely used in the design and verification of analog and AMS blocks. A broader implication of this approach is the ability to carry out hierarchical verification using relevant simulation traces obtained at different abstraction levels of a design when modeled in appropriate platforms. This enables a seamless transition of design and verification artifacts from the highest level of abstraction to the lowest level of implementation at the transistor level of any AMS design and a resulting increase in confidence on the correctness of the final implementation. The proposed approach has been justified with its applications to different AMS design blocks. For each design, its formal model and the proposed computational techniques have been incorporated into CheckMate [11] – a FV tool for hybrid systems based on MATLAB and the Simulink/Stateflow framework from MathWorks. A further justification of the proposed approach is the resulting improvements observed in terms of reduced verification time for different specifications in each design.
Additional Information
Future Work:
We are focusing on the following aspects towards extending the work presented in the paper in the area of formal verification of analog and mixed signal designs.
- Explore the feasibility of using temporal logic, other than ACTL, to capture the formal specifications of AMS designs. These could be extensions of PSL and SVA used extensively in the formal verification of digital circuits.
- Explore different approaches in the construction of flow- pipe approximations based on different geometrical shapes to improve the computational efficiency of the underlying formal analysis engine to enable us to target the formal verification of large sized industrial strength AMS circuits.
- Attempt non-flow pipe based formal analysis of AMS circuits using techniques such as trajectory directed state space modeling.
- Carry out time domain sensitivity analysis to reduce the size of state space variables on which properties will be needed to be written.
- Implementation of refinement during formal analysis/verification of analog mixed signal designs using SPICE simulation traces in our set up to enable us to validate and/or choose the ICS (Initial Continuous Set ) and the analysis region.
- To extend the development of a benchmark suite consisting of several industrial strength AMS circuit designs to study the efficacy of different flow-pipe over- approximation approaches, algorithms and property verification. During the work described in the paper, a significant amount of time was devoted to developing relevant examples of hybrid systems and analog mixed signal designs to analyze and verify using formal approaches. This will extensively benefit researchers working in this domain and help drive the quality of research in the formal verification of analog and mixed signal designs.
