Transcript F(x) - Department of Computer Science

SIMULATION BOUNDS FOR EQUIVALENCE VERIFICATION OF
ARITHMETIC DATAPATHS WITH FINITE WORD-LENGTH
OPERANDS
Namrata Shekhar1, Priyank Kalla1, M. Brandon Meredith2, Florian Enescu2
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
Problem Overview
Application: Arithmetic datapaths in DSP designs
Problem modeling
Polynomial functions over finite integer rings
Limitations of previous work
Theory and Applications
Results and Conclusions
Future work
The Equivalence Verification Problem
Fixed Bit-width Operands
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
General Datapath Model
Bit-vector operands with different word-lengths
20-bit
8-bit
32-bit
*
*
12-bit
Input variables : {x1,…, xd} Output variables : f
Input bit-widths: {n1,…, nd} Output width
:m
.x1 {0, ..., 2n -1},
.x1  Z 2 ,x2  Z 2
1
n1
n2
f {0, ..., 2m -1}
f  Z2
m
Model f as polynomial function
Z2n1 × Z2n2 ×
× Z2nd  Z2m
Arithmetic Data-path: Implementation
Signal Truncation
Keep lower-order bits, ignore higher bits
.f (x1 ,..,xd ) % 2m  g (x1 ,..,xd ) % 2m
Fractional Arithmetic with rounding
Keep higher-order m-bits, round lower order bits
m
m
f
f
%
2
g
g
%
2
.

m
2
2m
Saturation Arithmetic
Saturate at overflow
Used in image-processing applications
Motivation: Convolution of A and B
3
C = (c0, c1, c2, c3) where ci   a jbi  j
j 0
0i 3
C′ = (c′0, c′1, c′2, c′3) = DFT-1 (DFT(A)·DFT(B))
a0
a1
a2
a3
FFT(A)
FAB0
FAB2
b0
b1
b2
b3
c’0
FAB1
FAB3
invFFT(FAB)
c’1
c’2
c’3
FFT(B)
Datapath size is fixed
How many simulation vectors required to prove C = C’ ?
Example: Anti-Aliasing Function
F=
1
= 1 =
2√a2 + b2 2√x
[Peymandoust et al, TCAD‘03]
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
coefficients
a
b
x = a2 + b2
x
MAC
Scale coefficients;
Implement as bit-vectors
DFF
F
Example: Anti-Aliasing Function
Implemented as a fixed size datapath in x
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]
How many vectors required to prove: F1 % 216 ≡ F2 % 216
Contributions
Abstract the design as a polynomial function
Exhaustive simulation is not necessary to prove
equivalence
Upper bound on the number of vectors
To prove equivalence
Sufficient to catch errors
Bound corresponds to a function in number theory
Previous Work
Bit/Word level canonical diagrams
BDDs, ZBDDs, BMDs, TEDs
SAT and MILP-based techniques
Bit-vector decision procedures, Word-level ATPG, SMT
Theorem-Proving, term-rewriting
Problem model is algebraic
Previous Work: Simulation
Reduction in simulation complexity
Three-valued logic simulation [Bryant, ACM ’91]
Utilizing structural information [Brand, ICCAD ’92]
Automated approach using BDDs [Yuan , ICCAD ‘99]
Polynomial methods using the fundamental theorem of
algebra
Generate simulation vectors [Sanchez, HLDVT ‘99]
Reduce the complexity of model checking
[ Raudvere, ICCAD ‘05]
Fundamental Theorem of Algebra
A degree-k polynomial F(x) has exactly k roots
F(x) = x2 + 6x = x ( x + 6 )
If F(x) = 0 for k + 1 values, then F(x) is a zero polynomial
Can also be extended for multi-variate polynomials
Limitations:
Results applicable only over unique factorization domains
(UFD): Z, Zp, C
Z2m is a non-UFD
Why is the Problem Difficult?
Consider F(x) = x2 + 6x in Z8
F
x
F
x+6
x+4
x+2
Degree-2 polynomial has 4 unique roots
F(x) = 0 for 4 vectors, but F(x) ≠ 0 in Z8
Not applicable to bit-vector arithmetic
Previous Work: Finite Ring Algebra
f (x1, …, xd) % n ≡ g(x1, …, xd) % n
Proving equivalence is NP-hard [Ibarra et al, ACM ‘83]
Previous approaches
f (x1, x2, …, xd) – g (x1, x2, …, xd) ≡ 0 % 2m : Zero Equivalence
[ICCD ’05]
Reduction to canonical forms [ICCAD ’05]
Limitations:
Intermediate expression swell
No error trace is provided
Simulation vector generation: Based on zero equivalence
Zero Equivalence
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}: Vanishing polynomial
Required: To find if any given expression vanishes
Use concepts from ideal membership testing
Ideal Membership Testing
h: % 2m
Ideal
xi
xi % 2m
0
f
Z2m[x]
g
f–g?
Z2m
h:Z2m[x] → Z2m defined by % 2m
Ideal members map to 0
Test for membership in Ideal of Vanishing Polynomials
Representative expression for members of this ideal [Chen,
Disc. Math ‘96]
Use concepts from Number theory and polynomial algebra
Results From Number Theory
Find least n such that 2m|n!
Smarandache Function: λ = SF (2m)
λ = SF(23) = 4, since 23|4!
n! divides a product of n consecutive numbers
4! divides 99 X 100 X 101 X 102
2m divides the product of n consecutive numbers
23 divides the product of 4 consecutive numbers
Results From Number Theory
F ≡ G in Z23 or (F - G) ≡ 0 % 23
23|(F - G) in Z23
23 divides the product of 4 consecutive numbers
If (F-G) is a product of 4 consecutive numbers then
23|(F - G)
A polynomial as a product of 4 consecutive numbers?
.(x) (x-1) (x-2) (x-3)
Basis for Factorization
Y0(x) = 1
Y1(x) = (x)
Y2(x) = (x)(x - 1)
= Product of 2 consecutive numbers
Y3(x) = (x)(x - 1)(x - 2)
= Product of 3 consecutive numbers
…
…
Yk(x) = (x – k + 1) Yk-1(x) = Product of k consecutive numbers
Rule 1: Factorize into at least Yλ (x) to vanish, where
λ = SF(2m)
Example 1: Vanishing Polynomial
4th degree polynomial F over Z23
λ=4
.F
 x 4  2x3  3x 2  2x
