|
Hardware Verification Group |
|
Concordia University |
|
Analog and Mixed Signal (AMS) designs are an important part of embedded systems that link digital designs to the analog world. The verification of AMS designs is concerned with the assurance of correct functionality, in addition with checking whether an AMS design is robust with respect to different types of inaccuracies like parameters tolerances, nonlinearities, etc. In this project, we propose to develop approaches for the verification of different classes of AMS designs using formal and semi-formal methods. To this aim, we consider three research directions: The first proposed method is based on the computation of finite-state conservative abstraction of AMS designs. We use predicate abstraction to guarantee property preservation by the abstract model. We are mainly interested in systems with nonlinear dynamics, where the generated model is combined with the discrete model along with the environment constraints to be verified by conventional model checker algorithms. Due to the over-approximation of the abstraction, some properties are difficult to verify using this method; we overcome such limitation by developing a bounded model checking (BMC) approach. The principle of BMC is to search for a counter-example for a property that can be checked against the model for bounded k-steps over interval based domains. We extended the BMC with an induction based verification engine to prove properties for class of AMS described using difference equations. Another direction we pursue by developing a program monitoring (run-time verification) approach. Run-time verification is a technique for checking whether an execution of the design model under verification violates the given properties. No computational model needs to be generated prior to the verification, avoiding state space explosion. By employing logical monitors, an efficient analysis of the results is achieved, avoiding exhaustive inspection, by testing whether a given behavior satisfies a property. We tested and validated our approaches on systems like oscillator circuits, witched capacitor based designs, PLL designs, and Delta-Sigma modulators. |
|
|
， M. Zaki, G. Al Sammane, Z.J. Dong, S. Tahar, and G. Bois: Techniques for the Formal Verification of Analog and Mixed-Signal Designs; Proc. 77th ACFAS Symposium (ACFAS'09), Ottawa, Canada, May 2009. |
|
|
， R. Narayanan, N. Abbasi, M. Zaki, G. Al Sammane, and S. Tahar: On the Simulation Performance of Contemporary AMS Hardware Description Languages; Proc. IEEE International Conference on Microelectronics (ICM'08), Sharjah, UAE, December 2008. |
|
|
， R. Narayanan, N. Abbasi, G. Al Sammane, M. Zaki, and S. Tahar: A Comparative Study of AMS Circuit Simulation in VHDL-AMS and SystemC-AMS; Proc. International Conference on Embedded Systems & Critical Applications (ICESCA'08), Gammarth, Tunisia, May 2008, pp. 23-28. |
|
|
， W. Denman, M. Zaki and S. Tahar: A Bond Graph Approach for the Constraint based Verification of Analog Circuits; Proc. Workshop on Formal Verification of Analog Circuit (FAC'08), July 2008, Princeton, New Jersey, USA. |
|
|
， M. Zaki, S. Tahar, and G. Bois: Qualitative Abstraction based Verification for Analog Circuits; Proc. Workshop On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'07), Poitier, France, December 2007, IEEE Computer Society Press. |
|
|
， Z.J. Dong, M.H. Zaki, G. Al Sammane, S. Tahar and G. Bois: Checking Properties of PLL Designs using Run-time Verification; Proc. IEEE International Conference on Microelectronics (ICM'07), Cairo, Egypt, December 2007 |
|
|
， M. Zaki, G. Al Sammane, S. Tahar, and G. Bois: Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs; Proc. IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD'07), Austin, Texas, USA, November 2007, IEEE Computer Society Press. pp. 207-215. |
|
|
， G. Al Sammane, M.H. Zaki, Z.J. Dong and S. Tahar: Towards Assertion Based Verification of Analog and Mixed Signal Designs Using PSL; Proc. Languages for Formal Specification and Verification, Forum on Specification & Design Languages (FDL'07), Barcelona, Spain, September 2007. pp. 293-298 |
|
|
， G. Al Sammane, M. Zaki, S. Tahar, and G. Bois: Constraint-Based Verification of Delta Sigma Modulators Using Interval Analysis; Proc. IEEE Midwest Symposium on Circuits & Systems (MISWEST'07), Montreal, Quebec, Canada, August 2007, pp. 726-729. |
|
|
， Z.J. Dong, M. Zaki, G. Al Sammane, S. Tahar, and G. Bois: Run-Time Verification using the VHDL-AMS Simulation Environment; Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'07), Montreal, Quebec, Canada, August 2007, 1513-1516. |
|
|
， M. Zaki, S. Tahar, and G. Bois: A Symbolic Approach for the Safety Verification of Continuous Systems; Proc. International Conference on Computational Science (ICCS'07), Beijing, China, May 2007, pp. 93-100. |
|
|
， M. Zaki, G. Al Sammane, and S. Tahar: Formal Verification of Analog and Mixed Signal Designs in Mathematica; In: Y. Shi et al. (Eds.), Computational Science, Lecture Notes in Computer Science 4488, Springer Verlag, 2007, pp. 263-267. [Proc. International Conference on Computational Science (ICCS'07), Beijing, China, May 2007] |
|
|
， G. Al Sammane, M. Zaki, and S. Tahar: A Symbolic Methodology for the Verification of Analog and Mixed Signal Designs; Proc. IEEE/ACM Design Automation and Test in Europe (DATE'07), Nice, France, April 2007. |
|
|
， M. Zaki, S. Tahar, and G. Bois: Abstraction Based Verification of Analog Circuits Using Computer Algebra and Constraint Solving; Proc. IEEE International Workshop on Symbolic Methods and Applications to Circuit Design (SMACD'06), Florence, Italy, October 2006. |
|
|
， M. Zaki, S. Tahar, and G. Bois: Formal Verification of Analog and Mixed Signal Designs: Survey and Comparison; Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'06), Gatineau, Quebec, Canada, June 2006. |
|
|
， M. Zaki, S. Tahar, and G. Bois: A Practical Approach for Monitoring Analog Circuits; Proc. ACM 16th Great Lakes Symposium on VLSI (GLS-VLSI'06), Philadelphia, Pennsylvania, USA, April 2006, ACM Publications. |
|
|
， M. Zaki, S. Tahar, and G. Bois: On the formal Analysis of Analog Systems using Interval Abstraction; Proc. NETCA Workshop on Verification and Theorem Proving for Continuous Systems, Oxford, UK, August 2005. |
|
|
， M. Zaki, W. Denman, S. Tahar, and G. Bois: Integrating Abstraction Techniques for the Formal Verification of Analog Designs; American Institute of Aeronautics and Astronautics Journal, AIAA. In-Print [26 pages] |
|
|
， M. Zaki, S. Tahar and G. Bois: Formal Verification of Analog and Mixed Signal Designs: A Survey; Microelectronics Journal, Vol. 39, No. 12, Elsevier B.V. Pub., December 2008, pp. 1395-1404. |
|
|
， M. Zaki, S. Tahar, and G. Bois: Qualitative Abstraction based Verification for Analog Circuits; Revue des Nouvelles Technologies de l'information, Vol. 4, Issue ,December 2007, RNTI-SM-1, Edition Cepadues, pp. 147-158. |
|
|
， Z. J. Dong, M.H. Zaki, G. Al Sammane, S. Tahar and G. Bois. A Run-Time Verfication Approach for AMS Designs. Technical Report, Department of Electrical and Computer Engineering, Concordia University, July 2007. [16 Pages]. |
|
|
， M.H. Zaki, S. Tahar and G. Bois: Combining Constraint Solving and Formal Methods for the Verification of Analog Designs; Technical Report, Concordia University, Department of Electrical and Computer Engineering, June 2007. [28 Pages] |
|
|
， M.H. Zaki, G. Al Sammane, S. Tahar and Guy Bois: A Bounded Model Checking Approach for AMS Designs; Technical Report, Concordia University, Department of Electrical and Computer Engineering, May 2007. [22 Pages] |
|
|
， M.H. Zaki, S. Tahar, G. Bois: A Survey on Formal Methods for Analog and Mixed Signal Designs, Technical Report, ECE Dept, Concordia University, 2006 [16 Pages] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
， Mohamed Hamed Zaki Hussein, ＾ Techniques for the Formal Verification of Analog and Mixed- Signal Designs￣, Ph.D. Department of Electrical and Computer Engineering, Concordia University, September 2008. |