Approximate hardware generation using symbolic computer algebra employing grobner basis

Author(s):  
Saman Froehlich ◽  
Daniel Grose ◽  
Rolf Drechsler
2019 ◽  
Vol 56 (1-3) ◽  
pp. 22-54 ◽  
Author(s):  
Daniela Kaufmann ◽  
Armin Biere ◽  
Manuel Kauers

AbstractVerifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most effective approach uses polynomial reasoning over pseudo boolean polynomials. In this approach a word-level specification is reduced by a Gröbner basis which is implied by the gate-level representation of the circuit. This reduction returns zero if and only if the circuit is correct. We give a rigorous formalization of this approach including soundness and completeness arguments. Furthermore we present a novel incremental column-wise technique to verify gate-level multipliers. This approach is further improved by extracting full- and half-adder constraints in the circuit which allows to rewrite and reduce the Gröbner basis. We also present a new technical theorem which allows to rewrite local parts of the Gröbner basis. Optimizing the Gröbner basis reduces computation time substantially. In addition we extend these algebraic techniques to verify the equivalence of bit-level multipliers without using a word-level specification. Our experiments show that regular multipliers can be verified efficiently by using off-the-shelf computer algebra tools, while more complex and optimized multipliers require more sophisticated techniques. We discuss in detail our complete verification approach including all optimizations.


1997 ◽  
Vol 9 (5) ◽  
pp. 324-331
Author(s):  
Toshimi Shimizu ◽  
◽  
Haruhisa Kawasaki

This paper presents a new method for solving the inverse kinematics of robot manipulators symbolically using computer algebra. The kinematics equations, including the trigonometric functions of joint displacements, are expressed as multivariate polynomial equations by transforming these functions into variables. The multivariate polynomial equations can be solved by evaluating their reduced Grobner basis. The properties for efficient evaluation of the reduced Grobner basis and the inverse kinematics of a robot, whose last three joint axes intersect at a point, are shown. This procedure is implemented using Maple V and built into ROSAM (Robot Symbolic Analysis, by Maple) that is a robot analysis library made by our group. An analysis example of a structurechanged PUMA type robot is given.


2019 ◽  
Vol 13 (3-4) ◽  
pp. 229-237
Author(s):  
Stavros Kousidis ◽  
Andreas Wiemers

Abstract We improve on the first fall degree bound of polynomial systems that arise from a Weil descent along Semaev’s summation polynomials relevant to the solution of the Elliptic Curve Discrete Logarithm Problem via Gröbner basis algorithms.


2012 ◽  
Vol 47 (8) ◽  
pp. 926-941 ◽  
Author(s):  
Martin R. Albrecht ◽  
Carlos Cid ◽  
Jean-Charles Faugère ◽  
Ludovic Perret
Keyword(s):  

Author(s):  
HERVÉ PERDRY ◽  
PETER SCHUSTER

We give a constructive proof showing that every finitely generated polynomial ideal has a Gröbner basis, provided the ring of coefficients is Noetherian in the sense of Richman and Seidenberg. That is, we give a constructive termination proof for a variant of the well-known algorithm for computing the Gröbner basis. In combination with a purely order-theoretic result we have proved in a separate paper, this yields a unified constructive proof of the Hilbert basis theorem for all Noether classes: if a ring belongs to a Noether class, then so does the polynomial ring. Our proof can be seen as a constructive reworking of one of the classical proofs, in the spirit of the partial realisation of Hilbert's programme in algebra put forward by Coquand and Lombardi. The rings under consideration need not be commutative, but are assumed to be coherent and strongly discrete: that is, they admit a membership test for every finitely generated ideal. As a complement to the proof, we provide a prime decomposition for commutative rings possessing the finite-depth property.


Sign in / Sign up

Export Citation Format

Share Document