Degree (x) = k = 4 = λ
F can be written as a product of 4 consecutive numbers
in x
3
.F = (x) (x-1) (x-2) (x-3) = Y4 (x) % 2
F is a vanishing polynomial
Constraints on the Coefficient
F(x) = 4x2 + 4x = 4 (x)(x-1) % 23
compensated by constant
Y4(x) = (x)(x-1) (x-2)(x-3)
missing factor
Rule 2: Coefficient has to be a multiple of bk = 2m/gcd(k!, 2m)
Here, Coefficient of F(x) = 4, Degree of F(x) = 2
b2 = 23/gcd(2!, 23) = 4 is a multiple of the coefficient
Use Rule 1 and Rule 2 to determine if any F(x) = 0 % 2m
Deciding Vanishing Polynomials
Polynomial F in Z mvanishes if
2
F = F Y + k a k bk Yk
Rule 1
Rule 2
Fλ is an arbitrary polynomial over Z m
2
Yλ = Yk is as defined earlier: λ = SF(2m)
ak is an arbitrary integer
2m
.b k =
gcd(k!,2 m )
Polynomial Representations
Newton’s interpolation formula: Any polynomial F(x) can
be written as
 x
F( x)   ( F)(0)  
k 0
k 
p
k
(F)( x)  F( x  1)  F( x) : Forward difference operator
p is the degree of F(x)
Polynomial Representations
Newton’s interpolation formula: Any polynomial F(x) can
be written as
 x
F( x)   ( F)(0)  
k 0
k 
p
k
(F)( x)  F( x  1)  F( x) : Forward difference operator
p is the degree of F(x)
Reinterpret Vanishing ideal
Newton’s interpolation formula: Any polynomial F(x) can
be written as
(  k F)(0)
F( x)  
Yk ( x)
k!
k 0
p
(F)( x)  F( x  1)  F( x) : Forward difference operator
Yk(x) is as defined earlier
p is the degree of F(x)
Reinterpret Vanishing ideal
Newton’s interpolation formula: Any polynomial F(x) can
be written as
(  k F)(0)
F( x)  
Yk ( x )
k!
k 0
p
(F)( x)  F( x  1)  F( x) : Forward difference operator
Yk(x) is as defined earlier
p is the degree of F(x)
Polynomial Representations
Newton’s interpolation formula: Any polynomial F(x) can
be written as
p
F( x)   ckYk (x)
k 0
(  k F)(0)
ck 
is any arbitrary integer
k!
Yk(x) is as defined earlier
p is the degree of F(x)
Polynomial Representations
Any polynomial F(x) in Z m can be written as
2
F(x) = F0 Y + k ck Yk 0  k  
Rule 1
Fλ is an arbitrary polynomial over Z m
2
Yλ = Yk is as defined earlier: λ = SF(2m)
(  k F)(0) is an arbitrary integer
ck 
k!
Polynomial Representations
Any polynomial F(x) in Z mcan now be reduced to
2
F = k ck Yk
0k 
Fλ is an arbitrary polynomial over Z2m
Yλ = Yk is as defined earlier: λ = SF(2m)
(  k F)(0) is an arbitrary integer
ck 
k!
Polynomial Representations
Any polynomial F(x) in Z mcan now be reduced to
2
F = k ck Yk
0k 
Apply Rule 2
m
2
F(x) vanishes iff ck is a multiple of b k =
gcd(k!,2m )
Check for all ck, where 0  k  
ck evaluated no more than λ times
F(x) evaluated no more than λ times
Results
By extension,
If F(x) ≡ 0 for any λ consecutive values of x in Z
.F( x)  0 x  Z2m
2m
Further,
F(x) – G(x) = 0 → F(x) = G(x)
Any λ consecutive values of x are sufficient to prove
equivalence
Example
Consider f, g over Z23
λ = SF(23) = 4
f = x4 + x2
Simulating,
x=0, f=0
g = 2x2
Simulating,
x=0, g=0
x=1, f=2
x=1, g=2
x=2, f=4
x=2, g=0
x=3, f=2
x=3, g=2
x=4, f=0
x=4, g=0
x=5, f=2
x=5, g=2
x=6, f=4
x=6, g=0
x=7, f=2
x=7, g=2
Extension to Multiple Variables
Given d variables x = <x1, …, xd> with degrees
k = < k1, …, kd> over Z2m
Basis for d variables:
d
.Yk =  Yi ( xi )  Y0 ( x0 )  Y1 ( x1 )
Yd ( xd )
i=1
Rule 1 (for d variables): Factorize into Yλ (x), such that
ki ≥ λ for any xi ; λ = SF(2m)
Example: Vanishing Polynomial
4th degree polynomial F(x, y) over Z23
SF(23) = 4
F.  x 4 y  2x 3 y  3x 2 y  2xy
Degree (x) = k1 = 4 = SF(23)
Degree (y) = k2 = 1
F can be written as a product of 4 consecutive numbers
in x
.F = (x) (x-1) (x-2) (x-3) y = Y4 (x)  Y1 (y) % 23
F is a vanishing polynomial
Effect of Bit-vectors
4th degree polynomial F(x, y) in Z21 × Z22 → Z23
λ=4
.F = x 2
y - x y = x (x-1) (y)
x  Z 2 ,x  0,1
y  Z 2 , y  0,1,2,3
Define
i
1
2
i  min{2n , }
Rule 1(extended): Factorize into Yk(x), such that ki ≥ μi for
any xi
.1  min{21 ,SF(23 )}  2; 2  min{22 ,SF(23 )}  4
F = Y2(x) · Y1(y) ≡ 0 % 23
Results
By extension, for F(x) over
× Z2nd  Z2m
Z2n1 ×
If F(x) ≡ 0 for any μi consecutive values of xi in
.F( x )  0 x i  Z2n
Z 2n
i
i
Total number of vectors:
d

