> import Lava
> import Lava.Virtex2

Xilinx Lava では Bit は定義されている
一方 low, high は定義されていない
（そのかわり gnd, vcc がある）

§8.2

> halfAdd :: (Bit, Bit) -> Out (Bit, Bit)
> halfAdd (a, b) =
>   do
>     sum  <- xor2 (a, b)
>     cout <- and2 (a, b)
>     return (sum, cout)

シミュレーション機能は Xilinx 版では削られている？

> fullAdd :: (Bit, (Bit, Bit)) -> Out (Bit, Bit)
> fullAdd (cin, (a, b)) =
>   do
>     (sum1, car1) <- halfAdd (a, b)
>     (sum, car2)  <- halfAdd (cin, sum1)
>     cout         <- xor2 (car1, car2)
>     return (sum, cout)

§8.3

(bitAdder はあとで別定義が出てくるのでコメント化)

bitAdder :: (Bit, [Bit]) -> Out ([Bit], Bit)
bitAdder (cin, [])     = return ([], cin)
bitAdder (cin, a : as) =
  do
    (sum, car)   <- halfAdd (cin, a)
    (sums, cout) <- bitAdder (car, as)
    return (sum : sums, cout)

> adder :: (Bit, ([Bit], [Bit])) -> Out ([Bit], Bit)
> adder (cin, ([], []))         = return ([], cin)
> adder (cin, (a : as, b : bs)) =
>   do
>     (sum, car)   <- fullAdd (cin, (a, b))
>     (sums, cout) <- adder (car, (as, bs))
>     return (sum : sums, cout)

TODO: 練習問題 8.1〜8.4

§8.4

->- は Xilinx Laba で定義済み
一方 -|- は定義されてないので定義する

> (-|-) :: (a -> Out c) -> (b -> Out d) -> ((a, b) -> Out (c, d))
> (f -|- g) (a, b) =
>   do
>     c <- f a
>     d <- g b
>     return (c, d)

> row :: ((c, a) -> Out (b, c)) -> (c, [a]) -> Out ([b], c)
> row f (cin, [])     = return ([], cin)
> row f (cin, a : as) =
>   do
>     (b, car)   <- f (cin, a)
>     (bs, cout) <- row f (car, as)
>     return (b : bs, cout)

> bitAdder :: (Bit, [Bit]) -> Out ([Bit], Bit)
> adder' :: (Bit, [(Bit, Bit)]) -> Out ([Bit], Bit)

bitAdder (cin, inps) = row halfAdd (cin, inps)
adder' (cin, inps)   = row fullAdd (cin, inps)

> bitAdder = row halfAdd
> adder'   = row fullAdd

TODO: 練習問題 8.5〜8.7

§8.5

nand2 は定義されてないのでここで定義する

> nand2 :: (Bit, Bit) -> Out Bit
> nand2 = lut2gate (\a b -> not $ a && b) "nand2"

> prop_HalfAddOutputNeverBothHigh :: (Bit, Bit) -> Out Bit
> prop_HalfAddOutputNeverBothHigh (a, b) =
>   do
>     (sum, cout) <- halfAdd (a, b)
>     ok <- nand2 (sum, cout)
>     return ok

verify もない

> prop_FullAddOutputNeverBothHigh :: (Bit, (Bit, Bit)) -> Out Bit
> prop_FullAddOutputNeverBothHigh (c, (a, b)) =
>   do
>     (sum, cout) <- fullAdd (c, (a, b))
>     ok <- nand2 (sum, cout)
>     return ok

> prop_HalfAddCommutative :: (Bit, Bit) -> Out Bit
> prop_HalfAddCommutative (a, b) =
>   do
>     (sum1, cout1) <- halfAdd (a, b)
>     (sum2, cout2) <- halfAdd (b, a)
>     ok1 <- xnor2 (sum1, sum2)
>     ok2 <- xnor2 (cout1, cout2)
>     ok <- and2 (ok1, ok2)
>     return ok

<==> のような便利な演算子がないのでこの節の以降は面倒なので飛ばす

§8.6

delay もない?

§8.7 §8.8 simulate で確認できないので略す

§8.9

練習問題 8.24 現在の Xilinx Lava は lut で回路を実装するように
特化されており、lut を普通に実装できるようなプリミティブを持ってない

練習問題 8.25 Xilinx Lava には元から and6 があるので、my_and6 とする
Xilinx Lava 組み込みの lut4gate を使う

> my_and6 :: (Bit, Bit, Bit, Bit, Bit, Bit) -> Out Bit
> my_and6 inp =
>   do
>     high <- vcc
>     tmp <- lut4gate and4func "my_and6_tmp" (i0, i1, i2, i3)
>     out <- lut4gate and4func "my_and6_tmp" (tmp, i4, i5, high)
>     return out
>   where
>     (i0, i1, i2, i3, i4, i5) = inp
>     and4func a b c d = a && b && c && d