Article

RTL c-based methodology for designing and verifying a multi-threaded processor

Authors:

Daniel NgAuthors Info & Claims

DAC '02: Proceedings of the 39th annual Design Automation Conference

Pages 123 - 128

https://doi.org/10.1145/513918.513951

Published: 10 June 2002 Publication History

Get Access

Abstract

A RTL C-Based design and verification methodology is presented with enabled the successful high speed validation of a 7 million gate simultaneous multi-threaded (SMT) network processor. The methodology is centered on statically scheduled C-based coding style, C to HDL translation, and a novel RTL-C to RTL-Verilog equivalence checking flow. It leverages improved simulation performance combined with static techniques to reduce the amount of RTL-Verilog and gate-level verification required during development.

References

[1]

Avant! corp, Design Verifyer, http://www.avanticorp.com/

Google Scholar

[2]

C Level Design, C2HDL, http://www.cleveldesign.com/

Google Scholar

[3]

CoWare, N2C, http://coware.com/

Google Scholar

[4]

Cynergy System Design, http://www.cynergysd.com

Google Scholar

Cited By

View all

Grossman JTowles BBank JShaw D(2013)The role of cascade, a cycle-based simulation infrastructure, in designing the anton special-purpose supercomputersProceedings of the 50th Annual Design Automation Conference10.1145/2463209.2488884(1-9)Online publication date: 29-May-2013
https://dl.acm.org/doi/10.1145/2463209.2488884
Velev MGao PPhillips JHu AGraeb H(2011)Automatic formal verification of multithreaded pipelined microprocessorsProceedings of the International Conference on Computer-Aided Design10.5555/2132325.2132476(679-686)Online publication date: 7-Nov-2011
https://dl.acm.org/doi/10.5555/2132325.2132476
Velev MGao P(2011)Automatic formal verification of multithreaded pipelined microprocessorsProceedings of the 2011 IEEE/ACM International Conference on Computer-Aided Design10.1109/ICCAD.2011.6105403(679-686)Online publication date: 7-Nov-2011
https://dl.acm.org/doi/10.1109/ICCAD.2011.6105403
Show More Cited By

Index Terms

RTL c-based methodology for designing and verifying a multi-threaded processor
1. Hardware
  1. Electronic design automation
  2. Hardware validation
    1. Functional verification
      1. Simulation and emulation

Recommendations

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog

As a first step, most model checkers used in the hardware industry convert a high-level register-transfer-level (RTL) design into a netlist. However, algorithms that operate at the netlist level are unable to exploit the structure of the higher ...
Building a standard ESL design and verification methodology: is it just a dream?
DAC '06: Proceedings of the 43rd annual Design Automation Conference
Early cutpoint insertion for high-level software vs. RTL formal combinational equivalence verification
DAC '06: Proceedings of the 43rd annual Design Automation Conference

Ever-growing complexity is forcing design to move above RTL. For example, golden functional models are being written as clearly as possible in software and not optimized or intended for synthesis. Thus, equivalence verification between the high-level ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DAC '02: Proceedings of the 39th annual Design Automation Conference

June 2002

956 pages

ISBN:1581134614

DOI:10.1145/513918

General Chair:
Bryan Ackland
Agere Systems, Inc., Holmdel, NJ

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: 10 June 2002

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

DAC02

Sponsor:

SIGDA

DAC02: 39th Design Automation Conference

June 10 - 14, 2002

Louisiana, New Orleans, USA

Acceptance Rates

DAC '02 Paper Acceptance Rate 147 of 491 submissions, 30%;

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

14
Total Citations
View Citations
47
Total Downloads

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

Reflects downloads up to 14 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Grossman JTowles BBank JShaw D(2013)The role of cascade, a cycle-based simulation infrastructure, in designing the anton special-purpose supercomputersProceedings of the 50th Annual Design Automation Conference10.1145/2463209.2488884(1-9)Online publication date: 29-May-2013
https://dl.acm.org/doi/10.1145/2463209.2488884
Velev MGao PPhillips JHu AGraeb H(2011)Automatic formal verification of multithreaded pipelined microprocessorsProceedings of the International Conference on Computer-Aided Design10.5555/2132325.2132476(679-686)Online publication date: 7-Nov-2011
https://dl.acm.org/doi/10.5555/2132325.2132476
Velev MGao P(2011)Automatic formal verification of multithreaded pipelined microprocessorsProceedings of the 2011 IEEE/ACM International Conference on Computer-Aided Design10.1109/ICCAD.2011.6105403(679-686)Online publication date: 7-Nov-2011
https://dl.acm.org/doi/10.1109/ICCAD.2011.6105403
Feng XHu ASentovich E(2006)Early cutpoint insertion for high-level software vs. RTL formal combinational equivalence verificationProceedings of the 43rd annual Design Automation Conference10.1145/1146909.1147178(1063-1068)Online publication date: 24-Jul-2006
https://dl.acm.org/doi/10.1145/1146909.1147178
(2006)Automatic decomposition for sequential equivalence checking of system level and RTL descriptionsProceedings of the Fourth ACM/IEEE International Conference on Formal Methods and Models for Co-Design10.1109/MEMCOD.2006.1695903(71-80)Online publication date: 1-Jan-2006
https://dl.acm.org/doi/10.1109/MEMCOD.2006.1695903
Koelbl ALu YMathur A(2005)Embedded tutorialProceedings of the 2005 IEEE/ACM International conference on Computer-aided design10.5555/1129601.1129737(965-971)Online publication date: 31-May-2005
https://dl.acm.org/doi/10.5555/1129601.1129737
Feng XHu AYang JTang T(2005)Partitioned model checking from software specificationsProceedings of the 2005 Asia and South Pacific Design Automation Conference10.1145/1120725.1120967(583-587)Online publication date: 18-Jan-2005
https://dl.acm.org/doi/10.1145/1120725.1120967
Rodrigues RCardoso J(2005)An Infrastructure to Functionally Test Designs Generated by Compilers Targeting FPGAsProceedings of the conference on Design, Automation and Test in Europe - Volume 110.1109/DATE.2005.60(30-31)Online publication date: 7-Mar-2005
https://dl.acm.org/doi/10.1109/DATE.2005.60
Cheung NParameswaran SHenkel JChan J(2004)MINCEProceedings of the conference on Design, automation and test in Europe - Volume 210.5555/968879.969146Online publication date: 16-Feb-2004
https://dl.acm.org/doi/10.5555/968879.969146
(2004)Verification of SpecC using predicate abstractionProceedings of the Second ACM/IEEE International Conference on Formal Methods and Models for Co-Design10.1109/MEMCOD.2004.1459808(7-16)Online publication date: 1-Jan-2004
https://dl.acm.org/doi/10.1109/MEMCOD.2004.1459808
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

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog

Building a standard ESL design and verification methodology: is it just a dream?

Early cutpoint insertion for high-level software vs. RTL formal combinational equivalence verification