The PolyBoRi Framework

Fraunhofer ITWM

The PolyBoRi Framework

PolyBoRi is a performant reference implementation of a computer algebra system for Boolean polynomials. We can use it to model digital components algebraically and to proof the validity of poly­nomially specified conditions.

 

 

PolyBoRi owns a graphical user Interface for algebraically analyzing Boolean polynomial systems without previous knowledge. Users and developers can easily customize and extend this for handling specific tasks.

 

Application and Interface

PolyBoRi helps to validate fixed-size arithmetic instructions of microcontrollers, microprocessors and digital signal processors, that are out of the scope of classical verification. It allows for

  • Setting up and reducing bit-level equations
  • Treating large scale multiplier and adder blocks
  • Importing GAT, CNF and RTP files
  • Exporting optimized CNF files

Software

PolyBoRi is a dedicated open source software for analyzing Boolean polynomial systems arising from application areas like embedded and digital systems.
It features high-performance algebraic core routines together with an extensible and powerful modeling language.

Further information

Type of Project:

Open Source Development

Related projects:

  • »Computer Algebra for validating a digital World«
  • »VerSys«
  • »Polynomials over Boolean Rings«
  • SourceForge Homepage