摘要

针对模拟与混合信号(AMS)电路形式化建模逼真度低和描述不规范的问题,提出一种基于基尔霍夫电流定律节点分析的形式化建模方法。通过扩展计算树逻辑公式,在保留电路更多物理特性的前提下综合描述和验证AMS电路的离散事件和动态行为,保证性质验证的精确性和可信性。以环形振荡器为例,给出该方法的实现过程,并通过Coho工具对振荡器电路进行验证。实验结果表明该方法正确、有效。