High-Level Engineering Change Through Programmable Datapath and SMT Solvers

In this paper, we present a technique to automatically adjust Register-transfer level (RTL) implementation for Engineering Change Order (ECO) in high level. Our method focuses on the datapath structure, where circuit topologies are mostly, and only partial portions are replaced by programmable datapath. Exploring the correct configuration of the datapath is formulated as Quantified Boolean Formula (QBF) problem, and can be solved by using Satisfiability (SAT) /Satisfiability Modulo Theories (SMT) solver in an incremental way automatically. The experimental results with several example cases have confirmed that effectiveness of the proposed method.