Transcript Slide 1

Exploiting Vanishing Polynomials for
Equivalence Verification of Fixed-Size
Arithmetic Datapaths
Namrata Shekhar1, Priyank Kalla1, Florian Enescu2, Sivaram Gopalakrishnan1
1Department
of Electrical and Computer Engineering,
University of Utah, Salt Lake City, UT-84112.
2Department
of Mathematics and Statistics,
Georgia State University, Atlanta, GA-30303
Outline

Overall Verification Problem
• Our Focus: Equivalence Verification of Fixed-size Arithmetic
Datapaths
• Applications: Polynomial Signal Processing, etc.

Problem Modeling and Approach
• Polynomials over Finite Integer Rings

Limitations of Previous Work

Our Contributions
• Exploiting Vanishing Polynomials for Equivalence Test
• Related to Ideal Membership Testing

Algorithm Design and Experimental Verification Runs

Results

Conclusions & Future Work
The Equivalence Verification Problem
Fixed-Size (m) Data-path: Modeling

Control the datapath size: Fixed size bit-vectors (m)
16-bit
8-bit
*
8-bit

32-bit
*
8-bit
8-bit
8-bit
*
*
8-bit
Bit-vector of size m: integer values in 0,…, 2m-1
Fixed-size
(m) bit-vector
arithmetic
Polynomials
reduced %2m
Algebra over
the ring Z2m
Fixed-Size Data-path: Implementation

Signal Truncation
• Keep lower order m-bits, ignore higher bits
• f % 2m ≡ g % 2m

Fractional Arithmetic with rounding
• Keep higher order m-bits, round lower order bits
• f - f %2m ≡ g - g%2m
2m
2m

Saturation Arithmetic
• Saturate at overflow
• Used in image-processing applications
Example: Anti-Aliasing Function

F=
1
= 1 =
2√a2 + b2 2√x
[Peymandoust et al, TCAD‘03]

coefficients
a
b
Expand into Taylor series
• F ≈ 1 x6 – 9 x5 + 115 x4
64
32
64
– 75 x3 + 279 x2 – 81 x
16
64
32
+ 85
64

coefficients
Scale coefficients; Implement
as bit-vectors
x = a 2 + b2
x
MAC
DFF
F
Example: Anti-Aliasing Function

F1[15:0], F2[15:0], x[15:0]

F1 = 156x6 + 62724x5 + 17968x4 + 18661x3 + 43593 x2
+ 40244x +13281

F2 = 156x6 + 5380x5 + 1584x4 + 10469x3 + 27209 x2 + 7456x
+ 13281



F1 ≠ F2 ; F1[15:0] = F2[15:0]
Transform the problem
• F1 - F2 = 57344x5 + 16384x4 + 8192x3 + 16384x2 + 32768x
≡ 0 % 216
F1 - F2 : Vanishing polynomial
Previous Work: Function Representations

Boolean Representations (f: B → B)
• BDDs, MTBDDs, ADDs etc.

Moment Diagrams (f: B → Z)
• BMDs, K*BMDs, HDDs etc.

Canonical DAGs for Polynomials (f: Z → Z)
• Taylor Expansion Diagrams (TEDs)

Required: Representation for f: Z2m → Z2m
Previous Work: Others

SAT and MILP-based techniques
• Suitable for linear/multi-linear forms

Word-level ATPG, congruence closure based techniques,
co-operative decision procedures
• Solve linear congruences under modulo arithmetic

Theorem-Proving (HOL), term-rewriting
• Works when datapath size can be abstracted using
data dependence, symmetry, and other abstractions
• Here, datapath size (m) defines ring cardinality (Z2m)
Previous Work: Symbolic Algebra

MODDs: Based on finite fields [Pradhan et al, DATE ‘04]
• Literal based decomposition

Symbolic Algebra Tools: Singular, Macaulay, Maple,
Mathematica, Zen, etc.
• Polynomial equivalence over R, Q, C, Zp
• Unique Factorization Domains (UFDs) : Uniquely
factorize into irreducibles
• Match corresponding coefficients to prove
equivalence
Why is the Problem Difficult?

Z2m is a non-UFD
• f = x2 + x in Z6 can be factorized as
f
x
f
x+1
x+3
x+4
 Atypical approach required to prove equivalence
Proposed Solution

Equivalence can be proved by
• f (x) - g(x) ≡ 0 % 2m: Zero Equivalence

Exploit Vanishing polynomials

An instance of Ideal Membership Testing

Proposed solution based on:
• Niven & Warren’s work [Proc. Amer. Math.Soc, 1957]
• Singmaster’s work [J. Num. Th, 1974]
Ideal Membership Testing
h: % 2m
Ideal
x
x % 2m
0
f
g
P

f–g?
h:P →Q defined by % 2m
• x in P maps to x %2m in Q
• Ideal members map to 0

Derive Ideal of Vanishing Polynomials in Z2m

Grobner's basis? Buchberger's algorithm?

