invited-talk

ICCAD-2020 CAD contest in X-value equivalence checking and benchmark suite

Authors:

Chih-Jen (Jacky) Hsu,

Chi-An (Rocky) Wu,

Ching-Yi Huang,

Kei-Yong KhooAuthors Info & Claims

ICCAD '20: Proceedings of the 39th International Conference on Computer-Aided Design

Article No.: 68, Pages 1 - 4

https://doi.org/10.1145/3400302.3415739

Published: 17 December 2020 Publication History

Get Access

Abstract

Equivalence checking is the practical industrial solution to sign-off digital functionality for large-scale circuits. However, when design contains implicit and explicit X-values, the complexity of equivalence checking increases and heuristics used in binary-value equivalence checking may not be applicable for X-value equivalence checking. The goal of the ICCAD 2020 CAD contest is to ask the good algorithm and heuristic to solve the X-value equivalence checking. In this contest, we provide the benchmark suites for contestant to evaluate their program. We hope the contest result can improve industry applications and bring more research interests.

References

[1]

A. Kuehlmann and F. Krohm. "Equivalence checking using cuts and heaps," Design Automation Conference (DAC '97).

Digital Library

Google Scholar

[2]

E. I. Goldberg, M. R. Prasad and R. K. Brayton, "Using SAT for combinational equivalence checking," Design, Automation and Test in Europe. (DATE 2001)

Digital Library

Google Scholar

[3]

A. Mishchenko, R. Brayton, J.-H. Jiang, and S. Jang. "Scalable don't-care-based logic optimization and resynthesis," International symposium on Field programmable gate arrays (FPGA '09).

Digital Library

Google Scholar

[4]

IEEE Standard for Design and Verification of Low-Power, Energy-Aware Electronic Systems," in IEEE Std 1801--2018

Google Scholar

[5]

IEEE Standard Verilog Hardware Description Language," in IEEE Std 1364--2001

Google Scholar

[6]

Cadence Genus Synthesis Tool. https://www.cadence.com/en_US/home/tools/digital-design-and-signoff/synthesis/genus-synthesis-solution.html

Google Scholar

[7]

Candece Conformal LEC Tool. https://www.cadence.com/en_US/home/tools/digital-design-and-signoff/logic-equivalence-checking.html

Google Scholar

Cited By

View all

Mirkovic MMirkovic D(2024)Propagation Time Minimization of the on-Chip Critical Signal Path2024 11th International Conference on Electrical, Electronic and Computing Engineering (IcETRAN)10.1109/IcETRAN62308.2024.10645177(1-4)Online publication date: 3-Jun-2024
https://doi.org/10.1109/IcETRAN62308.2024.10645177
Sato TWang CChen YHuang T(2023)Invited Paper: Overview of 2023 CAD Contest at ICCAD2023 IEEE/ACM International Conference on Computer Aided Design (ICCAD)10.1109/ICCAD57390.2023.10323648(1-6)Online publication date: 28-Oct-2023
https://doi.org/10.1109/ICCAD57390.2023.10323648
Malik RBaunthiyal SKumar PJ SSaurabh S(2022)A Comparison of SAT-based and SMT-based Frameworks for X-value Combinational Equivalence Checking2022 IFIP/IEEE 30th International Conference on Very Large Scale Integration (VLSI-SoC)10.1109/VLSI-SoC54400.2022.9939646(1-6)Online publication date: 3-Oct-2022
https://doi.org/10.1109/VLSI-SoC54400.2022.9939646

Index Terms

ICCAD-2020 CAD contest in X-value equivalence checking and benchmark suite
1. Hardware
  1. Hardware validation
    1. Functional verification
      1. Equivalence checking

Recommendations

ICCAD-2015 CAD Contest in Large-scale Equivalence Checking and Function Correction and Benchmark Suite
ICCAD '15: Proceedings of the IEEE/ACM International Conference on Computer-Aided Design

Equivalence checking (EC) and functional Engineering Change Order (ECO) on large-scale designs becomes a crucial industrial topic as the design scale expands. In this topic, we are especially interested in how to partition the large-scale problems into ...
Proving Functional Equivalence of Two AES Implementations Using Bounded Model Checking
ICST '09: Proceedings of the 2009 International Conference on Software Testing Verification and Validation

Bounded model checking---as well as symbolic equivalence checking---are highly successful techniques in the hardware domain. Recently, bit-vector bounded model checkers like CBMC have been developed that are able to check properties of (mostly low-level)...
Using complete-1-distinguishability for FSM equivalence checking

This article introduces the notion of a Complete-1-Distinguishability (C-1-D) property for simplifying equivalence checking of finite state machines (FSMs). When a specification machine has the C-1-D property, the traversal of the product machine can be ...

Comments

Information & Contributors

Information

Published In

ICCAD '20: Proceedings of the 39th International Conference on Computer-Aided Design

November 2020

1396 pages

ISBN:9781450380263

DOI:10.1145/3400302

General Chair:
Yuan Xie
Univ. of California, Santa Barbara, CA

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 the author(s) 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].

In-Cooperation

IEEE CAS
IEEE CEDA
IEEE CS

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 December 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Invited-talk

Conference

ICCAD '20

Sponsor:

SIGDA

ICCAD '20: IEEE/ACM International Conference on Computer-Aided Design

November 2 - 5, 2020

Virtual Event, USA

Acceptance Rates

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
52
Total Downloads

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

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Mirkovic MMirkovic D(2024)Propagation Time Minimization of the on-Chip Critical Signal Path2024 11th International Conference on Electrical, Electronic and Computing Engineering (IcETRAN)10.1109/IcETRAN62308.2024.10645177(1-4)Online publication date: 3-Jun-2024
https://doi.org/10.1109/IcETRAN62308.2024.10645177
Sato TWang CChen YHuang T(2023)Invited Paper: Overview of 2023 CAD Contest at ICCAD2023 IEEE/ACM International Conference on Computer Aided Design (ICCAD)10.1109/ICCAD57390.2023.10323648(1-6)Online publication date: 28-Oct-2023
https://doi.org/10.1109/ICCAD57390.2023.10323648
Malik RBaunthiyal SKumar PJ SSaurabh S(2022)A Comparison of SAT-based and SMT-based Frameworks for X-value Combinational Equivalence Checking2022 IFIP/IEEE 30th International Conference on Very Large Scale Integration (VLSI-SoC)10.1109/VLSI-SoC54400.2022.9939646(1-6)Online publication date: 3-Oct-2022
https://doi.org/10.1109/VLSI-SoC54400.2022.9939646
Huang TChen YWang CSato T(2021)Overview of 2021 CAD Contest at ICCAD2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD)10.1109/ICCAD51958.2021.9643523(1-3)Online publication date: 1-Nov-2021
https://doi.org/10.1109/ICCAD51958.2021.9643523

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

ICCAD-2015 CAD Contest in Large-scale Equivalence Checking and Function Correction and Benchmark Suite

Proving Functional Equivalence of Two AES Implementations Using Bounded Model Checking

Using complete-1-distinguishability for FSM equivalence checking

Comments

Published In

Sponsors

In-Cooperation

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Conference

Acceptance Rates

Other Metrics

Article Metrics

Other Metrics

Cited By

Login options

Full Access

PDF

eReader

Abstract

References

Cited By

Index Terms

Recommendations

ICCAD-2015 CAD Contest in Large-scale Equivalence Checking and Function Correction and Benchmark Suite

Proving Functional Equivalence of Two AES Implementations Using Bounded Model Checking

Using complete-1-distinguishability for FSM equivalence checking

Comments

Information

Published In

Sponsors

In-Cooperation

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Conference

Acceptance Rates

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Login options

Full Access

View options

PDF

eReader

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations