Specifying and verifying imprecise sequential datapaths by Arithmetic Transforms
Katarzyna Radecka, Željko Žilić · Digest of technical papers/Digest of technical papers - IEEE/ACM International Conference on Computer-Aided Design · 2002
We address verification of imprecise datapath circuits with sequential elements. Using Arithmetic Transform (AT) and its extensions, we verify the sequential datapath circuits with finite precision. An efficient formulation of the precision verification is presented as a polynomial maximization search over Boolean inputs. Using a branch-and-bound search for the precision error and the block-level composition of ATs, we verify the approximated, rounded and truncated pipelined datapaths.