基于可视化规范的断言推理的自动综合
Automated Synthesis of Assertion Monitors using Visual Specifications
摘要：
在基于断言的验证中，从高级属性自动合成监控器起着重要的作用。我们在这里提出了一种方法来合成断言监视器从视觉规范CESC（时钟事件序列图）。CESC是一种可视化语言，用于指定涉及单个和多个时钟域的系统级交互。它具有定义良好的图形和文本语法以及基于同步语言范式的形式化语义，从而能够对规范进行形式化分析。在本文中，我们提供了一个概述CESC语言与一些说明性的例子。描述了CESC规范中断言监视器的自动合成算法。最后，以标准总线协议（OCP-IP和AMBA）为例，说明了监控器综合算法的应用。
英文摘要：
Automated synthesis of monitors from high-level properties plays a significant role in assertion-based verification. We present here a methodology to synthesize assertion monitors from visual specifications given in CESC (Clocked Event Sequence Chart). CESC is a visual language designed for specifying system level interactions involving single and multiple clock domains. It has well-defined graphical and textual syntax and formal semantics based on synchronous language paradigm enabling formal analysis of specifications. In this paper we provide an overview of CESC language with few illustrative examples. The algorithm for automated synthesis of assertion monitors from CESC specifications is described. A few examples from standard bus protocols (OCP-IP and AMBA) are presented to demonstrate the application of monitor synthesis algorithm.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
