Implementing bit-blasting for floating-point arithmetic in SMT

Question

I was wondering how people implement bit-blasting of floating-point arithmetic constructs in SMT solvers. Are there any existing libraries or facilities to do that (VHDL, ...), or are they implemented from scratch ? This represents how many lines of (C ? C++ ?) code ?

Thanks in advance.

Answer 1

There aren't "many" implementations in SMT solvers yet, but Z3 is one of those that implements everything. The code is in fpa2bv_converter.cpp and it's fairly self-explanatory. For large parts of the code I got inspiration from Mueller and Paul's "Computer Architecture" book, which features a chapter on floating-point circuits. The "Handbook of Floating-Point Arithmetic" (Muller at al.) also provides lots of information/programs/circuits.

Answer 2

To my knowledge the following implementation exist:

CBMC (not strictly and SMT solver but contains the necessary bits)

https://github.com/diffblue/cbmc/blob/master/src/solvers/floatbv/float_utils.cpp

Roughly 2KLoC in C++ (but built on top of utility functions for all of the bit-vector operations which is another 2KLoC). I believe it was originally written from Mueller and Paul's book. ESBMC contains a fork of an earlier version of this code.

Z3

See Christoph's answer above. There was an earlier prototype implementation in Z3 which was "inspired by" the CBMC implementation but this is lost to the mists of time.

MathSAT

Source not available, implementation is "inspired by" the CBMC one and is thus similar in size, etc.

CVC4

One of my CVC4 branches:

https://github.com/martin-cs/CVC4/tree/floating-point-symfpu

has a bit-blasting floating-point engine. It is written as a 'stand-alone' library ( see src/symfpu - I would give the full link but github prevents more than two links per post...) which will be released separately ... soon. It is parameterised in the 'back-end' so that it can be used as an arbitrary precision floating-point library, generate bit-vector expressions for different solvers, etc. It is about 3.5KLoC of code but does contain multiple implementations of some operations. It was written from scratch (although I have read the Handbook of Floating-Point).

SONOLAR

Source not available, I believe it to be implemented in C++ and have a feeling that someone told me that it was based on the Mueller and Paul book.

Note that there has been multiple, serious, independent efforts to (cross) verify and validate these implementations. I won't claim that everything is perfect (we're still trying to get full confidence on remainder and FMA) but you should find there they are free of obvious bugs.

You could use VHDL or Verilog designs but ... what makes a good synthesisable FPU is not (necessarily) something that makes a good encoding. I know some have used SoftFloat as a source of implementations but similar comments hold.