Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

Demonstrates how to use uninterpreted function models to synthesize a simple two-bit multiplier.

# Documentation

mul22 :: (SBool, SBool) -> (SBool, SBool) -> (SBool, SBool) Source #

The uninterpreted implementation of our 2x2 multiplier. We simply
receive two 2-bit values, and return the high and the low bit of the
resulting multiplication via two uninterpreted functions that we
called `mul22_hi`

and `mul22_lo`

. Note that there is absolutely
no computation going on here, aside from simply passing the arguments
to the uninterpreted functions and stitching it back together.

NB. While definining `mul22_lo`

we used our domain knowledge that the
low-bit of the multiplication only depends on the low bits of the inputs.
However, this is merely a simplifying assumption; we could have passed
all the arguments as well.

synthMul22 :: Goal Source #

Synthesize a 2x2 multiplier. We use 8-bit inputs merely because that is
the lowest bit-size SBV supports but that is more or less irrelevant. (Larger
sizes would work too.) We simply assert this for all input values, extract
the bottom two bits, and assert that our "uninterpreted" implementation in `mul22`

is precisely the same. We have:

`>>>`

Satisfiable. Model: mul22_hi :: Bool -> Bool -> Bool -> Bool -> Bool mul22_hi False True True False = True mul22_hi False True True True = True mul22_hi True False False True = True mul22_hi True False True True = True mul22_hi True True False True = True mul22_hi True True True False = True mul22_hi _ _ _ _ = False mul22_lo :: Bool -> Bool -> Bool mul22_lo True True = True mul22_lo _ _ = False`sat synthMul22`

It is easy to see that the low bit is simply the logical-and of the low bits. It takes a moment of
staring, but you can see that the high bit is correct as well: The logical formula is `a1b xor a0b1`

,
and if you work out the truth-table presented, you'll see that it is exactly that. Of course,
you can use SBV to prove this. First, define the model we were given to make it symbolic:

`>>>`

mul22_hi :: SBool -> SBool -> SBool -> SBool -> SBool mul22_hi a1 a0 b1 b0 = ite ([a1, a0, b1, b0] .== [sFalse, sTrue , sTrue , sFalse]) sTrue $ ite ([a1, a0, b1, b0] .== [sFalse, sTrue , sTrue , sTrue ]) sTrue $ ite ([a1, a0, b1, b0] .== [sTrue , sFalse, sFalse, sTrue ]) sTrue $ ite ([a1, a0, b1, b0] .== [sTrue , sFalse, sTrue , sTrue ]) sTrue $ ite ([a1, a0, b1, b0] .== [sTrue , sTrue , sFalse, sTrue ]) sTrue $ ite ([a1, a0, b1, b0] .== [sTrue , sTrue , sTrue , sFalse]) sTrue sFalse :}`:{`

Now we can say:

`>>>`

Q.E.D.`prove $ \a1 a0 b1 b0 -> mul22_hi a1 a0 b1 b0 .== (a1 .&& b0) .<+> (a0 .&& b1)`

and rest assured that we have a correctly synthesized circuit!