원문정보
초록
영어
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.
목차
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