Formal verification of arithmetic datapaths using algebraic geometry and symbolic computation
Priyank Kalla · 2015
Algebraic geometry is the study of the geometry of solutions to a system of multivariate polynomial equations. Modern algebraic geometry does not explicitly solve the system of equations to enumerate the solutions, but rather reasons about the presence, absence, dimensions or intersection properties of the solution-sets, etc. Abstract and computational algebra is often used for this purpose - particularly the theory and technology of Grobner bases, which provides a very powerful set of tools to solve many polynomial decision problems. In this talk, I will present a tutorial on how some of these techniques from algebraic geometry and commutative algebra can be used for formal verification of RTL datapaths and arithmetic circuits. Datapath designs implement arithmetic computations over finite word-length operands, say, over k-bit vectors. These circuits implement functions that are mappings over k-dimensional Boolean spaces f : Bk → Bk. Such functions can also be construed as mappings over: i) finite integer rings of the type Z2k≡ Z (mod 2k), i.e. as functions f : Z2k→ Z2k; or ii) as functions over the Galois field of 2k elements, i.e. f : F2k→ F2k. The designs can then be modeled as a system of polynomial functions over Z2kor F2k, and Grobner basis techniques can be applied for verification by reasoning about the solutions (functions) of the polynomial systems (circuits). Given the arithmetic nature of the designs, such an approach provides a natural word-level abstraction which can enable efficient verification. While Grobner basis techniques are very powerful, the computation suffers from high complexity. Therefore, the main focus of the tutorial will be on how to overcome this complexity. I will describe: . How to formulate various verification problems using ideal membership, Nullstellensatz, elimination theory and Grobner bases; . How to exploit the number-theoretic properties of finite rings and fields to simplify the problems; . How to analyze the structure/topology of the given circuits to get more theoretical insights into the corresponding polynomial ideals, and use this information to improve the computation; and . How to implement the aforementioned concepts using modern symbolic computation algorithms, e.g. Faugere's F4-style reductions, for practical datapath verification. Arithmetic datapaths are usually custom designed, and they often exhibit some structure or symmetry in the implementations. Grobner bases can help identify this inherent symmetry. By exploiting this information, efficient symbolic computation algorithms can then be devised for scalable verification. The verification context will be motivated by applications such as elliptic curve cryptography, error correcting circuits, polynomial signal processing, word-level RTL synthesis, etc. I will provide information on various resources - publications, design benchmarks and the verification tools developed by us - so that interested participants can explore this exciting area of work. I will conclude by describing important unsolved problems in this specific area, and the challenges that need to be overcome to fully exploit the potential of the theory and technology.