Automated synthesis of assertion monitors using visual specifications

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.