Thumbnail
Access Restriction
Open

Author Khasidashvili, Zurab ♦ Skaba, Marcelo ♦ Kaiss, Daher ♦ Hanna, Ziyad
Source CiteSeerX
Content type Text
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Sequential Hardware Equivalence ♦ Subcircuit Environment ♦ Intel Design ♦ Theoretical Framework ♦ Alignability Equivalence ♦ Classical Alignability Theory ♦ Alignability Verification ♦ Conquer Framework ♦ Design Constraint ♦ Compositional Sequential Hardware Equivalence Verification ♦ Synchronous Sequential Circuit ♦ Large Industrial Design ♦ Compositionality Result ♦ Essential Behavior
Description We are interested in sequential hardware equivalence (or alignability equivalence) verification of synchronous sequential circuits [Pix92]. 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. 1.
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 2004-01-01
Publisher Institution in Presence of Design Constraints, Proceedings of the International Conference on Computer Aided Design, IEEE