Automated Synthesis of Assertion Monitors using Visual Specifications
Ayush Pravin Gadkari, S. Ramesh · Design, Automation, and Test in Europe · 2005
Automated synthesis of monitors from high-level properties plays a significant role in assertion-based verification. We present 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 a synchronous language paradigm enabling formal analysis of specifications. We provide an overview of the CESC language with a 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 the monitor synthesis algorithm.