Algebraic Verification

Verifying the correctness of digital system designs requires high quality that can only be achieved with formal methods. Satisfiability solving (SAT) has moved mainstream in design flows, but it may fail for modern digital circuits topologies.

To close this design gap we take profit from the binary nature of digital system specifications by modeling Boolean expressions as polynomials. This step opens up the whole world of computer algebra and Gröbner bases. While these concepts were known much longer, their current practical importance is a result of dramatical improvements in performance and algorithms in ­recent years.

The concept of Boolean polynomials combines polynomial flexibility with the effectivity of decision diagrams from classical formal verification. It applies to propositional logic problems originating from:

• satisfiability analysis
• property checking of digital systems
• equivalence checking in safety-critical environment
• verified rapid prototyping
• cryptoanalysis

Services

Fraunhofer ITWM is co-developing PolyBoRi and supports ­integrating it into industrial frameworks. We offer the following services for validating digital systems:

• Consulting on digital verification
• Algebraic modeling of digital components
• Integrating algebraic techniques in design flows
• Implementing custom input and output filters
• Developing tailor-made verification solutions
• Setting up user interfaces