Transcript Slide 1

Equivalence Verification of Polynomial
Datapaths with Fixed-Size Bit-Vectors using
Finite Ring Algebra
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
 Problem Modeling
• Polynomial Functions over Finite Integer Rings
 Limitations of Previous Work
 Approach and Contributions
• Canonical form for Polynomials over Finite Rings
 Algorithm Design and Experimental Verification Runs
 Results, Conclusions & Future Work
The Equivalence Verification Problem
Motivation
 Quadratic filter design for polynomial signal processing
 y = a0 . x12 + a1 . x1 + b0 . x02 + b1 . x0 + c . x0 . x1
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 % 2 m
 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
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
 Scale coefficients; Implement
as bit-vectors
x = a 2 + b2
x
MAC
DFF
F
Example 1: 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]
 To Prove: F1 % 216 ≡ F2 % 216
• F1 ≡ F2 in Z2m[x1, …, xd]
Previous Work: Function Representations
 Boolean Representations (f: B → B): BDDs, ZBDDs 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
 SAT, MILP, Word-level ATPG, …
 Theorem-Proving (HOL), term-rewriting
• Works when datapath size can be abstracted away
Previous Work: Symbolic Algebra
 Symbolic Algebra Tools: Singular, Macaulay, Maple,
Mathematica, Zen, Dagwood etc.
• Polynomial representations: Sparse, Dense, Recursive,
Straight-line programs, DAGs, etc.
• Polynomial equivalence over R, Q, C, Zp
• Unique Factorization Domains (UFDs) : Uniquely factorize
into irreducibles
• Match corresponding irreducibles to prove equivalence
Why is the Problem Difficult?
 Z2m is a non-UFD
• f = x2 + 6x in Z8 can be factorized as
f
x
f
x+6
x+4
x+2
 Atypical approach required to prove equivalence
Proposed Solution
 f (x1, …, xd) % n ≡ g(x1, …, xd) % n
• Proving equivalence is NP-hard
 Vanishing polynomials [ICCD ‘05]
• f(x) – g(x) ≡ 0 % 2m : Zero Equivalence
• An instance of Ideal Membership Testing
• Efficient solutions over fields (Groebner’s bases): Z2m[x1,…, xd] ?
 Canonical forms: Current focus
• Unique representations for polyfunctions over Z2m
• Equivalence by coefficient matching
• Concepts from Hungerbuhler et al. [To appear J. Sm. Not., ‘06 ]
Polyfunctions over Z2m
Equivalence
classes
F1
F2
f
G1
G2
g
Z2m[x1, …, xd]
Z2m
 Polynomials over Z2m[x1, …, xd]
• Represented by polyfunctions from Z2m[x1, …, xd] to Z2m
 F1 % 2m ≡ F2 % 2m => they have the same underlying polyfunction (f )
 Use equivalence classes of polynomials
• Derive representative for each class: Canonical form
Motivating our Approach
module fixed_bit_width (x, f, g);
input [2:0] x;
output [2:0] f, g;
assign f[2:0] = 5x2 + 6x - 3;
assign g[2:0] = x2 + 2x + 5;
 f (x) = 5x2 + 6x - 3 = (x2 + 2x + 5) + (4x2 + 4x)
• f (x) = g(x) + V (x) in Z23
 V (x) = 4x2 + 4x ≡ 0 % 23 ; for x in {0,…,7}
• f (x) = g (x) + 0 in Z23
 Required: To identify and eliminate such redundant
sub-expressions
(vanishing)
Vanishing polynomials: Requirement
Set of all
Vanishing
polynomials
h: % 2m
0
f
g
Z2m[x1, …, xd]
Z2 m
 Generate vanishing expressions V(x)
• Test if f (x) = g (x) + V(x)
• f (x) = f (x) – V(x)
 Challenge: Infinite number of vanishing polynomials
 Required: To generate V(x) specific to given f (x)
Vanishing Polynomials for Reducibility
 In Z23, say f (x) = 4x2
• f (x) = f (x) - V(x)
• Generate V(x) of degree 2
• V(x) = 4x2 + 4x ≡ 0 % 23
 Reduce by subtraction:
•
4x2
f (x)
– 4x2 + 4x V(x)
=
- 4x = - 4x % 8 = 4x
• 4x2 can be reduced to 4x
• Degree reduction
Coefficient Reduction: Example
 Degree is not always reducible
 In Z23, f (x) = 6x2
• a=6
• k=2
 Divide and subtract
• 6x2 = 2x2 + 4x2 % 23
• 4x2 can be reduced to 4x
 f (x) = 2x2 + 4x : Lower Coefficient
Our Approach
 Say f (x) = akxk + ak-1xk-1 + …+ a0
• In decreasing lexicographic order
 Required: f (x) in reduced, minimal, unique form
• Check if degree can be reduced
• Check if coefficient can be reduced
• Perform corresponding reductions
• Repeat for all monomials …
Degree Reduction: Requirement
 Generate appropriate vanishing polynomial , V(x)

f (x) = axk + a1xk-1 + …
V(x) = axk + a2xk-1 + …
f (x) – V(x) =
bxk-1 + …
 V(x): axk is the leading term
 Identify constraints on
• Degree : k
• Coefficient : a
 Use concepts from number theory
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) of 2m = n
• SF(23) = 4, since 23|4!
 2m divides the product of n = SF(2m) consecutive numbers
 Use SF(2m) to generate vanishing polynomial V(x)
Results From Number Theory
 V (x) ≡ 0 % 23
