In this chapter we concentrated on checking the correctness or accuracy of analog behavioral models. The authors presented some approaches to judge the verification process using metrics like code or state-space coverage. These coverage methods are new for the analog domain and can be used to substantially increase the confidence in the verification setup and following in the model. Additionally, the authors presented a methodology to generate a model in a complete formal way due to the consideration of the whole reachable state space of the original circuit. This approach reaches a big abstraction in combination with a high speed-up comparable with manually written behavioral models.

Chapter Contents:

• 5.1 Overview
• 5.1.1 State space and normal form
• 5.2 Model validation
• 5.2.1 Model validation metrics
• 5.2.1.1 Code coverage
• 5.2.1.2 State-space coverage
• 5.3 Semiformal model verification
• 5.4 Formal model verification
• 5.4.1 Equivalence checking
• 5.4.2 Other formal techniques
• 5.5 Formal modeling
• 5.5.1 Correct by construction: (automatic) abstract model generation via hybrid automata
• 5.5.1.1 Abstraction by sampling the state space
• 5.5.1.2 Linear location identification
• 5.5.1.3 State-space representation of the HA locations
• 5.5.1.4 Experimental results
• 5.5.1.5 Correction and formal verification of the constructed model
• 5.6 Conclusion
• Acknowledgements
• References

Inspec keywords: analogue circuits; behavioural sciences computing

Other keywords: code coverage; manually written behavioral models; state-space coverage; reachable state space

Subjects: Other analogue circuits