基于混合自动机的PSL模型研究  

Research on extending PSL model with hybrid automata

作　　者：张萌[1] 高德远[1] 樊晓桠[1] 

机构地区：[1]西北工业大学计算机学院

出　　处：《计算机应用研究》2010年第1期196-199,203,共5页Application Research of Computers

摘　　要：基于SPICE的计算机仿真方法在混合信号电路验证应用中具有较大的计算开销,讨论基于属性描述的建模方法减小计算开销的问题。通过分析PSL(property specification language)对系统属性的形式化描述方法,并分析混合自动机理论对混合信号系统抽象能力,提出了适合于混合信号电路系统快速验证的PSL模型。结合混合自动机对PSL进行了基于混合自动机语义特点的扩展,使用巴克斯—诺尔范式对其拓展后语法进行规范,提出具有描述混合信号电路行为特性的HAPSL(hybrid automata-based PSL),并针对参考电路的混合信号特性进行了分析,详细说明了HAPSL模型描述在混合信号验证中的实现方法和意义。通过与SPICE仿真器对相同电路进行比较仿真实验,显示HAPSL方法数据在适当规模混合信号电路瞬态分析以及状态分析中具有较高的效率并且具有可接受的精确度。SPICE based simulation in analog and mixed-signal system （AMS） needs lot of computing sources and spends lot of computing time. This paper presented a property specified method for modefing to reduce computation. This paper addressed the formal method for modeling and verification of AMS with hybrid automata based PSL （property specification language ）. And presented the theoretical foundation of abstracting AMS with hybrid automata to derive PSL model extended to AMS verification. This paper presented a novel methodology HAPSL（hybrid automata-based PSL） ,which the syntax was defined by EBNF. The continued and temporal property of mixed signal circuit could be abstracted and modeled by using HAPSL. To illustrate this method, provided the analysis of a sample oscillator circuit with HAPSL in the end. Comparing with SPICE, HAPSL is more efficiency and the accuracy is acceptable in mixed-signal circuit.

关 键 词：计算机仿真 混合自动机 混合信号电路 模型 形式化方法 

分 类 号：TP391.9[自动化与计算机技术—计算机应用技术]