Automated Synthesis of Assertion Monitors using Visual Specifications
Ambar A. Gadkari, S. Ramesh

TL;DR
This paper introduces a method to automatically generate assertion monitors from visual system specifications in CESC, a language for describing interactions across clock domains, aiding verification.
Contribution
It presents a novel approach to synthesize assertion monitors directly from CESC visual specifications, integrating formal semantics for system-level verification.
Findings
Successfully applied to standard bus protocols like OCP-IP and AMBA
Demonstrates effectiveness of monitor synthesis from CESC specifications
Provides a formal basis for analyzing visual system specifications
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
