Article

Directed-simulation assisted formal verification of serial protocol and bridge

Authors:

Raj S. MitraAuthors Info & Claims

DAC '06: Proceedings of the 43rd annual Design Automation Conference

Pages 731 - 736

https://doi.org/10.1145/1146909.1147096

Published: 24 July 2006 Publication History

Get Access

Abstract

Robust verification of protocol conversion and arbitration schemes of SoC bridges forms a significant component of the overall SoC verification. Formal verification provides a way to achieve this, but a naive approach often leads to explosion of the state space, and is impractical for most of today's protocols and bridges. This problem is further complicated in the presence of serial protocols, where control and data are mixed together and transactions continue for very great depths. White-box verification is not a feasible solution, since these bridges are often imported or generated from other sources, and internal information is not readily available. In this paper, we propose a black-box and hybrid approach to this problem, by judiciously mixing simulation and formal verification. We illustrate our approach by applying it to two dual stage bridges that perform serial to parallel protocol conversion and vice versa.

References

[1]

E. Salminen, V. Lahtinen, K. Kuusilinna and T. Hamalainen, "Overview of Bus-Based System-on-Chip Interconnections," IEEE International Symposium on Circuits and Systems, 2002, vol 2, pp. II-372 -- II-375.

Google Scholar

[2]

Open Core Protocol 2.1 Specification, www.ocpip.org

Google Scholar

[3]

ARM Inc, AMBA AXI Protocol Specification, Mar., 2004. www.arm.com

Google Scholar

[4]

Philips Semiconductors, "The I2C-BUS specification", Version 2.1, January, 2000. http://www.cse.ucsc.edu/classes/cmpe123/Fall02/Files/I2C_BUS_SPECIFICATION.pdf

Google Scholar

[5]

USB Implementers Forum Inc, Universal Serial Bus Specification Revision 2.0, 2000. www.usb.org

Google Scholar

[6]

Abhik Roychoudhury, Tulika Mitra and S. R. Karri, "Using Formal Techniques to Debug the AMBA System-on-Chip Bus Protocol," Design, Automation and Test in Europe Conference, 2003, pp. 10828--10833.

Digital Library

Google Scholar

[7]

P. Chauhan, E. Clarke, Y. Lu and D. Wang, "Verifying IP-core based system-on-chip design," Proc. IEEE ASIC. Conf., Washington, DC, USA, Sept. 1999, pp. 27--31.

Google Scholar

[8]

A. Goel, and W. R. Lee, "Formal verification of an IBM coreconnect processor local bus arbiter core," Proc. Design Automation Conf., June, 2000.

Digital Library

Google Scholar

[9]

Shivakumar Chonnad and Balachander Needamangalam, "A Layered Approach to Behavioral Modeling of Bus Protocols," Proceedings of the 13th Annual IEEE International ASIC/SOC Conference, 2000, pp 170 -- 173.

Google Scholar

[10]

B. Plessier and C. Pixley, "Formal verification of a commercial serial bus interface," Conference Proceedings of the 1995 IEEE Fourteenth Annual International Phoenix Conference on Computers and Communications, 1995.

Google Scholar

[11]

C Norris Ip, "Formal interface compliance verification", Electronics Design Process Workshop, April 2003.

Google Scholar

[12]

Albin K, Yuan J, Aziz A, Pixley C, "Constraint synthesis for environment modelling in functional verification", Design Automation Conference, pp 296--299, 2003.

Digital Library

Google Scholar

[13]

Pastor E, Pena M A, "Combining simulation and guided traversal for the verification of concurrent systems", DATE Conference, pp 1158--1159, 2003.

Digital Library

Google Scholar

Cited By

View all

Feng LSong XZhao XZheng WLiu Y(2017)A method for analyzing serial bus protocols with standalone clock signals2017 First International Conference on Electronics Instrumentation & Information Systems (EIIS)10.1109/EIIS.2017.8298749(1-5)Online publication date: Jun-2017
https://doi.org/10.1109/EIIS.2017.8298749
Behrend JLettnin DGrünhage ARuf JKropf TRosenstiel W(2017)Scalable and Optimized Hybrid Verification of Embedded SoftwareEmbedded Software Verification and Debugging10.1007/978-1-4614-2266-2_8(183-205)Online publication date: 19-Apr-2017
https://doi.org/10.1007/978-1-4614-2266-2_8
Lettnin DWinterholer M(2017)An Overview About Debugging and Verification Techniques for Embedded SoftwareEmbedded Software Verification and Debugging10.1007/978-1-4614-2266-2_1(1-18)Online publication date: 19-Apr-2017
https://doi.org/10.1007/978-1-4614-2266-2_1
Show More Cited By

Index Terms

Directed-simulation assisted formal verification of serial protocol and bridge
1. Hardware
  1. Hardware validation
    1. Functional verification

Recommendations

Hybrid Verification of Protocol Bridges

It is becoming increasingly more evident that simulation cannot provide full verification for today's complex designs. Formal verification is emerging as an alternative technique to simulation that promises to guarantee complete verification. However, ...
Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Coverage metrics for formal verification

In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proven to be correct, there is still a question of how complete the specification is and whether it really covers all the behaviors of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DAC '06: Proceedings of the 43rd annual Design Automation Conference

July 2006

1166 pages

ISBN:1595933816

DOI:10.1145/1146909

General Chair:
Ellen M. Sentovich
Cadence Berkeley Labs, Berkeley, CA

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: 24 July 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

DAC06

Sponsor:

DAC06: The 43rd Annual Design Automation Conference 2006

July 24 - 28, 2006

CA, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 1,770 of 5,499 submissions, 32%

Upcoming Conference

DAC '25

Sponsor:
sigda

62nd ACM/IEEE Design Automation Conference

June 22 - 26, 2025

San Francisco , CA , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
323
Total Downloads

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

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Feng LSong XZhao XZheng WLiu Y(2017)A method for analyzing serial bus protocols with standalone clock signals2017 First International Conference on Electronics Instrumentation & Information Systems (EIIS)10.1109/EIIS.2017.8298749(1-5)Online publication date: Jun-2017
https://doi.org/10.1109/EIIS.2017.8298749
Behrend JLettnin DGrünhage ARuf JKropf TRosenstiel W(2017)Scalable and Optimized Hybrid Verification of Embedded SoftwareEmbedded Software Verification and Debugging10.1007/978-1-4614-2266-2_8(183-205)Online publication date: 19-Apr-2017
https://doi.org/10.1007/978-1-4614-2266-2_8
Lettnin DWinterholer M(2017)An Overview About Debugging and Verification Techniques for Embedded SoftwareEmbedded Software Verification and Debugging10.1007/978-1-4614-2266-2_1(1-18)Online publication date: 19-Apr-2017
https://doi.org/10.1007/978-1-4614-2266-2_1
Behrend JLettnin DGrünhage ARuf JKropf TRosenstiel W(2015)Scalable and Optimized Hybrid Verification of Embedded SoftwareJournal of Electronic Testing: Theory and Applications10.1007/s10836-015-5518-431:2(151-166)Online publication date: 1-Apr-2015
https://dl.acm.org/doi/10.1007/s10836-015-5518-4
Behrend JGruenhage ASchroeder DLettnin DRuf JKropf TRosenstiel W(2014)Optimized hybrid verification of embedded software2014 15th Latin American Test Workshop - LATW10.1109/LATW.2014.6841906(1-6)Online publication date: Mar-2014
https://doi.org/10.1109/LATW.2014.6841906
Tong JSarraf DBoule MZilic Z(2011)Generating compact assertions for control-based logic signals2011 IEEE 54th International Midwest Symposium on Circuits and Systems (MWSCAS)10.1109/MWSCAS.2011.6026268(1-4)Online publication date: Aug-2011
https://doi.org/10.1109/MWSCAS.2011.6026268
Yeh HHuang CLin Y(2010)Automatic constraint generation for guided random simulationProceedings of the 2010 Asia and South Pacific Design Automation Conference10.5555/1899721.1899865(613-618)Online publication date: 18-Jan-2010
https://dl.acm.org/doi/10.5555/1899721.1899865
Guoyin Zhang Ming Liu Aihong Yao (2010)A formal approach for modeling and verification of bus bridge based on Petri Net and model checking2010 3rd International Conference on Computer Science and Information Technology10.1109/ICCSIT.2010.5565021(335-339)Online publication date: Jul-2010
https://doi.org/10.1109/ICCSIT.2010.5565021
Lettnin DNalla PBehrend JRuf JGerlach JKropf TRosenstiel WSchönknecht VReitemeyer SBenini LDe Micheli GAl-Hashimi BMueller W(2009)Semiformal verification of temporal properties in automotive hardware dependent softwareProceedings of the Conference on Design, Automation and Test in Europe10.5555/1874620.1874912(1214-1217)Online publication date: 20-Apr-2009
https://dl.acm.org/doi/10.5555/1874620.1874912
Sinha RRoop PBasu S(2008)SoC design approach using convertibility verificationEURASIP Journal on Embedded Systems10.1155/2008/2962062008(1-19)Online publication date: 1-Jan-2008
https://dl.acm.org/doi/10.1155/2008/296206
Show More Cited By

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

Hybrid Verification of Protocol Bridges

Formal verification of ASMs using MDGs

Coverage metrics for formal verification