Article

Cost-Efficient Block Verification for a UMTS Up-Link Chip-Rate Coprocessor

Authors:

Klaus Winkelmann,

Hans-Joachim Trylus,

Dominik Stoffel,

Görschwin FeyAuthors Info & Claims

DATE '04: Proceedings of the conference on Design, automation and test in Europe - Volume 1

Page 10162

Published: 16 February 2004 Publication History

Get Access

Abstract

ASIC designs for future communication applications cannot be simulated exhaustively. Formal Property Checking is a powerful technology to overcome the limitations of current functional verification approaches. The paper reports on a large-scale experiment employingthe CVE property checker for verifying the block-level functional correctness of a large ASIC.This new verification methodology achieves substantial quality and productivity gains. The two biggest advantages are:Coding and Verification can be done in parallel.The whole state space of a test case will be verifiedin a single run.Formal Property Checking simplifies and shortens the functional verification of large-scale ASICs at least in the same order of magnitude as Static Timing Analysis did for timing verification.

References

[1]

{1} Biere, A. and Cimatti, A. and Clarke, E.M. and Zhu, Y. Symbolic Model Checking Without BDDs. TACAS'99, number 1579 in LNCS, pp. 193-207, 1999.

Google Scholar

[2]

{2} J. Bormann, C. Spalinger, Formale Verifikation für Nicht-Formalisten , IT+TI 2/2001.

Google Scholar

[3]

{3} R. Brinkmann, Using Symmetry for Problem Reduction in Bounded Model Checking on the Register-Transfer Level, SymCon 01, Paphos, Cyprus, 2001.

Google Scholar

[4]

{4} P. Johannsen, Booster: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstraction, Proceedings CAV'01, pp. 373-377, 2001.

Crossref

Google Scholar

[5]

{5} P. Johannsen, Reducing Bitvector Satisfiability Problems to Scale Down Design Sizes for RTL Property Checking, Proceedings HLDVT'01, pp. 123-128, 2001.

Digital Library

Google Scholar

[6]

{6} P. Johannsen, R. Drechsler, Formal Verification on the RT Level - Computing One-To-One Design Abstractions by Signal Width Reduction, Proceedings VLSI-SOC'01, 2001.

Google Scholar

[7]

{7} D. Stoffel, W. Kunz, Verification of Integer Multipliers on the Arithmetic Bit Level, Proceedings IEEE/ACM Intl. Conference on Computer-Aided Design (ICCAD-01), pp. 183-189, 2001.

Digital Library

Google Scholar

Cited By

View all

Grosse DWille RKuehne UDrechsler RLombardi FBhanja SMassoud YBahar R(2009)Contradictory antecedent debugging in bounded model checkingProceedings of the 19th ACM Great Lakes symposium on VLSI10.1145/1531542.1531586(173-176)Online publication date: 10-May-2009
https://dl.acm.org/doi/10.1145/1531542.1531586
Schönherr JFreibothe MStraube BBormann J(2008)Semi-formal verification of the steady state behavior of mixed-signal circuits by SAT-based property checkingTheoretical Computer Science10.1016/j.tcs.2008.03.032404:3(293-307)Online publication date: 1-Sep-2008
https://dl.acm.org/doi/10.1016/j.tcs.2008.03.032
Große DKühne UDrechsler RLauwereins RMadsen J(2007)Estimating functional coverage in bounded model checkingProceedings of the conference on Design, automation and test in Europe10.5555/1266366.1266620(1176-1181)Online publication date: 16-Apr-2007
https://dl.acm.org/doi/10.5555/1266366.1266620
Show More Cited By

Index Terms

Cost-Efficient Block Verification for a UMTS Up-Link Chip-Rate Coprocessor

Recommendations

Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
Efficient and User-Friendly Verification

A compositional verification method from a high-level resource-management standpoint is presented for dense-time concurrent systems and implemented in the tool of SGM (State-Graph Manipulators) with graphical user interface. SGM packages sophisticated ...
Compositional reachability analysis for efficient modular verification of asynchronous designs

Compositional verification is essential to address state explosion in model checking. Traditionally, an over-approximate context is needed for each individual component in a system for sound verification. This may cause state explosion for the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DATE '04: Proceedings of the conference on Design, automation and test in Europe - Volume 1

February 2004

688 pages

ISBN:0769520855

Publisher

IEEE Computer Society

United States

Publication History

Published: 16 February 2004

Check for updates

Qualifiers

Article

Conference

DATE04

Sponsor:

SIGDA

DATE04: Design, Automation and Test in Europe 2004

February 16 - 20, 2004

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

7
Total Citations
View Citations
110
Total Downloads

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

Reflects downloads up to 25 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Grosse DWille RKuehne UDrechsler RLombardi FBhanja SMassoud YBahar R(2009)Contradictory antecedent debugging in bounded model checkingProceedings of the 19th ACM Great Lakes symposium on VLSI10.1145/1531542.1531586(173-176)Online publication date: 10-May-2009
https://dl.acm.org/doi/10.1145/1531542.1531586
Schönherr JFreibothe MStraube BBormann J(2008)Semi-formal verification of the steady state behavior of mixed-signal circuits by SAT-based property checkingTheoretical Computer Science10.1016/j.tcs.2008.03.032404:3(293-307)Online publication date: 1-Sep-2008
https://dl.acm.org/doi/10.1016/j.tcs.2008.03.032
Große DKühne UDrechsler RLauwereins RMadsen J(2007)Estimating functional coverage in bounded model checkingProceedings of the conference on Design, automation and test in Europe10.5555/1266366.1266620(1176-1181)Online publication date: 16-Apr-2007
https://dl.acm.org/doi/10.5555/1266366.1266620
Fey GGroße DDrechsler RGielen G(2006)Avoiding false negatives in formal verification for protocol-driven blocksProceedings of the conference on Design, automation and test in Europe: Proceedings10.5555/1131481.1131820(1225-1226)Online publication date: 6-Mar-2006
https://dl.acm.org/doi/10.5555/1131481.1131820
Groβe DKühne UDrechsler RQu GIsmail YNarayanan VZhou H(2006)HW/SW co-verification of embedded systems using bounded model checkingProceedings of the 16th ACM Great Lakes symposium on VLSI10.1145/1127908.1127920(43-48)Online publication date: 30-Apr-2006
https://dl.acm.org/doi/10.1145/1127908.1127920
Wedler MStoffel DKunz WJoyner WMartin GKahng A(2005)Normalization at the arithmetic bit levelProceedings of the 42nd annual Design Automation Conference10.1145/1065579.1065699(457-462)Online publication date: 13-Jun-2005
https://dl.acm.org/doi/10.1145/1065579.1065699
Große DDrechsler R(2005)Acceleration of SAT-based iterative property checkingProceedings of the 13 IFIP WG 10.5 international conference on Correct Hardware Design and Verification Methods10.1007/11560548_29(349-353)Online publication date: 3-Oct-2005
https://dl.acm.org/doi/10.1007/11560548_29

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

Efficient Verification of Sequential and Concurrent C Programs

Efficient and User-Friendly Verification

Compositional reachability analysis for efficient modular verification of asynchronous designs