Algebraic verification method for SEREs properties via Groebner bases approaches (Q2375464)

Summary: This work presents an efficient solution using a computer algebra system to perform linear temporal properties verification for synchronous digital systems. The method is essentially based on both the Groebner bases approaches and symbolic simulation. A mechanism for constructing canonical polynomial set based symbolic representations for both circuit descriptions and assertions is studied. We then present a complete checking algorithm framework based on these algebraic representations using Groebner bases. The computational experience result in this work shows that the algebraic approach is a quite competitive checking method and will be a useful supplement to the existent verification methods based on simulation.