• 23| V (x) in Z23
• 23| 4! , since SF(23) = 4
• 4! divides the product of 4 consecutive numbers
Write V(x) 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) = 4! x + 4 ≡ 0 % 23
4
Constraints on the Coefficient
 In Z23 , SF(23) = 4. Product of 4 consecutive numbers:
• (x+1) (x+2) (x+3) (x+4)
missing factors
 V (x) = 4x2 + 4x = 4 (x+1)(x+2) ≡ 0 % 23
compensated by constant
 4(x+1)(x+2) = 4·2!· x + 2
2
 f (x) = axk + …
Rule 1: If 2m|ak!, then V(x) = ak! x + k ≡ 0 % 2m
k
= axk + a1xk-1…..
Example: Vanishing Polynomial
 Consider f (x) = 4x2 in Z23
• a=4
• k=2
• V (x) = ?
 Rule 1: 2m|a·k! => 23 | 4·2!
• V (x) = a·k! x + k = 4. 2! x + 2 = 4. 2! (x+2) (x+1)
k
2
2!
= 4x2 + 4x ≡ 0 % 23
• f (x) = 4x2
V(x) = - 4x2 + 4x
=
- 4x
=
- 4x % 8 = 4x
Coefficient Reduction: Requirement
 Define v2(k!) = {max x Є N: 2x| k!}
• number-of-factors-2 in k!
• v2(4!) = v2(4 * 3 * 2* 1) = 3
 Rule 1: 2m| a·k!
• Number-of-factors-2 in a·k! ≥ m or
• v2(a·k!) ≥ m
 If 2m does not divide a·k!
• v2(a·k!) < m
• v2(k!) < m and a < 2m- v2(k!)
Constraint
on degree
Constraint on
coefficient
Rule 2: Coefficient (a) has to be in the range {0, …, 2m- v2(k!)-1}
Notation: Multivariate Polynomials
 Given d variables x = <x1, …, xd>
with degrees k = <k1, …, kd>
 Replace in Rule 1 and Rule 2
• xk = ∏di=1 xiki
• k! = ∏di=1 ki!
• x = ∏di=1 xi
k
ki
• v2(k!) = ∏d v2(ki!)
 Use lexicographic term ordering for variables
Uniqueness

Theorem: Any polynomial F in Z2m can be uniquely
written as
F = Σ kЄNd αk xk
 d is the number of variables
 αk Є {0, …, 2m- v2(k!)-1} is the coefficient
 v2(k!) < m
Reduction Procedure
 Given a monomial f (x) = a·xk
 Degree reduction: Determine if 2m| a·k!
• If yes, generate V(x) of with a·xk as the leading term
• f (x) = f (x) – V(x)
 If 2m| a·k!, check if coefficient (a) is in {0, …, 2m- v2(k!)-1}
• If not, perform division according to
a·xk = q. 2m- v2(k!)·xk + r·xk
Degree reducible Reduced form
r < 2m- v2(k!)
Example: Reduction
Given poly = 6x2y + 4xy in Z23
1. Reducing 6x2y
2. Degree Reduction:
• a = 6;
• k! = kx!.ky! = 2!1! = 2
• 23 does not divide (a ·k! ) = 12;
•
Degree reduction not possible
•
Perform coefficient reduction
Example: Reduction
Given poly = 6x2y + 4xy in Z23
3. Coefficient Reduction:
•
•
•
v2(k!) = v2(2!·1!) = 1
Range = {0, …, 2m- v2(k!) – 1} = {0,…, 3}
a = 6 > 3; Can reduce coefficient
•
6x2y = 4x2y + 2x2y
•
Degree reduction for 4x2y:
 Rule 1: 23 | (4· 2! ·1!)
 4x2y – 4 . 2!·1! x + 2
2
4.
y + 1 = 4xy
1
poly = (4xy + 2x2y) + 4xy ≡ 2x2y in Z23
Experimental Setup
 Distinct RTL designs are input to GAUT [U. de LESTER, ‘04]
 Extract data-flow graphs for RTL designs
 Construct the corresponding polynomial representations (f, g)
• Extract bit-vector size
 Reduce f and g to canonical form
• Equivalence check by coefficient matching
 Algorithm implemented in MAPLE
• Complexity: O(kd); where k is the total degree and d is the
number of variables
 Compare with BDD, BMD and SAT
s
Al
ia
nt
i-
Fu PS
C nc K
u
t
Sa De bic ion
vi gre F
i
tz
y- e-4 lter
G
ol Fil
ay te
r
F
M i
H IB lter
or E
n N
H er CH
or Po
n
H er ly 1
or P
ne oly
r
Po Po 2
Va ly ly
ni
3
sh Un
in op
g t.
Po
ly
.
A
Results
1000
100
10
1
Our Approach (< 30 s)
BDD-VIS
BMD
SAT-Zchaff
Conclusions & Future Work
 Technique to verify equivalence of multivariate polynomial RTL
computations
 Fixed-size bit-vector arithmetic is polynomial algebra over the finite
integer ring, Z2m
 f (x1,…, xd) % 2m ≡ g (x1, …, xd) % 2m is proved by reduction to canonical
form
 Efficient algorithm to determine unique representations
 Future Work involves extensions for • Multiple Word-length Implementations [DATE ‘06]
• Verification of Rounding and Saturation Arithmetic
Questions?
A
Po
ly
ly
ly
.
Po
ly
.
3
2
1
io
n
Un
op
t
Po
Po
Po
in
g
ly
or
ne
r
or
ne
r
or
ne
r
Fu
nc
t
ni
sh
Va
H
H
H
s
Al
ia
nt
i-
Comparison
100
10
Our Approach (< 30 s)
Approach 2
1