Earticle

초록

영어

This paper proposes a new scalable approach to formal verification (SFV) for AMS SoC designs. Induction rules defined in computer symbolic algebra system Maple are followed to extract representation of property of AMS SoC, constraints solving is performed to formally verify the correctness of the system with respect to its given property. With an AMS description and a set of properties, SMT based model checker is applied to validate if the given system has a certain properties. The proposed methodology is applied on a tunnel diode oscillator. Experimental results for a benchmark and a tunnel diode oscillator demonstrate the effectiveness of the approach. The proposed method is scalable to other AMS system using language VHDL-AMS as description tool.

목차

Abstract
 1. Introduction
 2. The Proposed Algorithm SFV the Proposed Algorithm SFV
  2.1. Outline of the Proposed Approach: SFV
  2.2. Algorithm for the Proposed Method
 3. Counter-Example Generation
 4. Experimental Results
 5. Conclusion
 Acknowledgments
 References

키워드

저자

• Jingbo Shao [ Postdoctoral Research Station of Information and Communication Engineering, Harbin Engineering University, Harbin 150001, China, College of Computer Science and Information Engineering, Harbin Normal University, Harbin 150025, China ]
• Yongqing Fu [ Postdoctoral Research Station of Information and Communication Engineering, Harbin Engineering University, Harbin 150001, China ]
• Shikai Wang [ College of Mathematical Sciences, Harbin Normal University, Harbin 150025, China ] Corresponding Author

참고문헌

발행기관

간행물

표지보기 관심저널 등록

• 간행물명

  International Journal of Control and Automation

• 간기

  월간

• pISSN

  2005-4297

• 수록기간

  2008~2016

• 십진분류

  KDC 505 DDC 605