Formalization of Rectification Learning for Economic Design Updates

Engineering Change Order (ECO) is the task of finding the non-intrusive design implementation updates to comply with a specification revision. This paper states the rectification problem in quantified Boolean logic that gives sound and complete capture of the update choices for an ECO. Its closed-form statement offers an analytical search for small patches that maximize logic sharing in the implementation. With the abstraction-refinement paradigm assisted by relevance classification, we effectively generalize the sampled knowledge of a revision, enabling the identification of compact updates without undue computational costs. Our experimental evaluation demonstrates almost twice as few gates in synthesized patches compared to the reported state-of-the-art results.