i 1
i
Further,
Z2n1 × × Z2nd  Z2m
  vectors
F(x) – G(x) = 0 → F(x) = G(x) over
d
To prove equivalence, we need
i 1
i
Example
Consider f, g over Z22 × Z2 → Z23
λ = 4, μ1 = 4 ; μ2 = 2
Required: μ1.μ2 = 8 vectors
f = x4y+ x2y
g = 2x2y
Simulating,
Simulating,
x=0, y=0, f=0
x=0, y=0, g=0
x=1, y=0, f=0
x=1, y=0, g=0
x=2, y=0, f=0
x=2, y=0, g=0
x=3, y=0, f=0
x=3, y=0, g=0
x=0, y=1, f=0
x=0, y=1, g=0
x=1, y=1, f=2
x=1, y=1, g=2
x=2, y=1, f=4
x=2, y=1, g=0
x=3, y=1, f=2
x=3, y=1, g=2
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 sizes for inputs and outputs
Determine the maximum number of simulation vectors required
Check for equivalence or determine bugs
Simulation Results for Equivalent Designs
1.00E+70
1.00E+65
1.00E+60
1.00E+55
1.00E+50
1.00E+45
1.00E+40
1.00E+35
1.00E+30
1.00E+25
1.00E+20
1.00E+15
1.00E+10
1.00E+05
1.00E+00
IRR
PSK
Degree-4 Degree-4 Savitzky- 4th order MIBENCH
Filter 1
Filter 2
Golay
IIR
Filter
Total Test Vectors
Required Test Vectors
Simulation Results for Buggy Designs
1000
100
10
1
Anti-alias Function
PSK
Our approach
4th Order IIR
Random Simulation
Vanishing
Polynomial
Limitations
a[7:0]
b[7:0]
c[7:0]
a[7:0]
b[7:0]
+
c[7:0]
+
≠
t1[7:0]
a = 127
b=1
c = 255
t2[7:0]
+
+
f1[8:0]
f2[8:0]
f1 = 383
a = 127
b=1
c = 255
f2 = 127
Conclusions
Technique to verify equivalence of polynomial RTL
computations
Bit-vector arithmetic is polynomial algebra over the system
of finite integer rings Z n × Z n ×
21
22
× Z2nd  Z2m
Exhaustive simulation is not necessary to prove
f ( x1 , x2 ,
, xd ) % 2m = g ( x1 , x2 ,
, xd ) % 2m
Results based on concepts from number theory and
polynomial algebra
Questions ?
Polynomial Abstraction
If (x > 2b’10)
then y = x * x * x
Else y = x*x
Traditional modeling
x.  [0,2]  y = x 3 and x = 3  y = x 2
Proposed modeling: y as a polyfunction from Z 4  Z 32
y  3x 3  8x 2  22x : Unique representation
Issues with the proposed abstraction:
Scalability