振荡器电路特性的时域验证

--理论计算机科学电子笔记153（2006）9-22www.elsevier.com/locate/entcs振荡器电路特性的时域验证放大图片作者：Bruce H.作者：Krogh，Rob A. Rutenbar1部卡内基梅隆大学电气与计算机工程系美国宾夕法尼亚州匹兹堡，邮编：15213-3890Oded Maler2VERIMAGCentre Euation，2 av deVignate38610Gi`eres，France摘要形式化方法在模拟和混合信号电路中的应用需要有效的方法来构造电路行为的抽象本文讨论振荡器电路特性的验证问题通用监控自动机，提出了促进混合系统的可达性计算的应用，以表征振荡行为的时域特征，如信号幅度和抖动的界限。使用PHAVer（一种混合系统分析工具，基于线性混合自动机近似和无限精度计算提供合理的验证结果）对非线性隧道二极管电路模型进行了说明。关键词：验证，振荡器，模拟电路，混合系统，混合自动机1介绍形式化方法被广泛而成功地用于数字电路的正确性验证。到目前为止，在模拟和混合信号电路领域还没有足够强大的验证技术。由于几个原因，这种电路的验证问题的复杂性是巨大的。模拟1Email： 格弗雷谢|Krogh|ru ten bar@ec e. cm u.e du2电子邮件：Oded. imag.fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.02.01910G. Frehse等人理论计算机科学电子笔记153（2006）9设计具有高维非线性动力学。很难正式定义这种电路的期望行为。它们对各种物理效应的复杂性使得很难将它们的行为孤立起来，并从它们的相互作用中抽象出来。考虑到这种复杂性，形式化方法的初始焦点应该放在早期的块级设计步骤中。在本文中，我们讨论的方法来验证振荡器电路的设计特性，在许多实际应用中发挥了重要作用，作为一个基本的设计块，通过使用的方法和工具的可达性分析。振荡器电路被设计成即使在受到参数变化和干扰时也能产生幅度和相位变化很小的周期信号。我们可以通过应用特别适合于处理不确定性和不确定性的形式验证技术来保证这些变化的保守界限。我们的模型，所谓的混合自动机[1]，捕捉连续以及离散状态的行为，并可用于建模非线性动力学。验证工具的存在，保证结果的正确性，通过使用精确的算术和过近似，最近，取得了进展，在有效计算的可达状态的混合系统。我们提出了一套通用的模型，用于测量和验证幅度变化和（相位）抖动的界限。我们使用PHAVer提供了一些实验结果，PHAVer是一种混合系统工具，可以计算可达状态集的保证保守过近似[7]。作为基准，我们使用隧道二极管振荡器电路，如[10，9]中所示非线性模拟电路的模型检测首先在[10]中提出，其中连续状态空间被离散化，并且为有限的离散模型计算抽象的转移关系。传统的模型检查，ING可以应用到这个抽象，但由于过度近似，只有安全属性被保留。类似于PHAVer中的方法，状态空间的划分适合于系统的动态。在这种方法中的过渡关系的过度近似是远远大于连续值过度近似的PHAVer。它不能保证是保守的，并且在基于离散化的方法中追求保守性可能很快导致过度的准确性损失。在[9]中，使用工具CheckMate [5]验证了模拟电路，该工具计算状态空间的用户定义区域之间的抽象转换关系。优化用于尽可能保证可达状态的多面体包围的保守性，但不能保证找到全局最优。工具d/dt [2]通过离散时间积分计算具有随机动态的混合系统的可达状态，并使用最大化多面体面上向量场的套G. Frehse等人理论计算机科学电子笔记153（2006）911用正交多面体有效地表示状态。这种方法在算法上是合理的，因为使用了欠近似和过近似。线性模拟电路在[6]中已经用d/dt分析过。上述所有工具在数值上都不是精确的，因此它们的过度近似在形式上也不合理.虽然在PHAVer中积分误差会累积，但CheckMate和d/dt都具有过逼近误差不会随时间累积的优点。具有非线性和非线性动力学的混合自动机的过逼近的形式背景起源于Henzinger等人的工作。[11].在下面的部分中，我们定义了振荡，并推导出可以使用可达性检查的振荡属性，例如幅度和相位抖动。我们展示了混合自动机模型，用于监测这些属性使用，ING可达性工具。在第3节中，我们说明了如何PHAVer可以应用于验证这些属性，并在第4节中提供了隧道二极管电路的一些实验结果。最后，我们得出一些结论，在节。五、2定义和消除振荡我们的目标是采取一个模型的振荡器的形式xstec =f（x，p，u），其中p代表参数和u代表外部干扰，并检查它是否表现出振荡行为，是强大的变化下p和所有允许值的u。 作为第一步，我们精确而近似地定义振荡。规格可能因应用而异。讨论的重点是研究某些周期极限环附近的振荡行为，因此我们忽略瞬态行为并假设相位误差接近于零。为了简单起见，我们假设我们的要求描述了作为我们的系统到一个感兴趣的变量x上的投影而获得的标量信号的期望特性这简化了阈值交叉和其他行为的表示在纯量域上，我们将使用x*y表示的|x-y|没有<具体说明。2.1参考信号最严格的规范由参考振荡行为给出，比如ωt（t）=Asin（ωt+φ），（1）在某个度量d中，d（，）<。12G. Frehse等人理论计算机科学电子笔记153（2006）9|−|J使用逐点最大距离d（m，m）= maxm（t）m（t）t∈R+等同于t∈R+：（二）这是一个可达性属性，因为它是满足的，如果状态随时间的推移保持在一个包络内的一个包络内，周围的，并可以计算在增广的状态空间的，和t。由于线性振荡器仅是边缘稳定的，它将很难用数字来模拟。或者，可以使用包络的显式解析计算表示。在实践中，这种性质的验证是相当困难的。无限时间间隔必须映射到有界区间[0，T]，例如，通过在t=T时重新设置参考时间，这需要T的显式知识。保守的可达性分析通常依赖于某种类型的overap，近似，这将导致许多电路的周期可以在某个间隔内变化，除非电路被设计为相对于周期T渐近稳定。由于（2）中的量化在所有时间范围内，周期中的任何偏差都会导致两个信号之间的距离过大。因此，在下文中，我们将考虑更适合于实际目的的性质。2.2任意T周期行为另一个不太具体的性质是周期时间T。假设我们知道所有的信号，无论是干净的还是有噪声的，都保持在一个范围内，因为集合X是一个很好的欠估计。3Sincexcanoccurmore在一个周期内，我们考虑x只出现一次的信号，期间在一些组合的迹象，更高的衍生物，并为此，以避免病理情况下，在任何时候为一些k>0的衍生物d k/dt k x（t）不为零。 为了简单起见，我们在下文中将X表示为类似状态的元组（x，J，D a1，. ，D a m），其中xJ∈ X，Da i∈ {≤，≥}且m+1是产生信号的系统的阶。此外，我们写<$（t）=x，如果<$（t）=x以及在时间t处的di/dti ∈（t）Dai0。这将使我们能够表达在时间点上，X？occur中的值是什么。表达周期性的经典方法是（t+nT）.（三）[3]我们可以把它定义为所有感兴趣的信号都无限频繁访问的最大集合G. Frehse等人理论计算机科学电子笔记153（2006）913另一个几乎等价的定义（当使用严格相等时，它们是等价的）可以通过计数值x为n的第n出现来实现。设τ（x，n）=ti，则x在时间t上第n出现在τ中.我们稍后将使用这个公式来构建监控自动机。配备了这个功能，我们可以说：<$x∈X<$，n，m∈N：τ（x，n）<$τ（x，m）−（m-n）T.（四）（3）和（4）之间的区别在于，我们在（3）中对t的所有正值进行量化，而在（4）中对X的值进行量化，即，只是为了你的幸福x出现在每个x中。（3）和（4）都不是系统原始状态空间上的可达性，因为它们需要有限（有界但密集）的内存。让我们先把它们简化为t∈R+：<$x∈X<$，n∈N：τ（x，n）<$τ（x，n+1）−T.（六）只有当我们使用严格相等时，上面的性质才等价于（3）和（4）在（5）的情况下，存储器由函数z：[0，T）<$→X组成，使得在任意时刻t，z（tJ）=<$（t-tJ）。 对于（6），存储器是一个函数w：X<$×{≤，≥}m<$→R+，其中w（x）= τ（x，nx），nx是x在τ中已出现的次数.2.3减少到有限内存现在我们引入具有有限记忆的近似来表征这些性质。 这个想法非常简单：只需将所有t或x上的量化替换为每个周期的有限个值。不失一般性，让我们为t和x都选择零，以及一些固定的符号元组Da这两个公式简化为：对于衍生品。（（n+1）T），（7）<$n ∈ N：τ（0，n）<$τ（0，n +1）− T.（八）在（7）中，我们说我们每T个时间单位大致得到相同的值 在（8）我们说过零点的间隔大约为T。从机械上讲，这些属性可以通过向14G. Frehse等人理论计算机科学电子笔记153（2006）9系统添加时钟以及可以记住时间或值的内存变量来检查。对于第一个属性，也称为周期到周期幅度变化，我们记住x的最后一个值为nT，当时钟到达T时 ，我们将当前的nT值与前 一个 值进行比较，重置时钟并更新内存。为G. Frehse等人理论计算机科学电子笔记153（2006）915（a）单周期（b）绝对值（c）周期到周期Fig. 1. 振幅变化第二个属性，称为周期抖动，我们每次遇到（t）= 0时将时钟值与内存进行比较，然后重置时钟并更新内存。为了使x在每个周期只出现一次，我们考虑了导数（或其他状态变量），它们是用离散状态编码的。2.4监控自动机图1和图2显示了使用可达性分析验证幅度变化和相位抖动边界的监视器自动机。它们包含一个特殊的错误位置，如果这个错误位置不可达，则这些属性将被填充。 振幅变化的最简单形式，即单个周期内的变化，由图1（a）中的监视器检查。它有一个测量周期T流逝的时钟。 如果在循环结束时，x可能离零太远，则错误位置是可到达的，并且违反了该属性。图1（b）中的监视器检查对于周期T的所有倍数，状态是否在零交叉附近，即，是否<$n∈ N：<$（nT）<$0.（九）监视器最初处于循环状态。时钟t测量周期，并且在t=T时可能有两个转变：如果x接近于零，则时钟复位并且监视继续。如果x在零附近的非零区域之外，则监视器进入错误位置并且违反属性。正如在2.1节末尾所讨论的，关于显式周期T的绝对变差只有在特殊情况下才是实际的。相比之下，振幅的周期到周期变化，即，性质（7）是实际有用的，因为它允许与周期T的一些偏差。相应的监视器如16G. Frehse等人理论计算机科学电子笔记153（2006）9图1（c）. 将t=T时x的值与最后一个 周期的x值进行比较。监控抖动稍微复杂一些，因为我们必须在每个周期唯一地识别一个过零点 我们证明了这一点的二阶系统，其中最多有两个零交叉，可以区分由该信号的derivativxstec。图中的显示器。2（a）定义了抖动，即， 财产（8）。它有一个时钟t，有三个位置，一个用于x的正值，一个用于x的负值，还有一个错误位置。自动机最初在位置循环pos，并假设x的导数为正。循环的前半部分发生在该位置，直到零交叉与一个重复的驱动器同步，此时触发到循环负位置的过渡。在那里，发生循环的第二半，直到零交叉被正导数击中。在这一点上，两个转变是可能的：如果时钟t是在周期T的100个单位内，时钟被重置，并且周期在位置循环位置重新开始。否则，监视器进入错误状态。图2（b）中的监视器验证周期间抖动，即，物业n ∈ N：τ（0，n +1）− τ（0，n）<$τ（0，n）− τ（0，n −1）。（十）它的工作原理与图2（a）中的监视器相似，只是前一个循环时间存储在变量t中，在每个新的循环之后，时间再次比较，而不是T。最后，我们转向获得幅度变化和相位抖动的界限的问题，而不是验证先验已知的界限。图2中的监视器自动机。1和2通过去除错误位置而容易地适应。然后，幅度变化的界限可以可以从可达状态集合与约束t=T的交集中的状态获得。对于相位抖动的界限，我们将位置循环neg，neg中的可达状态视为具有约束x= 0。3在PHAVer我们在前面的部分中提供了一些监控自动机的实验结果。为了计算可达状态集，我们使用验证工具PHAVer [7]，它可以计算线性混合自动机4（LHA）的精确可达性[1]。在线性混合自动机中，[4]线性混合自动机这个术语在文献中使用得很模糊，有时也指我们所说的线性动力学。G. Frehse等人理论计算机科学电子笔记153（2006）917我（a）周期（b）周期间图二. 相位抖动由线性谓词给出，由线性约束a Txstecda ib i，a i∈Z n，b i∈ Z，D a i∈ {<，≤，=}，i = 1，.，M.（十一）对于这类混合系统，计算在算法上是精确的，并且纯粹基于状态，在有限时间内变化。PHAVer使用多面体来表示状态集，并使用基于ParmaPolyhedra Library [3]的精确算法和强大的无界整数表示。由于精确的算术，表示状态的线性谓词的复杂性通常在分析过程中增加得令人望而却步。谓词中的系数的大小这种复杂性是通过对系数中使用的位数和约束数的完全用户可控的限制来管理的。超过这些限值的同品种器械被保守地认为是简单同品种器械的过度近似。除了可达性分析之外，PHAVer还支持compo- sitional和assume-guarantee推理，并使用单独的引擎来计算仿真关系，该引擎也可用于验证抽象[8]。PHAVer可以通过用LHA过近似来分析具有形式为xstec =Ax+b的线性动力学的系统。保证过近似是保守的，算法上和数值上都是合理的[11]。阿贡18G. Frehse等人理论计算机科学电子笔记153（2006）9我我| || |我动力学以一种放松的形式被指定为约束的结合aTxstec+aTxdaibi，ai∈Zn.（十二）放松的形式允许我们在近似或参数的模型不确定性。 例如，在一个示例中，对于动力学xstec =ax，a∈[al，au]的参数范围对于x的正值，产生一个微分包含al x≤xstec≤au x，并且au x≤xstec≤al x否则。这两种情况是通过引入一个单独的每种情况下的位置，从而为了进行分析，通过线性规划将来自（12）的LHA动态过度近似于来自（11）的LHA动态，如下所示。设等式由两个不等式的合取来如果不变量Inv（loc）为位置loc是有界的，x的集合bi−p/q，其中p/q是有理数这个满填充（12）由一个Txstecdaip/q=infa∈Tx， p，q∈Z.我x∈Inv（loc）这种过近似引入了精度损失，其取决于位置的大小和位置中的导数向量的角展度，即，矢量场加宽的空间角度。为了提高精度，位置被递归地分成两个沿着一个合适的超平面，有效地划分状态空间与网格，其形状取决于分裂超平面的选择。它们的优先次序是根据一组准则，其目的在于最小化分区的数量，即，位置我通过分裂引入D。LetXstec是在一个位置上的导数的集合。我们将衍生品的价差定义为q（Xstec）=arccosminxTy/xy。x，y∈X空间通过选择使导数的扩展最小化的超平面，并且一旦达到扩展的较低阈值就停止分裂，可以使划分适应于动态。将分区限制为可达位置集，当从可达性算法的等待列表中取出每个位置时，但在实际计算位置中的可达状态之前，递归地为每个位置触发分裂。一旦一个可到达的位置被分解为较低的大小和分布阈值，它在分析的剩余部分中保持固定图3显示了分析过程中的分区示例。开始从一组初始状态I L= 0 6 mA时，该区域被分割，直到初始状态被分割，使得每个分区具有s_p_readq（X_stec）=a_r_cc_o_s0。85. 然后在每个位置内通过应用G. Frehse等人理论计算机科学电子笔记153（2006）919I_L [mA]0.60 0.600.58 0.580.56 0.560.54 0.540.52 0.520.500.450.460.470.480.490.500.500.450.460.470.480.49 0.50V_d [V](a) 计算期间的快照V_d [V](b) 最终结果图三. 可达状态和不变量时间流逝操作符。结果如图3（a）所示。位置之间的转换产生被放入等待列表中的后继状态。等待列表上的位置被分区，并应用时间流逝运算符重复该过程，直到图中的定点3（b）得到。我们用（12）式中的分段非线性微分包含来模拟非线性电路方程。分割非线性分量的一维特征，例如，二极管，到凸或凹部分，使我们能够很容易地构建一个线性包络的每个间隔。实现这一点通过在最小值、最大值和最小值点处分离。找到这些点的不准确性可以通过重叠部分来补偿（更准确地说，结果抽象的不变量），更多细节请参见[11]。不含非线性元素的方程直接建模。然后，可以在PHAVer中分析AQUINE模型，在分析期间，PHAVer使用LHA对其进行过近似。在线方法决定性地提高了分析的速度和内存要求。前两节中的监视自动机是线性混合自动机，并且很容易在PHAVer的文本输入语言中建模。对于具有错误状态的自动机，只要该状态可达，即可停止可达性计算，大大提高了试错实验的速度。4实验结果在本节中，我们将介绍[9]中隧道二极管振荡器电路的实验结果。我们模型的电流IL通过电感和电压降Vd的隧道二极管并联电容的串联RLC电路，这是在稳定的振荡给定的参数。的I_L [mA]20G. Frehse等人理论计算机科学电子笔记153（2006）90的情况。069 2V3−0。042 1V2+0。004Vd+8。如果为0，则为96·10−4。055≤Vd≤0. 三十五岁，∈第六章. 01V3−0。992V2+0。054 5Vd（如果Vd≤0）。055，DDDDId=DD见图4。 隧道二极管电路状态方程由下式给出：Vstecd=1/C（−Id（Vd） +IL），（13）IstecL= 1/L（−Vd− 1/G·IL+Vin），（14）其中，C=1pF，L=1μ H，G=5mΩ−1，Vin=0。3V，和电流000. 263V3−0。277V2+0。096 8Vd−0。如果为0，则为0112。35≤Vd.按照上一节中概述的程序，为隧道二极管特性 Id（V）构造分段的α-Ekenne我们选择64个区间的范围V d∈ [− 0. 1、0. 6]以产生足够的准确性，从而获得（13）的分段a-logne模型。 它被建模为混合动力汽车-ton，其中Vd作为输出变量，IL作为输入变量，并且由64个位置组成，每个间隔一个。方程（14）是一个随机数，并且被建模为具有Vd作为输入和单个位置的混合自动机。这两种模型都在PHAVer中进行了合成和分G. Frehse等人理论计算机科学电子笔记153（2006）921析。图4显示了从由Vd [0]给出的一组初始状态可达到的状态。42伏，0.52 V]，I L= 0。6mA。它还显示了不变量（灰色），其中垂直线对应于64个间隔的二极管特性，其余的分区22G. Frehse等人理论计算机科学电子笔记153（2006）9图五. 图1的电路和幅度监视器的可达状态。1（a）是在分析过程中产生的。该算法的参数是分裂平面的方向，位置的最小和最大尺寸，这里是可见区域的1/256和1/16，以及每个位置中的导数的最小扩展qmin= arccos（0. 999）。为了控制复杂性，多面体的约束限制为24位，多面体限制为32个约束。在运行32位Linux内核的2.8GHz和4GBRAM的Intel Xeon处理器上，可达性分析需要72。8s和要求126. 7 MBRAM。分区产生2998个位置，其中1892个是可到达的。我们现在应用可达性分析来测量IL（t）的单周期幅度变化和周期抖动。如2.4节所述，我们分别使用图1（a）和图2（a）的监控自动机，去除错误位置以检测周期和过零。我们使用的是一个aausanne近似的二极管特性与128分区。除了1 /512 th的最小位置大小和qmin= arccos（0.99999）。为了测量振幅变化，我们假设周期时间为T = 13。75微秒。可达性分析需要1880秒（1325 MB）.如图5所示，所获得的可达状态IL（t）和Vd（t）的集合保证了0. 532 mA和0. 636毫安。为了测量相位抖动，假设过零点在IL= 0处。6 mA。每个周期有两个交叉点，我们根据Vd> 0来区分. 25 V或V d<0。图6中所示的可达状态保证周期在13. 52 μ s和13. 86微秒。计算需要1997秒（1463 MB）。G. Frehse等人理论计算机科学电子笔记153（2006）923见图6。 电路的可达状态和图1的相位抖动监视器。2（a）5结论本文提出了一种基于与感兴趣的规格相关的标量信号特性的分析来构造振荡器电路的监视自动机的方法。这里我们考虑幅度和相位抖动。我们的目标是构建混合系统模型，适合有限时间可达性分析。典型的混合系统可达性计算集中于从一组初始条件开始的瞬态系统行为。目前的工作旨在验证性能的渐近，“稳态”的行为的电路。我们有兴趣扩展这种方法来验证其他属性，通常使用频域技术进行分析。引用[1] 巴尔河，C. Courcoubetis，N.Halbwachs，T.A. Henzinger，P.H. Ho，X.Nicollin，A.奥利维罗，J. Sifakis和S.Yovine，混合系统的算法分析，理论计算机科学138（1995），pp.3-34，一个初步版本出现在Proc. 11 th Int. Conf. Analysis and Optimization of Systems：Discrete-Event Systems（ICAOS），LNCIS 199，Springer，1994，pp. 331-351.[2] Asarin，E.，T. Dang和O.Maler，混合系统验证的d/dt工具，在：Brinksma和Larsen [4]，pp.365-370[3] 巴尼亚拉河E. Ricci，E. Za Zaghanella和P.M. Hill，Possibly not closed convex polyhedraand the Parma Polyhedra Library ，in ： M. 诉Hermenegildo 和G.Puebla，editors ，StaticAnalysis：Proc. Int. Symp. ，LNCS2477（2002），pp. 213-229[4] Brinksma，E.和K. G. Larsen，编辑，[5] Chutinan，A.和B.H. Krogh，混合系统验证的计算技术，IEEE自动控制48（2003），pp.六十四比七十五24G. Frehse等人理论计算机科学电子笔记153（2006）9[6] 天啊T A. Donze和O. Maler，Verification of analog and mixed-signal circuits using hybridsystem techniques，in：Formal Methods in Computer-Aided Design（FMCAD 2004），Austin，Texas，November 14-17，2004。[7] Frehse，G.，Phaver：混合动力系统过去的物理验证hytech，M。莫拉里和L. Thiele，编辑，混合系统：计算和控制（HSCC '05），3月。 9 http://www.cs.ru.nl/-11，2005，Zuürich，CH，2005，P H A V e r is a v aila b l e a t www.example.com goranf/.[8] Frehse，G.，Z. Han和B. H. Krogh，Assume-guarantee reasoning for hybrid i/o-automataby over-approximation of continuous interaction ， in ： Proc. IEEE Conf. Decision andControl（CDC[9] 古普塔，S.，B. H. Krogh和R. A. Rutenbar，Towards formal verification of analog designs，in：Proc. IEEE Intl.计算机辅助设计会议（ICCAD-2004），2004年11月7日至11日，圣何塞，加利福尼亚州（美国），2004年。[10] Hartong，W.，L. Hedrich和E.Barke，非线性模拟系统的离散建模和模型检验。，in：Brinksmaand Larsen [4]，pp.401-413[11] Henzinger，T.一、P. - H. Ho和H.王泰，非线性混杂系统的数学分析，IEEE自动控制学报43（1998），pp. 540-554