Article

Automated equivalence checking of switch level circuits

Authors:

Atanas Parashkevov,

Tim McDougallAuthors Info & Claims

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

Pages 299 - 304

https://doi.org/10.1145/513918.513996

Published: 10 June 2002 Publication History

Abstract

A chip that is required to meet strict operating criteria in terms of speed, power, or area is commonly custom designed at the switch level. Traditional techniques for verifying these designs, based on simulation, are expensive in terms of resources and cannot completely guarantee correct operation. Formal verification methods, on the other hand, provide for a complete proof of correctness, and require less effort to setup. This paper presents Motorola's Switch Level Verification (SLV) tool, which employs detailed switch level analysis to model the behavior of MOS transistors and obtain an equivalent RTL model. This tool has been used for equivalence checking at the switch level for several years within Motorola for the PowerPC, M*Core and DSP custom blocks. We focus on the novel techniques employed in SLV, particularly in the areas of pre-charged and sequential logic analysis, and provide details on the automated and integrated equivalence checking flow in which the tool is used.

References

[1]

Andersen, H.R., and Hulgaard, H. Boolean Expression Diagrams. LICS'97, pp. 88--98, 1997.

Digital Library

[2]

Bryant, R.E. Boolean analysis of MOS circuits. IEEE Transactions on CAD-ICS, vol. 6, no. 4, pp. 634--649, July 1987.

Digital Library

[3]

Bryant, R.E. Algorithmic aspects of symbolic switch network analysis. IEEE Transactions on CAD-ICS, vol. 6, no. 4, pp. 618--633, July 1987.

Digital Library

[4]

Bryant, R.E. Extraction of gate level models from transistor circuits by four-valued symbolic analysis. Fujitsu Labs Ltd., April 1991

[5]

Bryant, R.E. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, vol. C-35, pp.677--691, August 1986.

Digital Library

[6]

Brzozowski, J.A., and Yoeli, M. Combinational Static CMOS Networks. Integration, the VLSI Journal, 5, pp. 103--122, 1987.

Digital Library

[7]

Groupe Bull. Generalized recognition of gates: User Guide. Version 06, April 1996.

[8]

Gu, J., Purdom, P.W., Franco, J., and Wah, B.W. Algorithms for the satisfiability (SAT) problem: a survey. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, pp. 19--152, 1997.

[9]

IEEE. 1364--1995, Verilog Language Reference Manual. 1995.

[10]

Jain, S., Bryant, R.E., and Jain, A. Automatic clock abstraction from sequential circuits. DAC'95, pp. 707--711, 1995.

Digital Library

[11]

Kam, T., and Subrahmanyam, P.A. Comparing layouts with HDL models: a formal verification technique. IEEE Transactions on CAD-ICS, vol. 14, no. 4, pp. 503--509, April 1995.

Digital Library

[12]

Kuehlmann, A., Srinivasan, A., and LaPotin, D.P. Verity-a formal verification program for custom CMOS circuits. IBM Journal of Research and Development, vol. 39, no 1,2, January/March 1995.

Digital Library

[13]

Kundu, S. GateMaker: A Transistor to Gate Level Model Extractor for Simulation, Automatic Test Pattern Generation and Verification. IEEE International Test Conference, pp. 372--381, 1998.

Digital Library

[14]

Laurentin, M., Greiner, A., and Marbot, R. DESB, a functional abstractor for CMOS VLSI circuits. EDAC'92, pp. 22--27, 1992.

Digital Library

[15]

Malik, S. Analysis of cyclic combinational circuits. ICCAD'93, pp. 618--625, 1993.

Digital Library

[16]

McDougall, T., Parashkevov, A., Jolly, S., Zhu, J., Zeng, J., Pyron, C., and Abadir, M. SLV/ATPG: An Automated Flow for Test Model Generation from Switch Level Custom Circuits. Submitted to MTV 02

[17]