Known for UFDs, but for Z2m ?
Q
Ideal Membership Testing in Zp

Fermat’s Little Theorem:
• x p ≡ x (mod p) or
• x p – x ≡ 0 (mod p)
• x p –x generates the vanishing ideal in Zp[x]

f(x) = 0 % p iff f(x) = (xp-x)g(x)

Zp: Principal Ideal Domain

This does not follow in Z2m
Ideal Membership Testing
h: % 2m
Ideal
x
x % 2m
0
f
g
P

f–g?
Q
Generate the ideal of vanishing polynomials % 2m ?
• Vanishing Ideal is finitely generated
[Niven et al, Am. Math. Soc., ‘57]

Need an algorithm for membership testing
• Representative expression for members of this ideal
[Singmaster, J. Num. Th ‘74]
Results From Number Theory

n! divides a product of n consecutive numbers.
• 4! divides 99 X 100 X 101 X 102

Find least n such that 2m|n!
• Smarandache Function (SF).
• SF(23) = 4, since 23|4!

2m divides the product of n = SF(2m) consecutive
numbers
Results From Number Theory

f ≡ g in Z23 or (f - g) ≡ 0 % 23
• 23|(f - g) in Z23
• 23|4!
• 4! divides the product of 4 consecutive numbers
Write (f-g) as a product of SF(23) = 4 consecutive
numbers
 A polynomial as a product of 4 consecutive numbers?
• (x+1)
Results From Number Theory

f ≡ g in Z23 or (f - g) ≡ 0 % 23
• 23|(f - g) in Z23
• 23|4!
• 4! divides the product of 4 consecutive numbers
Write (f-g) as a product of SF(23) = 4 consecutive
numbers
 A polynomial as a product of 4 consecutive numbers?
• (x+1)(x+2)
Results From Number Theory

f ≡ g in Z23 or (f - g) ≡ 0 % 23
• 23|(f - g) in Z23
• 23|4!
• 4! divides the product of 4 consecutive numbers
Write (f-g) as a product of SF(23) = 4 consecutive
numbers
 A polynomial as a product of 4 consecutive numbers?
• (x+1)(x+2)(x+3)
Results From Number Theory

f ≡ g in Z23 or (f - g) ≡ 0 % 23
• 23|(f - g) in Z23
• 23|4!
• 4! divides the product of 4 consecutive numbers
Write (f-g) as a product of SF(23) = 4 consecutive
numbers
 A polynomial as a product of 4 consecutive numbers?
• (x+1)(x+2)(x+3)(x+4)
Basis for factorization

S0(x) = 1

S1(x) = (x + 1)

S2(x) = (x + 1)(x + 2)

S3(x) = (x + 1)(x + 2)(x + 3) = Product of 3 consecutive numbers

…

…

Sn(x) = (x + n) Sn-1(x)
= Product of 2 consecutive numbers
= Product of n consecutive numbers
Rule 1: Factorize into atleast Sn(x) to vanish, where n = SF(2m).
Example 1: Vanishing polynomial

4th degree polynomial p in Z23 ; SF(23) = 4

p = x4 +2x3 + 3x2 + 2x

p can be written as a product of 4 consecutive numbers.
• or p = (x+1)(x+2)(x+3)(x+4) = S4(x) in Z23.

p is a vanishing polynomial.
Example 2: Vanishing polynomial
module fixed_bit_width (x, f, g);
input [2:0] x;
output [2:0] f, g;
assign f[2:0] = x2 + 6x – 3;
assign g[2:0] = 5x2 + 2x + 5;
 h(x) = f(x) – g(x) = 4x2 + 4x
 h(x) ≡ 0 for all values of x in {0,…,7}
 4x2+4x not equal to (x+1)(x+2)(x+3)(x+4)
 Required: To show that h(x) is a vanishing polynomial
in Z23
Constraints on the Coefficient

h(x) = 4x2 + 4x = 4(x+1)(x+2)

In Z23 , SF(23) = 4. Product of 4 consecutive numbers:
• S4(x) = (x+1) (x+2) (x+3) (x+4)
Rule 2: Coefficient has to be a multiple of bk = 2m/gcd(k!, 2m)
 Here, Coefficient of h(x) = 4, Degree of h(x) = 2
 b2 = 23/gcd(2!, 23) = 4 is a multiple of the coefficient
Constraints on the Coefficient

h(x) = 4x2 + 4x = 4(x+1)(x+2)
compensated by constant

In Z23 , SF(23) = 4. Product of 4 consecutive numbers:
• S4(x) = (x+1) (x+2) (x+3) (x+4)
missing factors
Rule 2: Coefficient has to be a multiple of bk = 2m/gcd(k!, 2m)
 Here, Coefficient of h(x) = 4, Degree of h(x) = k = 2
 b2 = 23/gcd(2!, 23) = 4 is a multiple of the coefficient
Deciding Vanishing Polynomials

