Article

Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints

Authors:

Z. Khasidashvili,

Z. HannaAuthors Info & Claims

ICCAD '04: Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design

Pages 58 - 65

https://doi.org/10.1109/ICCAD.2004.1382543

Published: 07 November 2004 Publication History

Abstract

We are interested in sequential hardware equivalence (or alignability equivalence) verification of synchronous sequential circuits as stated in C. Pixley (1992). To cope with large industrial designs, the circuits must be divided into smaller subcircuits and verified separately. Furthermore, in order to succeed in verifying the subcircuits, design constraints must be added to the subcircuits. These constraints mimic "essential" behavior of the subcircuit environment. In this work, we extend the classical alignability theory in the presence of design constraints, and prove a compositionality result allowing inferring alignability of the circuits from alignability of the subcircuits. As a result, we build a divide and conquer framework for alignability verification. This framework is successfully used on Intel designs.

References

[1]

{BCC99} Biere, A., A. Cimatti, and E. Clarke, Symbolic model checking without BDDs, Tools and Algorithms for the Construction and Analysis of Systems, 1999.

Digital Library

[2]

{Bry86} Bryant R.E., Graph-based algorithms for Boolean function manipulation, IEEE Trans. Computers, C-35(8), 1986.

Digital Library

[3]

{CA89} Cheng K.-T. and D. Agrawal, State assignment for initializable synthesis, ICCAD'89, 1989.

[4]

{CGP99} Clarke E.M., O. Grumberg, D.A. Peled, Model Checking, MIT Press, 1999.

Digital Library

[5]

{DLL62} Davis, M., G. Logemann and D. Loveland, A machine program for theorem-proving, Communications of ACM 5(7), 1962.

Digital Library

[6]

{HS98} Hachtel G.D. and F. Somenzi, Logic Synthesis and Verification Algorithms, Kluwer Academic Publishers, 1998.

Digital Library

[7]

{HCC01} Huang, S.-Y., K.-T., Cheng, and K.-C. Chen, Verifying sequential equivalence using ATPG techniques, ACM Trans. on Design Automation of Electronic Systems, 2001.

Digital Library

[8]

{KRSH04} Kaiss, D., A. Rosenmann, M. Skaba and Z. Hanna, A formal method and apparatus for an automatic synchronization of finite state machines for sequential verification of chip design, US Patent application, 2004.

[9]

{KH03} Khasidashvili, Z., Z. Hanna, SAT-Based methods for sequential hardware equivalence verification without synchronization, BMC'03, ENTCS 89 (4), 2003.

[10]

{Koh78} Kohavi, Z., Switching and Finite Automata Theory, McGraw-Hill, 1978.

Digital Library

[11]

{Par81} Park, D. Concurrency and automata on infinite sequences, 5th GI-Conference on Theoretical Computer Science, Springer LNCS, vol. 104, 1981.

Digital Library

[12]

{Pix92} Pixley, C., A theory and implementation of sequential hardware equivalence, IEEE transactions on CAD, 1992.

[13]

{Pnu85} Pnueli, A., In transition from global to modular temporal reasoning about programs, In: Logics and Models of Concurrent Systems, Springer LNCS, vol. F-13 of NATO ASI series, 1985.

Digital Library

[14]

{PR96} Pomeranz, I. and S.M. Reddy, On removing redundancies from synchronous sequential circuits with synchronizing sequences, IEEE Trans. Computers, 1996.

Digital Library

[15]

{RH02} Rosenmann, A. and Z. Hanna, Alignability equivalence of synchronous sequential circuits, HLDVT'02, 2002.

Digital Library

[16]

{SPAB01} Singhal, V., C. Pixley, A. Aziz, and R.K. Brayton, Theory of Safe replacement for sequential circuits, IEEE Trans. on CAD of integrated circuits and systems, vol. 20, n. 2, 2001.

Digital Library

Cited By

Lu HXing YGupta AMalik S(2023)SoC Protocol Implementation Verification Using Instruction-Level Abstraction SpecificationsACM Transactions on Design Automation of Electronic Systems10.1145/361029228:6(1-24)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3610292
Eisner CNahir AYorav K(2009)Functional verification of power gated designs by compositional reasoningFormal Methods in System Design10.1007/s10703-009-0077-x35:1(40-55)Online publication date: 1-Aug-2009
https://dl.acm.org/doi/10.1007/s10703-009-0077-x
Khasidashvili Z(2008)On formal equivalence verification of hardwareProceedings of the 3rd international conference on Computer science: theory and applications10.5555/1813695.1813700(11-12)Online publication date: 7-Jun-2008
https://dl.acm.org/doi/10.5555/1813695.1813700
Show More Cited By

Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints
1. Theory of computation

Recommendations

Post-reboot Equivalence and Compositional Verification of Hardware
FMCAD '06: Proceedings of the Formal Methods in Computer Aided Design

We introduce a finer concept of a Hardware Machine, where the set of post-reboot operation states is explicitly a part of the FSM definition. We formalize an ad-hoc flow of combinational equivalence verification of hardware, the way it was performed ...
Compositional verification of retiming and sequential optimizations
DAC '08: Proceedings of the 45th annual Design Automation Conference

Once a design is both retimed and sequentially optimized, sequential equivalence verification becomes very hard since retiming breaks the equivalence of the retimed sub-blocks although the design equivalence is preserved.

This paper presents a novel ...
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. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICCAD '04: Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design

November 2004

913 pages

ISBN:0780387023

Sponsors

SIGDA: ACM Special Interest Group on Design Automation

Publisher

IEEE Computer Society

United States

Publication History

Published: 07 November 2004

Check for updates

Qualifiers

Article

Conference

ICCAD04

Sponsor:

SIGDA

ICCAD04: The International Conference on Computer-Aided Design 2004

November 7 - 11, 2004

Acceptance Rates

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
104
Total Downloads

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

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lu HXing YGupta AMalik S(2023)SoC Protocol Implementation Verification Using Instruction-Level Abstraction SpecificationsACM Transactions on Design Automation of Electronic Systems10.1145/361029228:6(1-24)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3610292
Eisner CNahir AYorav K(2009)Functional verification of power gated designs by compositional reasoningFormal Methods in System Design10.1007/s10703-009-0077-x35:1(40-55)Online publication date: 1-Aug-2009
https://dl.acm.org/doi/10.1007/s10703-009-0077-x
Khasidashvili Z(2008)On formal equivalence verification of hardwareProceedings of the 3rd international conference on Computer science: theory and applications10.5555/1813695.1813700(11-12)Online publication date: 7-Jun-2008
https://dl.acm.org/doi/10.5555/1813695.1813700
Moon IFix L(2008)Compositional verification of retiming and sequential optimizationsProceedings of the 45th annual Design Automation Conference10.1145/1391469.1391506(131-136)Online publication date: 8-Jun-2008
https://dl.acm.org/doi/10.1145/1391469.1391506
Eisner CNahir AYorav K(2008)Functional Verification of Power Gated Designs by Compositional ReasoningProceedings of the 20th international conference on Computer Aided Verification10.1007/978-3-540-70545-1_42(433-445)Online publication date: 7-Jul-2008
https://dl.acm.org/doi/10.1007/978-3-540-70545-1_42
Bischoff GBrace KCabodi G(2007)A compositional approach for equivalence checking of sequential circuits with unknown reset state and overlapping partitionsProceedings of the 11th international conference on Computer aided systems theory10.5555/1783034.1783104(505-514)Online publication date: 12-Feb-2007
https://dl.acm.org/doi/10.5555/1783034.1783104
Moon IBjesse PPixley CLauwereins RMadsen J(2007)A compositional approach to the combination of combinational and sequential equivalence checking of circuits without known reset statesProceedings of the conference on Design, automation and test in Europe10.5555/1266366.1266619(1170-1175)Online publication date: 16-Apr-2007
https://dl.acm.org/doi/10.5555/1266366.1266619
Mathur AKrishnaswamy VLevitan S(2007)Design for verification in system-level models and RTLProceedings of the 44th annual Design Automation Conference10.1145/1278480.1278528(193-198)Online publication date: 4-Jun-2007
https://dl.acm.org/doi/10.1145/1278480.1278528
Vardi MLevitan S(2007)Formal techniques for SystemC verificationProceedings of the 44th annual Design Automation Conference10.1145/1278480.1278527(188-192)Online publication date: 4-Jun-2007
https://dl.acm.org/doi/10.1145/1278480.1278527
Khasidashvili ZNadel APalti AHanna Z(2005)Simultaneous SAT-Based model checking of safety propertiesProceedings of the First Haifa international conference on Hardware and Software Verification and Testing10.1007/11678779_5(56-75)Online publication date: 13-Nov-2005
https://dl.acm.org/doi/10.1007/11678779_5

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