Earticle

초록

영어

This paper proposes a novel methodology 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.

목차

Abstract
 1. Introduction
 2. Preliminary Knowledge for LHPN
  2.1. Basics for LHPN
  2.2. LHPN model for tunnel diode oscillator
 3. Symbolic Description for Tunnel Diode Oscillator
 4. Formal Verification for Tunnel Diode Oscillator
 5. Experimental Results
 6. Conclusion
 Acknowledgements
 References

키워드

저자

• Jingbo Shao [ College of Computer Science and Information Engineering, Harbin Normal University, Harbin 150025, China , Postdoctoral Research Station of Information and Communication Engineering, Harbin Engineering University, Harbin 150001, China ]
• Jing Wu [ College of Zhengzhou Normal School for Kindergarten, Zhengzhou 450099, China ]
• Jingyu Liu [ College of Computer Science and Information Engineering, Harbin Normal University, Harbin 150025, China ] Corresponding author

참고문헌

발행기관

간행물

표지보기 관심저널 등록

• 간행물명

  International Journal of Control and Automation

• 간기

  월간

• pISSN

  2005-4297

• 수록기간

  2008~2016

• 십진분류

  KDC 505 DDC 605