File size: 1,174 Bytes
56de343 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 | module IR.BitVec where
import IR.Boolean
type BitVec = [BExpr]
bvConst :: Int -> Int -> BitVec
bvConst width val = [if testBit i then BTrue else BFalse | i <- [0..width-1]]
where testBit i = (val `div` (2^i)) `mod` 2 == 1
bvVar :: Int -> Int -> BitVec
bvVar start width = [BVar (start + i) | i <- [0..width-1]]
bvNot :: BitVec -> BitVec
bvNot = map bnot
bvAnd :: BitVec -> BitVec -> BitVec
bvAnd = zipWith band
bvOr :: BitVec -> BitVec -> BitVec
bvOr = zipWith bor
bvXor :: BitVec -> BitVec -> BitVec
bvXor = zipWith bxor
halfAdder :: BExpr -> BExpr -> (BExpr, BExpr)
halfAdder a b = (bxor a b, band a b)
fullAdder :: BExpr -> BExpr -> BExpr -> (BExpr, BExpr)
fullAdder a b cin =
let (s1, c1) = halfAdder a b
(s2, c2) = halfAdder s1 cin
in (s2, bor c1 c2)
bvAdd :: BitVec -> BitVec -> BitVec
bvAdd [] [] = []
bvAdd as bs = go as bs BFalse
where
go [] [] _ = []
go (a:as') (b:bs') cin =
let (s, cout) = fullAdder a b cin
in s : go as' bs' cout
go _ _ _ = []
bvEq :: BitVec -> BitVec -> BExpr
bvEq as bs = foldr band BTrue (zipWith xnor as bs)
where xnor a b = bnot (bxor a b)
|