Article

CESC: a visual formalism for specification and verification of SoCs

Authors:

Ambar A. Gadkari,

S. Ramesh,

Rubin A. ParekhjiAuthors Info & Claims

GLSVLSI '04: Proceedings of the 14th ACM Great Lakes symposium on VLSI

Pages 354 - 357

https://doi.org/10.1145/988952.989038

Published: 26 April 2004 Publication History

Get Access

Abstract

Verification of present day SoCs is proving to be challenging due to complex interactions among various subcomponents and IPs, with multiple clock domains and diverse bus protocols. The quality of verification depends on the precision in specifying the interaction behaviors. We propose a visual specification language called CESC (Clocked Event Sequence Chart), designed to specify interaction scenarios in SoCs. CESC provides a unique mechanism for representating multiple clock domains, based upon which event occurrences and interactions among different subcomponents can be represented. CESC has a pictorial and textual syntax, and a formal semantics to enable rigorous analysis. The semantics is based on standard notions of partial ordering and timed event traces. CESC is useful in many ways in formalizing SoC verification flows, namely, formalization of verification scenarios, synthesis of protocol checkers and consistency checking of specification versus implementation. This paper describes an algorithm to translate CESC scenarios to protocol checkers used in SoC verification flow. A few examples from industrial designs are included to illustrate the applicability of this formalism in specifying bus transactions and properties of protocols.

References

[1]

Cumming, P. The TI OMAP™ Platform Approach to SoC, Winning the SoC Revolution, Ed. Martin, G. and Chang, H., Kluwer Academic Publishers, 2003.

Google Scholar

[2]

Foster, H., Krolnik, A. and Lacey, D. Assertion-Based Design. Kluwer Academic Publishers, 2003.

Digital Library

Google Scholar

[3]

Accellera, Property Specification Language Ref Manual, version 1.01, 2003.

Google Scholar

[4]

Halbwachs, N. Synchronous Programming of Reactive Systems. Kluwer Academic Publishers, 1993.

Digital Library

Google Scholar

[5]

ITU-T, ITU-T Recommendation Z.120: Message Sequence Charts (MSC), Geneva, 1996.

Google Scholar

[6]

Object Management Group: http://www.omg.org/

Google Scholar

[7]

Verisity Design Inc. web site : http://www.verisity.com/

Google Scholar

[8]

Bunker, A. and Gopalakrishnan, G. Using Live Sequence Charts for Hardware Protocol Specification and Compliance Verification, Proc. 6th IEEE Intl. High-Level Design Validation and Test Workshop. (HLDVT'01), 2001.

Digital Library

Google Scholar

[9]

Andre, C., Peraldi-Frati, M-A. and Rigault, J-P. Scenario and Property Checking of Real-Time Systems Using a Synchronous Approach, Proc. 4th Intl. Symp. on Object-Oriented Real-Time Distributed Computing, 2001.

Digital Library

Google Scholar

[10]

Harel, D. and Marelly, R. Playing with Time: On the Specification and Execution of Time-Enriched LSCs, Proc. IEEE/ACM Intl. Symp. on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS 2002), 2002.

Digital Library

Google Scholar

Cited By

View all

Arora SGadkari ARamesh S(2011)Scenario-Based Specification of Automotive Requirements With Quantitative Constraints and Synthesis of SL/SF MonitorsIEEE Embedded Systems Letters10.1109/LES.2011.21274453:2(62-65)Online publication date: 1-Jun-2011
https://dl.acm.org/doi/10.1109/LES.2011.2127445
Pasricha SDutt N(2008)Verification and Security Issues in On-Chip Communication Architecture DesignOn-Chip Communication Architectures10.1016/B978-0-12-373892-9.00010-4(367-402)Online publication date: 2008
https://doi.org/10.1016/B978-0-12-373892-9.00010-4
Gadkari ARamesh S(2005)Automated Synthesis of Assertion Monitors using Visual SpecificationsProceedings of the conference on Design, Automation and Test in Europe - Volume 110.1109/DATE.2005.74(390-395)Online publication date: 7-Mar-2005
https://dl.acm.org/doi/10.1109/DATE.2005.74

Index Terms

CESC: a visual formalism for specification and verification of SoCs
1. Computer systems organization

Recommendations

Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of ...
A formal requirements engineering method for specification, synthesis, and verification
SEE '97: Proceedings of the 8th International Conference on Software Engineering Environments (SEE '97)

This paper presents a formal requirements engineering method capturing specification, synthesis, and verification. Being multi-paradigm, our approach integrates individual established formal methods: temporal logics are used to express abstract ...
Experiences with specification and verification in LOTOS: a report on two case studies
WIFT '95: Proceedings of the 1st Workshop on Industrial-Strength Formal Specification Techniques

We consider the problems of verifying properties of LOTOS specifications with specific reference to two case studies, one of which was proposed by an industrial collaborator. The case studies present quite different verification requirements and we ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

GLSVLSI '04: Proceedings of the 14th ACM Great Lakes symposium on VLSI

April 2004

479 pages

ISBN:1581138539

DOI:10.1145/988952

General Chair:
David Garrett
Bell Labs Research, Lucent Technologies
,
Program Chairs:
John Lach
University of Virginia
,
Charles Zukowski
Columbia University

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 April 2004

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

GLSVLSI04

Sponsor:

GLSVLSI04: Great Lakes Symposium on VLSI 2004

April 26 - 28, 2004

MA, Boston, USA

Acceptance Rates

Overall Acceptance Rate 312 of 1,156 submissions, 27%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
202
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Arora SGadkari ARamesh S(2011)Scenario-Based Specification of Automotive Requirements With Quantitative Constraints and Synthesis of SL/SF MonitorsIEEE Embedded Systems Letters10.1109/LES.2011.21274453:2(62-65)Online publication date: 1-Jun-2011
https://dl.acm.org/doi/10.1109/LES.2011.2127445
Pasricha SDutt N(2008)Verification and Security Issues in On-Chip Communication Architecture DesignOn-Chip Communication Architectures10.1016/B978-0-12-373892-9.00010-4(367-402)Online publication date: 2008
https://doi.org/10.1016/B978-0-12-373892-9.00010-4
Gadkari ARamesh S(2005)Automated Synthesis of Assertion Monitors using Visual SpecificationsProceedings of the conference on Design, Automation and Test in Europe - Volume 110.1109/DATE.2005.74(390-395)Online publication date: 7-Mar-2005
https://dl.acm.org/doi/10.1109/DATE.2005.74

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP

A formal requirements engineering method for specification, synthesis, and verification

Experiences with specification and verification in LOTOS: a report on two case studies