Polynomial F in Z2m vanishes if
F = FnSn + Σ n-1ak bk Sk
k=0
Rule 1
Rule 2

n = SF(2m), i.e. the least n such that 2m|n!

Fn is an arbitrary polynomial in Z2m[x]

ak is an arbitrary integer

bk = 2m/gcd(k!,2m)
Algorithm
F = FnSn + Σ n-1ak bk Sk
Input: poly, 2m
1.
2.
Calculate n = SF(2m)
k = n: Reduce according
to Rule 1
• Divide by Sn
• If remainder is zero,
F = FnSn, else
Continue
k=0
Example 1
poly = 4x2 + 4x in Z23
1.
2.
n = SF(23) = 4
k = 4: Divide by S4
• Degree (poly) = 2
< degree(S4) = 4
•
•
quo = 0, rem = 4x2 + 4x
F4 = 0; Continue
Algorithm
F = FnSn + Σ n-1ak bk Sk
Input: poly, 2m
1.
2.
Calculate n = SF(2m)
k = n: Reduce according
to Rule 1
• Divide by Sn
• If remainder is zero,
F = FnSn, else
Continue
k=0
Example 1
poly = 4x2 + 4x in Z23
1.
2.
n = SF(23) = 4
k = 4: Divide by S4
• Degree (poly) = 2
< degree(S4) = 4
•
•
quo = 0, rem = 4x2 + 4x
F4 = 0; Continue
Algorithm
3.
F = FnSn + Σ n-1ak bk Sk
Reduce according to
Rule 2. Divide by Sn-1 to
S0
• Check if quotient is a
multiple of
bk = 2m/gcd(k!,2m)
• If remainder is zero,
stop. Else, continue
k=0
3.
4.
Example 1
k = 3: Divide by S3
• degree (poly) = 2 <
degree(S3) = 3
• quo= 0, rem = 4x2 + 4x
continue
k = 2: Divide by S2
• quo = 4; rem = 0
• b2 = 23/gcd(2!,23) = 4
• a2 = quo/ b2 = 1 Є Z
poly = a2.b2.S2 = 1.4.(x+1)(x+2) ≡ 0 in Z23
Algorithm
3.
F = FnSn + Σ n-1ak bk Sk
Reduce according to
Rule 2. Divide by Sn-1 to
S0
• Check if quotient is a
multiple of
bk = 2m/gcd(k!,2m)
• If remainder is zero,
stop. Else, continue
k=0
3.
4.
Example 1
k = 3: Divide by S3
• degree (poly) = 2 <
degree(S3) = 3
• quo= 0, rem = 4x2 + 4x
continue
k = 2: Divide by S2
• quo = 4; rem = 0
• b2 = 23/gcd(2!,23) = 4
• a2 = quo/ b2 = 1 Є Z
poly = a2.b2.S2 = 1.4.(x+1)(x+2) ≡ 0 in Z23
Example 2






poly = 5x2 + 3x + 7 in Z23
n = SF(23) = 4
degree (poly) = 2 < n. Skip Rule 1 and goto Rule 2
Divide by S2
• quo = 5; rem = 5 + 4x
• b2 = 23/gcd(2!,23) = 4
• a2 = quo/ b2 is not in Z
poly does not satisfy Rule 2
poly is not a vanishing polynomial in Z23
Experimental Setup

Distinct RTL designs are input to GAUT [U. de LESTER, 2004]

Extract data-flow graphs for RTL designs

Construct the corresponding polynomial representations (f, g)
• Extract bit-vector size

Find the difference (f-g) and invoke the algorithm

Algorithm implemented in MAPLE

Compare with BMD, SAT and MILP

Complexity: O(n+1), n = SF(Z2m)
A
H
F
or unc
n
t
H er ion
or Po
n
H er ly 1
or P
ne oly
r
Po Po 2
ly ly
Un 3
op
t
co .
s
co x
t-1
x
l
Va n( er
ni 1+ f x
sh x/
in 1-x
g
Po )
ly
.
s
Al
ia
nt
i-
Results
1000
100
10
1
Our Approach (< 10 s)
BMD
SAT-Zchaff
Applications to Synthesis
 Datapath size (m): 8 bits
 SF(28) = 10
 Polynomial can be
factorized into S10(x)
Conclusions

Technique to verify equivalence of univariate polynomial
RTL computations

Fixed-size bit-vector arithmetic is polynomial algebra over
finite integer rings

f(x) % 2m ≡ g(x) % 2m is transformed into f(x) - g(x) ≡ 0 % 2m

Efficient algorithm to determine vanishing polynomials
Future Work

Future Work involves extensions for • Multivariate datapaths with fixed bit-widths
[To Appear, ICCAD ‘05]
• Multiple Word-length Implementations
[In Review, DATE ‘06]

Verification of Rounding and Saturation Arithmetic

Formal Error Analysis

Applications to Synthesis –
• Need cost models for low power, area, delay
Questions?