Synopsys. Synopsys Online Documentation. Version 2001.08, August 2001.

[18]

Verplex Systems. Logical Equivalence Checker Reference Manual version 3.0. August 2001.

Cited By

Trukhachev AIvanova N(2017)Extracting of High-Level Structural Representation from VLSI Circuit Description Using Tangled Logic StructuresBiologically Inspired Cognitive Architectures (BICA) for Young Scientists10.1007/978-3-319-63940-6_45(318-323)Online publication date: 26-Jul-2017
https://doi.org/10.1007/978-3-319-63940-6_45
Javaheri MSedaghat RKant LZalev J(2006)Verification and fault synthesis algorithm at switch-levelMicroprocessors and Microsystems10.1016/j.micpro.2005.12.00230:4(199-208)Online publication date: Jun-2006
https://doi.org/10.1016/j.micpro.2005.12.002
Ejlali AMiremadi EGetreu IFix LLavagno L(2003)Switch-level emulationProceedings of the 40th annual Design Automation Conference10.1145/775832.775996(644-649)Online publication date: 2-Jun-2003
https://dl.acm.org/doi/10.1145/775832.775996
Show More Cited By

Index Terms

Automated equivalence checking of switch level circuits
1. Applied computing
  1. Arts and humanities
    1. Architecture (buildings)
      1. Computer-aided design
  2. Physical sciences and engineering
    1. Engineering
      1. Computer-aided design

Recommendations

An Equivalence-Checking Method for Scheduling Verification in High-Level Synthesis

A formal method for checking equivalence between a given behavioral specification prior to scheduling and the one produced by the scheduler is described. Finite state machine with data path (FSMD) models have been used to represent both the behaviors. ...
Formal verification of code motion techniques using data-flow-driven equivalence checking
Special section on verification challenges in the concurrent world

A formal verification method for checking correctness of code motion techniques is presented in this article. Finite State Machine with Datapath (FSMD) models have been used to represent the input and the output behaviors of each synthesis step. The ...
Leveraging sequential equivalence checking to enable system-level to RTL flows
DAC '08: Proceedings of the 45th annual Design Automation Conference

It has long been the practice to create models in C or C++ for architectural studies, software prototyping and RTL verification in the design of Systems-on-Chip (SoC). It is often the case that by the end of a design project, multiple C models exist for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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

Copyright © 2002 ACM.

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]

Sponsors

SIGDA: ACM Special Interest Group on Design Automation

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

4
Total Citations
View Citations
15
Total Downloads

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

Reflects downloads up to 09 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Trukhachev AIvanova N(2017)Extracting of High-Level Structural Representation from VLSI Circuit Description Using Tangled Logic StructuresBiologically Inspired Cognitive Architectures (BICA) for Young Scientists10.1007/978-3-319-63940-6_45(318-323)Online publication date: 26-Jul-2017
https://doi.org/10.1007/978-3-319-63940-6_45
Javaheri MSedaghat RKant LZalev J(2006)Verification and fault synthesis algorithm at switch-levelMicroprocessors and Microsystems10.1016/j.micpro.2005.12.00230:4(199-208)Online publication date: Jun-2006
https://doi.org/10.1016/j.micpro.2005.12.002
Ejlali AMiremadi EGetreu IFix LLavagno L(2003)Switch-level emulationProceedings of the 40th annual Design Automation Conference10.1145/775832.775996(644-649)Online publication date: 2-Jun-2003
https://dl.acm.org/doi/10.1145/775832.775996
McDougall TParashkevov AJolly SZhu JZeng JPyron CAbadir MYasuura H(2003)An automated method for test model generation from switch level circuitsProceedings of the 2003 Asia and South Pacific Design Automation Conference10.1145/1119772.1119943(769-774)Online publication date: 21-Jan-2003
https://dl.acm.org/doi/10.1145/1119772.1119943

View Options

Get Access

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents