SE3: Sequential Equivalence Checking for Non-Cycle-Accurate Design Transformations

You Li; Guannan Zhao; Yunqi He; Hai Zhou

doi:10.1109/DAC56929.2023.10247912

SE3: Sequential Equivalence Checking for Non-Cycle-Accurate Design Transformations

You Li^*, Guannan Zhao, Yunqi He, Hai Zhou

^*Corresponding author for this work

Electrical and Computer Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

3 Scopus citations

Abstract

In high-level design explorations, many useful optimizations transform a circuit into another with different operating cycles for a better trade-off between performance and resource usage. How to efficiently check their equivalence is critical and challenging since most existing equivalence checkers are designed for cycle-accurate circuits. This paper presents SE3, an efficient sequential equivalence checker without assumption on cycle-accuracy, latch mapping, or I/O interface of the checked circuits. It proves the equivalence of two circuits by computing an equivalence relation between the states of the two circuits and utilizes syntax abstraction to accelerate this process. Experimental results show that SE3 is significantly faster than state-of-the-art sequential equivalence checking algorithms.

Original language	English (US)
Title of host publication	2023 60th ACM/IEEE Design Automation Conference, DAC 2023
Publisher	Institute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)	9798350323481
DOIs	https://doi.org/10.1109/DAC56929.2023.10247912
State	Published - 2023
Event	60th ACM/IEEE Design Automation Conference, DAC 2023 - San Francisco, United States Duration: Jul 9 2023 → Jul 13 2023

Publication series

Name	Proceedings - Design Automation Conference
Volume	2023-July
ISSN (Print)	0738-100X

Conference

Conference	60th ACM/IEEE Design Automation Conference, DAC 2023
Country/Territory	United States
City	San Francisco
Period	7/9/23 → 7/13/23

Funding

†∗Equal contribution. This work is partially supported by the National Science Foundation under grants 2113704 and 2148177.

Keywords

equivalence checking
model checking
quantifier elimination
sequential circuit

ASJC Scopus subject areas

Computer Science Applications
Control and Systems Engineering
Electrical and Electronic Engineering
Modeling and Simulation

Access to Document

10.1109/DAC56929.2023.10247912

Cite this

@inproceedings{e7279c37dd6e45fa9d812b12ed2c4c7f,

title = "SE3: Sequential Equivalence Checking for Non-Cycle-Accurate Design Transformations",

abstract = "In high-level design explorations, many useful optimizations transform a circuit into another with different operating cycles for a better trade-off between performance and resource usage. How to efficiently check their equivalence is critical and challenging since most existing equivalence checkers are designed for cycle-accurate circuits. This paper presents SE3, an efficient sequential equivalence checker without assumption on cycle-accuracy, latch mapping, or I/O interface of the checked circuits. It proves the equivalence of two circuits by computing an equivalence relation between the states of the two circuits and utilizes syntax abstraction to accelerate this process. Experimental results show that SE3 is significantly faster than state-of-the-art sequential equivalence checking algorithms.",

keywords = "equivalence checking, model checking, quantifier elimination, sequential circuit",

author = "You Li and Guannan Zhao and Yunqi He and Hai Zhou",

note = "Publisher Copyright: {\textcopyright} 2023 IEEE.; 60th ACM/IEEE Design Automation Conference, DAC 2023 ; Conference date: 09-07-2023 Through 13-07-2023",

year = "2023",

doi = "10.1109/DAC56929.2023.10247912",

language = "English (US)",

series = "Proceedings - Design Automation Conference",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

booktitle = "2023 60th ACM/IEEE Design Automation Conference, DAC 2023",

address = "United States",

}

Li, Y, Zhao, G, He, Y & Zhou, H 2023, SE3: Sequential Equivalence Checking for Non-Cycle-Accurate Design Transformations. in 2023 60th ACM/IEEE Design Automation Conference, DAC 2023. Proceedings - Design Automation Conference, vol. 2023-July, Institute of Electrical and Electronics Engineers Inc., 60th ACM/IEEE Design Automation Conference, DAC 2023, San Francisco, United States, 7/9/23. https://doi.org/10.1109/DAC56929.2023.10247912

SE3: Sequential Equivalence Checking for Non-Cycle-Accurate Design Transformations. / Li, You; Zhao, Guannan; He, Yunqi et al.
2023 60th ACM/IEEE Design Automation Conference, DAC 2023. Institute of Electrical and Electronics Engineers Inc., 2023. (Proceedings - Design Automation Conference; Vol. 2023-July).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - SE3

T2 - 60th ACM/IEEE Design Automation Conference, DAC 2023

AU - Li, You

AU - Zhao, Guannan

AU - He, Yunqi

AU - Zhou, Hai

PY - 2023

Y1 - 2023

N2 - In high-level design explorations, many useful optimizations transform a circuit into another with different operating cycles for a better trade-off between performance and resource usage. How to efficiently check their equivalence is critical and challenging since most existing equivalence checkers are designed for cycle-accurate circuits. This paper presents SE3, an efficient sequential equivalence checker without assumption on cycle-accuracy, latch mapping, or I/O interface of the checked circuits. It proves the equivalence of two circuits by computing an equivalence relation between the states of the two circuits and utilizes syntax abstraction to accelerate this process. Experimental results show that SE3 is significantly faster than state-of-the-art sequential equivalence checking algorithms.

AB - In high-level design explorations, many useful optimizations transform a circuit into another with different operating cycles for a better trade-off between performance and resource usage. How to efficiently check their equivalence is critical and challenging since most existing equivalence checkers are designed for cycle-accurate circuits. This paper presents SE3, an efficient sequential equivalence checker without assumption on cycle-accuracy, latch mapping, or I/O interface of the checked circuits. It proves the equivalence of two circuits by computing an equivalence relation between the states of the two circuits and utilizes syntax abstraction to accelerate this process. Experimental results show that SE3 is significantly faster than state-of-the-art sequential equivalence checking algorithms.

KW - equivalence checking

KW - model checking

KW - quantifier elimination

KW - sequential circuit

UR - http://www.scopus.com/inward/record.url?scp=85173097435&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85173097435&partnerID=8YFLogxK

U2 - 10.1109/DAC56929.2023.10247912

DO - 10.1109/DAC56929.2023.10247912

M3 - Conference contribution

AN - SCOPUS:85173097435

T3 - Proceedings - Design Automation Conference

BT - 2023 60th ACM/IEEE Design Automation Conference, DAC 2023

PB - Institute of Electrical and Electronics Engineers Inc.

Y2 - 9 July 2023 through 13 July 2023

ER -

SE3: Sequential Equivalence Checking for Non-Cycle-Accurate Design Transformations

Abstract

Publication series

Conference

Funding

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this