Article

On the Design and Verification Methodology of the Look-Aside Interface

Authors:

Ali Habibi,

Asif Iqbal Ahmed,

Otmane Ait Mohamed,

Sofiene TaharAuthors Info & Claims

DATE '05: Proceedings of the conference on Design, Automation and Test in Europe - Volume 3

Pages 290 - 295

https://doi.org/10.1109/DATE.2005.228

Published: 07 March 2005 Publication History

Get Access

Abstract

In this paper, we present a technique to design and verify the Look-Aside (LA-1) Interface standard used in network processors. Our design flow includes several refinements starting from an informal UML specification until getting to an RTL modeled in Verilog. We integrate the verification of the LA-Interface in the design flow by considering two intermediate levels: (1) Abstract State Machines (ASM); and (2) SystemC. The first one serves the verification by model checking of a set of PSL properties, while the second includes a set of assertions to be verified by simulation. To evaluate the performance of our approach, we used the Rule-Base model checker to verify the same properties; and the OVL library to verify the same assertions.

References

[1]

{1} Accellera Organization. Open Verification Library, Assertion Monitor Reference Manual, v 03.06.06., 2003.

Google Scholar

[2]

{2} Accellerab Organization. Accellera Property Specification Language reference manual, Version 1.01., 2004.

Google Scholar

[3]

{3} H. Bhugra. La-1b: Moving the look-aside interface forward. CommsDesign, August 2002.

Google Scholar

[4]

{4} IBM Haifa Research Laboratories. RuleBase Formal Verification Tool (Version 1. 5). Users Guide. May 2003.

Google Scholar

[5]

{5} K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

Digital Library

Google Scholar

[6]

{6} Microsoft Corporation. AsmL for Microsoft. NET Framework, Microsoft., 2004.

Google Scholar

[7]

{7} Network Processing Forum. Look-Aside (LA-1) Interface, Implementation Agreement, Revision 1. 1. Kluwer Academic Publishers, April 15, 2004.

Google Scholar

[8]

{8} Open SystemC Initiative. www.systemc.org, 2004.

Google Scholar

[9]

{9} OSI. SystemC 2.0.1 language reference manual. 2004.

Google Scholar

[10]

{10} K. Shimizu, D. L. Dill, and A. J. Hu. Monitor-based formal specification of PCI. In Formal Methods in Computer-Aided Design, pages 335-353, Austin, Texas, November 2000.

Digital Library

Google Scholar

Cited By

View all

Abed SHussain KAit-Mohamed O(2018)Abstract property language for MDG model checking methodologyInternational Journal of Computer Applications in Technology10.1504/IJCAT.2012.04820544:1(23-36)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.1504/IJCAT.2012.048205
Habibi ATahar S(2006)Design and verification of systemc transaction-level modelsIEEE Transactions on Very Large Scale Integration (VLSI) Systems10.1109/TVLSI.2005.86318714:1(57-68)Online publication date: 1-Jan-2006
https://dl.acm.org/doi/10.1109/TVLSI.2005.863187
Habibi ATahar S(2005)An approach for the verification of systemc designs using asmlProceedings of the Third international conference on Automated Technology for Verification and Analysis10.1007/11562948_8(69-83)Online publication date: 4-Oct-2005
https://dl.acm.org/doi/10.1007/11562948_8

Recommendations

Automated interface refinement for compositional verification

Compositional verification is essential for verifying large systems. However, approximate environments are needed when verifying the constituent modules in a system. Effective compositional verification requires finding a simple but accurate ...
An Interface Theory for Program Verification
Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles
Abstract
Program verification is the problem, for a given program and a specification , of constructing a proof of correctness for the statement “program satisfies specification ” () or a proof of violation ([inline-graphic not available: see fulltext]). ...
An assertion-based verification methodology for system-level design

In this paper, we integrate an assertion-based verification methodology with our object-oriented system-level synthesis methodology to address the problem of HW/SW co-verification. In this direction a system-level assertion language is defined. The ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DATE '05: Proceedings of the conference on Design, Automation and Test in Europe - Volume 3

March 2005

283 pages

ISBN:0769522882

Publisher

IEEE Computer Society

United States

Publication History

Published: 07 March 2005

Check for updates

Qualifiers

Article

Conference

DATE05

Sponsor:

SIGDA

DATE05: Design, Automation and Test in Europe

March 7 - 11, 2005

Acceptance Rates

Overall Acceptance Rate 518 of 1,794 submissions, 29%

Upcoming Conference

DATE '25

Sponsor:
sigda

Design, Automation and Test in Europe

March 31 - April 2, 2025

Lyon , France

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
9
Total Downloads

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

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Abed SHussain KAit-Mohamed O(2018)Abstract property language for MDG model checking methodologyInternational Journal of Computer Applications in Technology10.1504/IJCAT.2012.04820544:1(23-36)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.1504/IJCAT.2012.048205
Habibi ATahar S(2006)Design and verification of systemc transaction-level modelsIEEE Transactions on Very Large Scale Integration (VLSI) Systems10.1109/TVLSI.2005.86318714:1(57-68)Online publication date: 1-Jan-2006
https://dl.acm.org/doi/10.1109/TVLSI.2005.863187
Habibi ATahar S(2005)An approach for the verification of systemc designs using asmlProceedings of the Third international conference on Automated Technology for Verification and Analysis10.1007/11562948_8(69-83)Online publication date: 4-Oct-2005
https://dl.acm.org/doi/10.1007/11562948_8

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

Automated interface refinement for compositional verification

An Interface Theory for Program Verification

An assertion-based verification methodology for system-level design