Charge Pump Phase-Locked Loops and Full Wave Rectifiers for Reachability Analysis
Charge Pump Phase-Locked Loops and Full Wave Rectifiers for Reachability Analysis
复制标题
用于可达性分析的电荷泵锁相环和全波整流器
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Taylor T. Johnson
中科院分区：
文献类型：
--
作者：
O. Beg;A. Davoudi;Taylor T. Johnson
模拟混合信号（AMS）电路广泛应用于各种关键任务的应用，需要在实现之前进行形式验证。我们考虑建模两个AMS电路的混合自动机，特别是电荷泵锁相环（CP-PLL）和全波整流器（FWR）。我们提出了SpaceEx格式的基准测试的可执行模型，进行可达性分析，并展示了他们的自动转换到MathWorks Simulink/Stateflow（SLSF）格式使用HyST工具。此外，作为实现的下一步，我们提出了验证模型的基础上的电路的VHDL-AMS描述。分类：学术困难：背景和起源许多模拟混合信号（AMS）电路广泛用于各种使命关键应用中，并且在实现之前需要正式验证。形式化验证方法构造了一个具有精确语义的数学模型M，并对正确性要求P进行了广泛的分析，|= P [2]。这可以通过可达性分析来确定[1]。作为可以在现场实现和部署之前从正式验证中受益的电路的示例，我们为混合验证研究社区提供了两个潜在的基准，即，电荷泵锁相环（CP-PLL）和全波整流器（FWR）。CP-PLL集成电路广泛用于现代移动的、无线电和无线通信应用中，以使高频信号与低频参考信号同步。在[8]中，作者使用SpaceEx模型检查工具[6]来验证数字PLL的相位和频率锁定的全局收敛性。FWR将AC电输入信号转换为DC输出信号，并且在[5]中使用不同的模型检查工具报告了通过可达性分析进行的正式验证，SpaceEx除外。我们开发了CP-PLL和FWR的混合自动机模型，并使用SpaceEx [6]（一种可达性分析工具）来计算可达状态的过度近似集1。这是一个经典的定点计算工具，操作符号状态。我们还使用HyST（Hybrid Source Transformer）[3]将SpaceEx中开发的混合自动机模型自动转换为MathWorks Simulink/Stateflow（SLSF）模型2。它是一个源代码到源代码的转换工具，可以接受SpaceEx模型格式的输入，并将其转换为HyCreate、Flow*、dReach、C2 E2、Passel 2.0和HyComp格式。其他工具支持正在不时增加。验证和确认研究社区可以使用HyST将SpaceEx格式的混合自动机模型自动转换为1。该工具可从SpaceEx网站http://spaceex.imag.fr/在线获得。2可执行模型包含在HyST网站上，也可从HyST网站http://verivital.com/hyst/在线获取。
Analog-mixed signal (AMS) circuits are widely used in various mission-critical applications necessitating their formal verification prior to implementation. We consider modeling two AMS circuits as hybrid automata, particularly a charge pump phase-locked loop (CP-PLL) and a full-wave rectifier (FWR). We present executable models for the benchmarks in SpaceEx format, perform reachability analysis, and demonstrate their automatic conversion to MathWorks Simulink/Stateflow (SLSF) format using the HyST tool. Moreover, as a next step towards implementation, we present the VHDL-AMS description of a circuit based on the verified model. Category: academic Difficulty: medium 1 Context and Origins Many analog-mixed signal (AMS) circuits are widely used in various mission cicritical applications and require formal verification prior implementation. Formal verification methods construct a mathematical modelM with precise semantics, provide extensive analysis with respect to some correctness requirement P, and verify thatM |= P [2]. This can be ascertained through reachability analysis [1]. As an example of circuitry that can benefit from formal verification prior to field implementation and deployment, we provide two potential benchmarks for hybrid verification research community, i.e., charge pump phase-locked loop (CP-PLL), and full-wave rectifier (FWR). CP-PLL integrated circuits are widely used in modern mobile, radio, and wireless communication applications to synchronize a high-frequency signal with a low-frequency reference signal. In [8], the auhtors use SpaceEx model checking tool [6] to verify the global convergence with respect to phase and frequency lock for a digital PLL. An FWR converts an AC electric input signal to a DC output signal, and formal verification through reachability analysis has been reported using different model checking tools in [5], except SpaceEx. We develop hybrid automaton models of CP-PLL and FWR, and used SpaceEx [6], a reachability analysis tool, to compute the over-approximated sets of reachable states 1. This a classical fixed point computation tool that operates on symbolic states. We also use HyST (Hybrid Source Transformer) [3] to automatically convert the hybrid automaton models developed in SpaceEx to MathWorks Simulink/Stateflow (SLSF) models 2. It is a source-to-source translation tool that takes input in the SpaceEx model format, and translates it to the formats of HyCreate,Flow*, dReach, C2E2, Passel 2.0, and HyComp. Additional tool support is being added from time to time. Verification and validation research community may use HyST to automatically transform the hybrid automaton models in SpaceEx format to 1The tool is available online from the SpaceEx website at: http://spaceex.imag.fr/. 2The executable models are included on the ARCH website and are also available online from the HyST website at: http://verivital.com/hyst/.