2026-09-19T05:04:44Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/81909 2023-07-11 col_2142_5131 col_2142_10761 com_2142_5130 com_2142_10755 com_2142_234

Banerjee, Prithviraj Hasteer, Gagan 2015-09-25T20:20:57Z 2015-09-25T20:20:57Z 10000-01-01 1998 1998 We address the issue of transforming multi-phase designs, a popular industry practice to equivalent one-phase designs to enable the application of the current equivalence checking techniques. We propose an algorithm to compute the steady states of a machine by relaxing the assumption of a designated set of initial states (DIS). This assumption is used in research but is often restrictive in an industrial design environment. We use the paradigm of sequential hardware equivalence (SHE), which does not make the DIS assumption, for checking the equivalence of two machines. We show that two machines are SHE if the outputs of their product machine are 0 in the steady states. We propose machine partitioning and minimum area retiming to alleviate the problem of large state spaces common in industrial designs. Our techniques result in exponential reductions in the state space and enable equivalence checking of machines which cannot be handled otherwise. Lastly, we address the issue of interface verification arising out of a modular design environment. We show that the constraints required to express the input don't care space for equivalence checking of a module need to be verified formally for the completeness of equivalence checking. We characterize these constraints as combinationally provable and sequentially provable. Subsequently, we develop an assertion checking framework with efficient techniques to handle both types of constraints. Made available in DSpace on 2015-09-25T20:20:57Z (GMT). No. of bitstreams: 2 license.txt: 4848 bytes, checksum: 96035ab3f5e1c23cc7138a224ce498bd (MD5) 9834686.pdf: 3770184 bytes, checksum: db440e8ad837a7c4f1e8d84d36f67014 (MD5) Previous issue date: 1998 Embargo set by: Seth Robbins for item 83190 Lift date: Forever Reason: Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs U of I Only 128 p. Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 1998. http://hdl.handle.net/2142/81909 (MiAaPQ)AAI9834686 eng Computer Science Efficient Equivalence Checking in a Modular Design Environment text Computer Science Computer Science University of Illinois at Urbana-Champaign Dissertation Ph.D.