Title :
Specifying and verifying imprecise sequential datapaths by arithmetic transforms
Author :
Radecka, Katarzyna ; Zilic, Zeljko
Author_Institution :
Concordia Univ., Montreal, Que., Canada
Abstract :
We address verification of imprecise datapath circuits with sequential elements. Using the arithmetic transform (AT) and its extensions, we verify the sequential datapath circuits with finite precision. An efficient formulation of 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.
Keywords :
Boolean functions; digital arithmetic; formal verification; industrial property; integrated circuit design; integrated circuit modelling; integrated circuit testing; logic design; logic testing; pipeline arithmetic; sequential circuits; transforms; tree searching; AT block-level composition; AT extensions; Boolean input polynomial maximization search; IP core reuse; approximated/rounded/truncated pipelined datapaths; arithmetic circuits; arithmetic transforms; finite precision verification; imprecise sequential datapath circuit specification/verification; pipelined circuits; precision error branch-and-bound searching; sequential elements; Adders; Arithmetic; Binary decision diagrams; Boolean functions; Circuit testing; Cost accounting; Decoding; Intellectual property; Polynomials;
Conference_Titel :
Computer Aided Design, 2002. ICCAD 2002. IEEE/ACM International Conference on
Print_ISBN :
0-7803-7607-2
DOI :
10.1109/ICCAD.2002.1167524
