Supervisors:
Prof. Pallab Dasgupta
Prof. Partha Pratim Chakrabarti
Title: Formal Methods for Effective Verification of Local Design Changes
Abstract: Large digital integrated circuits typically consist of multiple functional units
integrated using glue logic. The main functional units in the design are typically extensively
verified using both formal and simulation techniques, whereas the glue logic (tribal logic),
which accounts for a large fraction of the integrated circuit (40% or above), is not well-documented
and not formally verified in industrial practice. The glue logic is often modified
locally late in the design cycle for (a) fixing bugs which often appear due to incorrect
interpretation of the architecture in specific corner case scenarios, (b) intent modification
which is performed later in the design cycle and the component is modified accordingly.
Both these two kinds of changes are expected to have local side effects. However, these
local changes may indirectly affect a much larger portion of the glue logic, and it is nontrivial
to determine the exact boundary of the cone-of-influence of that change. Therefore
model checking or sequential equivalence checking on the glue logic in its entirety does
not scale. In this research, we propose methodologies for effectively verifying such local
design changes at a global level, without attempting to apply formal methods on the entire
glue logic.