Property-Based Monitoring of Analog and Mixed-Signal Systems
Property-Based Monitoring of Analog and Mixed-Signal Systems
复制标题
模拟和混合信号系统基于属性的监控
DOI：
10.1007/978-3-642-15297-9_3
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
D. Ničković
中科院分区：
文献类型：
--
作者：
John Havlicek;S. Little;O. Maler;D. Ničković
近年来，手机、GPS和便携式多媒体系统等嵌入式消费设备的市场一直在稳步增长。在嵌入式系统中，数字、模拟和软件组件组合在单个芯片上，导致设计越来越复杂，在更小的设备上引入更丰富的功能。因此，在设计中插入错误的可能性变得更高，从而对自动模拟和混合信号验证工具的需求日益增加。在纯数字化环境中，基于工业规范语言（如PSL和SVA）表示的属性的形式验证如今已成功地集成到设计流程中。另一方面，模拟和混合信号系统的验证在很大程度上仍然依赖于基于仿真的ad-hoc方法。在本教程中，我们将考虑标准验证方法的一些要素，这些要素可以成功地从数字导出到模拟和混合信号设置，特别是基于属性的监控技术。基于属性的监控是形式验证的一种更轻松的方法，其中系统被视为生成跟踪集的“黑盒子”，其正确性根据属性进行检查，这是其高级规范。虽然不完整，监测有效地用于捕捉系统中的故障，而不保证其完全正确性。在本教程的第一部分，我们提出了一种基于属性的模拟和混合信号监测技术。在该框架的心脏liessignal时序逻辑STL，这是一个高层次的规范语言，允许表达模拟，混合和定时信号的瞬态特性。STL是实时时间间隔时态逻辑MITL的扩展，其中可以指定使用数值谓词捕获的连续信号中相关“事件”之间的时态关系。然后，我们提出的程序自动翻译任意STL规格intomonitors，即程序，检查一组模拟痕迹的正确性相对于给定的属性。我们介绍了模拟监测工具AMT，实现了所提出的监测技术，并说明了两个工业案例研究的有用性和局限性的方法，考虑属性的FLASH存储器单元和DDR2存储器接口。虽然在AMT实现的STL框架提供了模拟和混合信号验证的理论基础，它是不足以工业强度的验证。DDR2的例子表明，STL缺乏表现力，无法指定工业设计所需的复杂时序关系。STL框架提供了对线性时态逻辑的实时扩展，但它没有提供对PSL和SVA中存在的正则表达式的扩展。然而，工业界对该方法的兴趣导致了Accellera Verilog-AMS委员会的A-SVA小组委员会的成立，该委员会正在研究扩展SVA，使其具有能够对模拟和混合信号系统进行基于工业强度属性的监控的功能。这特别包括实时正则表达式、局部变量和属性访问精确连续值的要求。委员会已经就实时正则表达式和局部变量的初步语法和语义达成一致。他们正在将实时正则表达式与数字和实时属性相结合。这些结果预计将被集成到下一个版本的Verilog-AMS和SystemVerilog。
In the recent past, there has been a steady growth of the market for consumerembedded devicessuch as cell phones, GPS and portable multimedia systems. In embedded systems, digital, analog and software components are combined on a single chip, resulting in increasingly complex designs that introduce richer functionality on smaller devices. As a consequence, the potential insertion of errors into a design becomes higher, yielding an increasing need for automated analog and mixed-signal validation tools. In the purely digital setting, formal verification based on properties expressed in industrial specification languages such as PSL and SVA is nowadays successfully integrated in the design flow. On the other hand, the validation of analog and mixed-signal systems still largely depends on simulation-based, ad-hoc methods. In this tutorial, we consider some ingredients of the standard verification methodology that can be successfully exported from digital to analog and mixed-signal setting, in particularproperty-based monitoringtechniques. Property-based monitoring is a lighter approach to the formal verification, where the system is seen as a “black-box” that generates sets of traces, whose correctness is checked against a property, that is its high-level specification. Although incomplete, monitoring is effectively used to catch faults in systems, without guaranteeing their full correctness.In the first part of the tutorial, we present a technique for property-based analog and mixed-signal monitoring. In the heart of the framework liessignal temporal logicSTL, that is a high-level specification language allowing to express transient properties of analog, mixed and timed signals. STL is an extension of the real-timemetric interval temporal logicMITL, where one can specify temporal relations between relevant “events” in the continuous signals that are captured using numerical predicates. We then present procedures for automatic translation of arbitrary STL specifications intomonitors, i.e. programs that check the correctness of a set of simulation traces with respect to the given property. We introduceanalog monitoring toolAMT that implements the presented monitoring techniques and illustrate the usefulness and the limitations of the approach on two industrial case studies, considering properties of a FLASH memory cell and a DDR2 memory interface.Although the STL framework implemented in AMT provides a theoretical basis for analog and mixed-signal verification, it is not adequate for industrial-strength verification. The DDR2 example shows that STL lacks the expressiveness to specify complex timing relationships required by industrial designs. The STL framework provides real-time extensions tolinear temporal logic, but it does not provide extensions to the regular expressions present in both PSL and SVA. However, the industrial interest in the methodology resulted in the creation of the A-SVA sub-committee of the Accellera Verilog-AMS committee that is investigating extending SVA with features that would enable industrial-strength property-based monitoring of analog and mixed-signal systems. This includes in particular real-time regular expressions, local variables, and requirements for the properties to access accurate continuous values. The committee have agreed upon a preliminary syntax and semantics for real-time regular expressions and local variables. They are in the process of integrating the real-time regular expressions with the digital and real-time properties. These results are expected to be integrated into the next revisions of Verilog-AMS and SystemVerilog.