AMS SoC Formal Verification based on Hybrid Scheme
This paper proposes for AMS SoC formal verification based on Hybrid Scheme combined with symbolic computing and LHPN model, FV-HS. The paper is concerned with a class of AMS designs, continuous-time AMS designs i.e., tunnel diode oscillator for research target. Firstly, Labeled Hybrid Petri Net model is established for safety property verification of tunnel diode oscillator, then mathematical expression for this model is extracted for efficiency enhancement, and then proof policy built in computer algebra Maple is applied to the corresponding LHPN model for tunnel diode oscillator to verify the property. The proposed method is implemented on tunnel diode oscillator and experiment results demonstrate the advantages of the proposed method over previous method. The proposed method overcomes the drawbacks of LHPN, makes full use of the merits of LHPN and symbolic computing, simplifies the workflow of algorithm and enhances the efficiency.
Gupta S., Krogh B. H., & Rutenbar R. A. (2004). Towards formal verification of analog designs. International Conference on Computer-Aided Design, 210-217
Dang T., Donze A., & Maler O. (2004). Verification of analog and mixed-signal circuits using hybrid systems techniques. Formal Methods for Computer Aided Design, 21-36.
Sebastian, S. & Lars, H. (2012). Trajectory-directed discrete state space modeling for formal verification of nonlinear analog circuits. IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, 202-209
Singh, A. K., Lok, M., Ragab, K., Caramanis, C., & Orshansky, M. (2010). An Algorithm for Exploiting Modeling Error Statistics to Enable Robust Analog Optimization, IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, 62-69
Al-Sammane, G., Zaki, & M.H.,Tahar, S. (2007). A symbolic methodology for the verification of analog and mixed signal designs. Proceedings of the conference on Design, automation and test in Europe, 249-254
Little,S., Walter, D., Myers, C., Thacker, R., Batchu, S., & Yoneda, T. (2011). Verification of analog/mixed-signal circuits using labeled hybrid Petri nets. IEEE Transactions on computer-aided design of integrated circuits and systems, 30(4), 617-630
Frehse, G., Krogh, B. H., & Rutenbar, R.A. (2006). Verifying analog oscillator circuits using forward/backward refinement. In Proc. Design, Automation and Test in Europe (DATE), IEEE Computer Society Press, 257-262.
Hartong, W., Hedrich, L., & Barke, E. (2002). Model checking algorithms for analog verification. Proceedings of DAC, 542-547.
Henzinger, T.A., Hho, P., & Wong-Toi, H. (1997). HyTech: a model checker for hybrid Systems. Software Tools for Technology Transfer [J], 110-122.
M. Alassir, J. Denoulet, O. Romain, & P. Garda. (2014). Signal integrityaware virtual prototyping of field bus-based embedded systems. IEEE Transactions on Components, Packaging and Manufacturing Technology, 3(12), 2081–2091.
Copyright (c) 2018 International Journal of Engineering and Management Research
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.