Discrete Mathematics Using a Computer Chapter 13: Circuit Simulation

DiscreteMathComputer13.hs

{- Discrete Mathematics Using a Computer
   Chapter 13: Circuit Simulation
   
   Story: verify circuit properties using math because actually building and 
          testing is expensive.
-}
module Main where
import Data.List (intersperse)

-- Signal is anything that can be manipulated by circuits
-- e.g. Bool

-- Since nand gates are functionally complete, they'll be the only required
-- function. 
-- The other gates are derived using nand (if user doesn't provide them)

class Signal a where
  nand2 :: a -> a -> a
  zero :: a
  
  inv :: a -> a
  inv x = nand2 x x

  and2 :: a -> a -> a
  and2 x y = inv $ nand2 x y
  
  or2 :: a -> a -> a
  or2 x y = inv $ and2 (inv x) (inv y)
  
  xor2 :: a -> a -> a
  xor2 x y = nand2 (nand2 x z) (nand2 z y)
    where z = nand2 x y

{- Proof of correctness of the default functions.

--------------------
Correctness of inv

nand2 x x = not (and x x) = not x

--------------------
Correctness of and2

and = not . nand = not (not and) = and

--------------------
Correctness of or2

x or y = not (not x or y) = not ((not x) and (not y)) = nand (not x) (not y)

--------------------
Correctness of xor2

| x | y | z = nand x y | a = nand x z | b = nand z y | nand a b |
| T | T | F            | T            | T            | F        |
| T | F | T            | F            | T            | T        |
| F | T | T            | T            | F            | T        |
| F | F | T            | T            | T            | F        | 
so, nand a b is exactly a xor b  
-}

instance Signal Bool where
  nand2 x y =  not $ x && y
  zero = False
  
--------------------------------------------------------------------------------
-- Designing Circuits from Truth Tables
  
{- Suppose we're given a truth table:

| a | b | c | output |   |
|---+---+---+--------+---|
| 0 | 0 | 0 |      0 |   |
| 0 | 0 | 1 |      1 |   |
| 0 | 1 | 0 |      0 |   |
| 0 | 1 | 1 |      1 |   |
| 1 | 0 | 0 |      1 |   |
| 1 | 0 | 1 |      0 |   |
| 1 | 1 | 0 |      1 |   |
| 1 | 1 | 1 |      0 |   |

To turn this into a circuit, first note the rows that have nonzero outputs
we have: 0 0 1, 0 1 1, 1 0 0, 1 1 0

convert terms: e.g. 0 0 1 = (not a) and (not b) and c 
               e.g. 0 1 1 = (not a) and b and c
               e.g. 1 0 0 = a and (not b) and (not c)
               e.g. 1 1 0 = a and b and (not c)

or the terms together:

(~a ^ ~b ^ c) v (~a ^ b ^ c) v (a ^ ~b ^ ~c) v (a ^ b ^ ~c)

That is the required circuit:
-}

-- first, some helpers
and3 :: Signal a => a -> a -> a -> a
and3 a b c = and2 a (and2 b c)

or3 :: Signal a => a -> a -> a -> a
or3 a b c = or2 a (or2 b c)

or4 :: Signal a => a -> a -> a -> a -> a
or4 a b c d = or2 (or2 a b) (or2 c d)

exampleCircuit :: Signal a => a -> a -> a -> a
exampleCircuit a b c = or4 (and3 na nb c) 
                           (and3 na b c)
                           (and3 a nb nc)
                           (and3 a b nc)
  where na = inv a
        nb = inv b
        nc = inv c

-- TODO: Look at 6.004 maps to use karnaugh maps to simplify the circuit
-- TODO: Make a tiny jsim! Or atleast, get the gate timings from jsim
--       and propagate that (state monad?) to get an idea about how fast the circuit is.
        
{- Exercise 1: Write a circuit that implements:

| a | b | c | output |
| 0 | 0 | 0 |      1 |
| 0 | 0 | 1 |      1 |
| 0 | 1 | 0 |      0 |
| 0 | 1 | 1 |      0 |
| 1 | 0 | 0 |      0 |
| 1 | 0 | 1 |      1 |
| 1 | 1 | 0 |      1 |
| 1 | 1 | 1 |      1 |

Easier to take invert the outputs of the 3 functions that give 0s

~((na ^ b ^ nc) v (na ^ b ^ c) v (a ^ nb ^ nc))
= ~((na ^ b) v (a ^ nb ^ nc))  Combining ((na ^ b) ^ nc) v ((na ^ b) ^ c)
-}

exerciseCircuit :: Signal a => a -> a -> a -> a
exerciseCircuit a b c = inv $ or2 (and2 na b) (and3 a nb nc)
  where na = inv a
        nb = inv b
        nc = inv c

-- MAIN> [(a, b, c, exerciseCircuit a b c) | a <- [True, False], 
--         b <- [True, False], 
--         c <- [True, False]]
-- [(True,True,True,True),(True,True,False,True),(True,False,True,True),
--  (True,False,False,False),(False,True,True,False),(False,True,False,False),
--  (False,False,True,True),(False,False,False,True)]

--------------------------------------------------------------------------------
-- Multiplexors
{- Mux1 takes in a control line and two inputs: a and b
   When control is 0, returns a
                   1, returns b

   So it's an "if-then" of the circuit world.
-}

mux1 :: Signal a => a -> a -> a -> a
-- mux1 a x y = or2 (and2 (inv a) x) (and2 a y) -- book's definition. yuck
-- I made a truth table and got:
-- (nc ^ x ^ ny) v (nc ^ x ^ y) v (c ^ ~x ^ y) v (c ^ x ^ y)
-- simplify: (nc ^ x) v (c ^ y)
-- nandify!: ~(nc ^ x) NAND ~(c ^ y)
--         :  (nc NAND x) NAND (c NAND X)
mux1 c x y = (nc `nand2` x) `nand2` (c `nand2` x)
  where nc = inv c
        
-- Demultiplexor: takes a single data input x and a control input a
-- Provides two outputs: (z0, z1)
-- x is supplied to the output selected by a
-- 0 is sent to the other one.
        
demux1 :: Signal a => a -> a -> (a,a)
demux1 a x = (and2 (inv a) x,
              and2 a x)

--------------------------------------------------------------------------------
-- Doing some arithmetic: Half Adder

{- Truth Table for the adder:
   "c" is the carry term, "s" is the sum term

   | x | y | c | s |
   | 0 | 0 | 0 | 0 |
   | 0 | 1 | 0 | 1 |
   | 1 | 0 | 0 | 1 |
   | 1 | 1 | 1 | 0 |

   Note: c is just and2
         x is just xor
-}

halfAdder :: Signal a => a -> a -> (a,a)
halfAdder x y = (x `and2` y, x `xor2` y)

{- THEOREM: Let (c,s) = halfAdd a b then a + b = 2 * c + s
where + and * is binary arithmetic.
Proof: look at the truth table for the half adder. we have:
0 + 0 = 2 * 0 + 0 = 0 
0 + 1 = 2 * 0 + 1 = 1
1 + 0 = 2 * 0 + 1 = 1
1 + 1 = 2 * 1 + 0 = 10
So, the half adder is doing addition of two binary digits
-}

--------------------------------------------------------------------------------
-- Building a Full Adder
-- We need three inputs: two for the bits we want to add, and another that represents
-- the carry in.
-- We'll build a full adder out of two half adders:

fullAdder :: Signal a => (a,a) -> a -> (a,a)
fullAdder (a,b) c = (or2 w y, s)
  where (w, x) = halfAdder a b
        (y, s) = halfAdder x c

{- THEOREM: Correctness of full adder
   Let (c', s) = fullAdder (a,b) c. Then,
   c' * 2 + s = a + b + c [binary addition and multiplication]

   Direct Proof using the correctness of Half-Adder

   a + b + c
   = (a + b) + c         by associativity of binary addition
   = (2 * w + x) + c     where (w,x) = halfAdd a b
   = 2 * w + (x + c)
   = 2 * w + (2 * y + s)  where (y,s) = halfAdd x c
   = 2 * (w + y) + s
     Now the problem is that i need to convert w + y into w or y

   LEMMA 1: w and y are never simultaneously 1.
   PROOF: By contradiction.
    Suppose we have w = 1 and y = 1.

    Since w is the carry from a + b, both bits a and b must have been 1.
    In that case, x, which is the sum part of a + b, must be 0 (since 1 + 1 = 10)

    Since y is the carry from x + c, both x and c must be 1.
    But we just showed that x must be 0.
    
    Hence contradiction.

   LEMMA 2: "w + y" is equivalent to "w or y" when w and y are not simulatenously 1
   PROOF: Direct Proof Using Truth Table

   | w | y | w or y | w + y |
   | 0 | 0 |      0 |     0 |
   | 0 | 1 |      1 |     1 |
   | 1 | 0 |      1 |     1 |

   Back to the theorem:
    Since w and y cannot both be simultaneously 1 (by Lemma 1), we can write:

    = 2 * (w or y) + s      
    = (w or y, s)     since 2 * p + q = (p,q) in the carry notation.

-}

-- Exercise 3: Verify the half adder results.

halfAdderTable :: [(Bool, Bool, (Bool, Bool))]
halfAdderTable = [(x, y, halfAdder x y) | x <- [True, False], y <- [True, False]]

showHalfAdderTable :: IO ()
showHalfAdderTable = showHeader >> mapM_ showLine halfAdderTable
  where showLine (x, y, (c,s)) = putStrLn $ show x ++ "\t" ++ show y ++ "\t" ++ show c ++ "\t" ++ show s
        showHeader = putStrLn"x\ty\tc\ts"

{- *Main> showHalfAdderTable
x	y	c	s
True	True	True	False
True	False	False	True
False	True	False	True
False	False	False	False
-}

-- Exercise 4: Prove Half Adder correctness. Done earlier.
-- Exercise 5: Prove Full adder correctness. Done.
        
--------------------------------------------------------------------------------
-- Binary Representation
        
-- Note: the book talks about using a typeclass called Static to represent these
-- signals, but the definition is not in Stdm. So i'll just use Integers.
-- 0 means 0, 1 means 1.
        
-- Big Endian aka Higher order bit first
-- 110 means 6
-- Little Endian aka Lower order bit first
-- 110 means just 11, which is 3
        
bigEndian :: [Integer] -> Integer
bigEndian = foldl conv 0 
  where conv acc new = 2 * acc + new

-- *Main> bigEndian [1,1,0]
-- 6
-- *Main> bigEndian [1,1]
-- 3

littleEndian :: [Integer] -> Integer
littleEndian = foldr conv 0
  where conv new acc = new + 2 * acc
        
-- *Main> littleEndian [1,1,0]
-- 3
-- *Main> littleEndian [1,1]
-- 3
-- *Main> littleEndian [1,0]
-- 1
-- *Main> littleEndian [0,1]
-- 2

wordValue = bigEndian -- this is what the book is calling the fn

-- Exercise 6: Work out the value of [1,0,0,1,0] in big endian
-- 2^4 * 1 + 2^1 * 1 = 16 + 2 = 18

-- *Main> wordValue [1,0,0,1,0]
-- 18

--------------------------------------------------------------------------------
-- Ripple Carry Adder
-- IDEA: Chain full adders so that the carry is propagated. This way we can 
--       words (list of bits) instead of just bits.

-- Assume we're using little endian (more convenient since our lists are linked lists)

adder :: Signal a => [a] -> [a] -> [a]
adder xs ys = adder' xs ys (zero, [])
  
{- VERSION 1:
adder' :: Signal a => [a] -> [a] -> (a, [a]) -> [a]
adder' []     [] (c, s) = reverse $ c:s
adder' (x:xs) [] (c, s) = adder' xs [] (c', s':s)
  where (c', s') = halfAdder c x
adder' [] (y:ys) (c, s) = adder' [] ys (c', s':s)
  where (c', s') = halfAdder c y
adder' (x:xs) (y:ys) (c,s) = adder' xs ys (c', s':s)
  where (c', s') = fullAdder (x,y) c
-}

-- If i just use the full adder everywhere, I could simplify that:
adder' :: Signal a => [a] -> [a] -> (a, [a]) -> [a]
adder' []     []     (c,s) = reverse $ c:s
adder' (x:xs) []     (c,s) = adder' xs [] $ newState x zero c s
adder' []     (y:ys) (c,s) = adder' [] ys $ newState y zero c s
adder' (x:xs) (y:ys) (c,s) = adder' xs ys $ newState x y c s
  
newState a b c s = (c', s':s)
  where (c', s') = fullAdder (a,b) c

instance Signal Integer where
  nand2 0 0 = 1
  nand2 0 1 = 1
  nand2 1 0 = 1
  nand2 1 1 = 0
  nand2 _ _ = error "0 and 1 are the only valid signals"
  
  zero = 0
    
-- now we can do:
egAdder1, egAdder2, egAdder3 :: [Integer]
egAdder1 = adder [1] [1] -- [0,1]
egAdder2 = adder [1,1,1] [1,1,1] -- [0,1,1,1]
egAdder3 = adder [0] [1,1,1] -- [1,1,1,0]

-- Exercise 7: Can the adder do 3 + 8 correctly?
-- 3 : [1,1]. 8: [0,0,0,1]
-- 11 : [1,1,0,1]
-- Remember: we're doing LSB First
ex7 :: [Integer]
ex7 = adder [1,1] [0,0,0,1]

-- *Main> ex7
-- [1,1,0,1,0]

--------------------------------------------------------------------------------
{- Circuit Patterns
   The book built a 4 bit adder by manually hooking up 4 full adders
   Now, they're building the following abstraction:

      x0     x1            xn-1
 a'<-[f] <- [f] <- ... <- [f] <- a
      y0     y1            yn-1

    will be represented as:
             [x]
    a' <- [mscanr f] <- a
             [y]
-}

mscanr :: (b -> a -> (a,c)) -> a -> [b] -> (a,[c])
mscanr _ a [] = (a, [])
mscanr f a (x:xs) = (a'', y:ys)
  where (a', ys) = mscanr f a xs
        (a'', y) = f x a'

-- This is designed to work in an msb first setting: 
-- imagine f is the full adder then when we do mscanr f a xs,
-- we get the sum of the remainder of the sequence
-- then we add it to the current digit.
        
-- now they define:
rippleAdd :: Signal a => a -> [(a,a)] -> (a, [a])
rippleAdd c zs = mscanr fullAdder c zs

-- for this to work with uneven length lists, you can't just use zip
-- because zip would discard the remainder of the longer list
-- So, we need:

zipSignal :: Signal a => [a] -> [a] -> [(a,a)]
zipSignal [] ys = zip (repeat zero) ys
zipSignal xs [] = zip xs (repeat zero)
zipSignal (x:xs) (y:ys) = (x,y):zipSignal xs ys

-- *Main> zipSignal [1,1] [1,1,1]
-- [(1,1),(1,1),(0,1)]
-- *Main> zipSignal [1,1] [1,1,1,1]
-- [(1,1),(1,1),(0,1),(0,1)]
-- *Main> zipSignal [1,1,1,1] [1,1]
-- [(1,1),(1,1),(1,0),(1,0)]

-- Give it the same signature as my adder
-- and maybe reverse arguments to make it work lsb-first
bookAdd :: Signal a => [a] -> [a] -> [a]
bookAdd xs ys = c:s
  where (c,s) = rippleAdd zero $ zipSignal xs ys 

-- actually, working msb first is much more reasonable:
-- *Main> bookAdd [1] [1]
-- [1,0]
-- *Main> bookAdd [1] [1,1]
-- [1,0,1]
        
{- Exercise 8: Draw a diagram showing the structure of the circuit specified by 
   mscanr f a [(x0,y0), (x1, y1), (x2,y2)]
         (x0,y0) (x1,y1) (x2,y2)
   a' <- [f]   <- [f]   <- [f] <- a
         z0       z1        z2
   zs are the outputs
-}
--------------------------------------------------------------------------------
-- My adder revisited
-- the middle two clauses in adder' dealt with the case when one list was
-- shorter than the other. But i have zipSignal. So I should be able to simplify it

adder'' :: Signal a => [(a,a)] -> (a, [a]) -> [a]
adder'' []          (c,s) = reverse $ c:s
adder'' ((x,y):xys) (c,s) = adder'' xys newState
  where (c', s') = fullAdder (x,y) c
        newState = (c', s':s)

newAdder :: Signal a => [a] -> [a] -> [a]
newAdder xs ys = adder'' (zipSignal xs ys) (zero, [])

-- the adder helper is a bit simpler than the older one.

--------------------------------------------------------------------------------
-- Exercise 9: Test the ripple carry adder using 13 + 41 = 54

ex9 :: [Integer]
ex9 = bookAdd [0,0,1,1,0,1] [1,0,1,0,0,1]

-- *Main> ex9
-- [0,1,1,0,1,1,0]
-- *Main> bigEndian ex9
-- 54

ex9my :: [Integer]
ex9my = newAdder [1,0,1,1] [1,0,0,1,0,1]

-- *Main> ex9my
-- [0,1,1,0,1,1,0]
-- *Main> littleEndian ex9my
-- 54

--------------------------------------------------------------------------------
{- THEOREM: Correctness of the ripple carry adder

   Let xs and ys be k-bit words.
   Define (c,sum) = rippleAdd zero (zip xs ys)

   Then, c * 2^k + wordValue ss = wordValue xs + wordValue ys

   PROOF: By induction on k.

   Case: k = 0 i.e. xs = ys = [], zs = []
     rippleAdd zero []
   = mscanr fullAdder zero []
   = (zero, [])
    zero + wordValue [] = zero + zero = zero . Which is correct.

   Inductive Case: k = n, inductive hypothesis: ripple carry adder works for n-1 bit words.

    rippleAdd zero [(x0,y0), ... (x_n-1, y_n-1)]
   = mscanr fullAdder zero [(x0, y0), ..., (x_n-1, y_n-1)]
    
    Let (a', qs) = mscanr fullAdder zero [(x1, y1), ... (x_n-1, y_n-1)]
                 = rippleAdd zero [(x1, y1), ... (x_n-1, y_n-1)]
       By induction hypothesis, 2 * a' ^(n-1) + wordValue qs = wordValue xs + wordValue ys

    Now, fullAdder (x0, y0) a' = (a'', q)  where a'' * 2 + q = x0 + y0 + a'
    
    rippleAdder returns (a'', q:qs). a'' is the final carry so it is at position 2^n+1. q:qs is n bits long

    The numeric value  of this is:
      a'' * 2 ^(n + 1) + wordValue q:qs
    = a'' * 2^(n + 1) + q * 2^n + wordValue qs
    = (a'' * 2 + q) * 2^n + wordValue qs
    = (x0 + y0 + a') * 2^n + wordValue qs   -- by the correctness of full adder
    = a' * 2^n + (x0 + y0) * 2^n + wordvalue qs
    = (x0 + y0) * 2^n + a' * 2^n + wordvalue qs
    = (x0 + y0) * 2^n + wordvalue xs + wordvalue ys   -- by induction hypothesis
    = wordvalue (x0:xs) + wordvalue (y0:ys)  -- since xs and ys are n-1 bits long, can add x*2^n to the front by cons
    = wordvalue xss + wordvalue yss
    QED
-}

-- =============================================================================
-- Binary Comparator

-- We'll have our comparator return a triple (lt, eq, gt) where at a value of 1
-- signifies what it is.
{- TRUTH TABLE

| x | y | lt | eq | gt |
| 0 | 0 |  0 |  1 |  0 |
| 0 | 1 |  1 |  0 |  0 |
| 1 | 0 |  0 |  0 |  1 |
| 1 | 1 |  0 |  1 |  0 |

lt is: ~x ^ y
eq is: (~x ^ ~y) v (x ^ y) -- equivalently, not . xor
gt is: x ^ ~y
-}

halfCmp :: Signal a => (a, a) -> (a,a,a)
halfCmp (x, y) = (and2 (inv x) y,
                  inv (xor2 x y),
                  and2 x (inv y))

-- Full comparator:
-- We have result from comparing previous bits (which were more significant)
-- If we had lt or gt, the answer from this block cannot change
-- But, if we got eq, we need to compare and propagate this forward.
-- We don't have "pattern matching" in circuits, so use gates to do something equivalent.

fullCmp :: Signal a => (a, a, a) -> (a, a) -> (a, a, a)
fullCmp (lt, eq, gt) (x, y) = (or2 lt (and3 eq (inv x) y), -- 1
                               and2 eq (inv (xor2 x y)),   -- 2 
                               or2 gt (and3 eq x (inv y))) -- 3

-- Explanation:
-- 1: If the previous bit was LT, then the answer is automatically lt. hence or2
--    If it was EQ, we need to perform the lt check (as in half adder)
--    NOTE: If the previous bit was GT, then the answer is automatically 0. 
--    Hence we do an and2 with eq to ensure we're in the eq case
-- 2: If the previous bit was not an EQ, the answer is automatically 0.
--    Hence and with EQ and perform check
-- 3: If previous bit was GT, answer is automatically gt
--    If it was EQ, then we need to check. 


rippleCmp :: Signal a => [(a,a)] -> (a,a,a)
rippleCmp z = foldl fullCmp (zero, inv zero, zero) z 

-- Base case: assume equality
-- Bug in the book: their base case is (False, True, False) which works only if a is Bool

-- Exercise 10: Test the half comparator
halfCmpTable :: [(Integer, Integer, (Integer, Integer, Integer))]
halfCmpTable = [(x, y, halfCmp (x,y)) | x <- [0,1], y <- [0,1]]

showHalfCmpTable :: IO ()
showHalfCmpTable = showHeader >> mapM_ showLine' halfCmpTable
  where showHeader = putStrLn"X\tY\tLT\tEQ\tGT"
        showLine (x, y, (lt, eq, gt))= putStrLn $ show x ++ "\t" ++ show y ++ "\t|\t" ++ show lt ++ "\t" ++ show eq ++ "\t" ++ show gt

-- is this better?
showLine' (x, y, (lt, eq, gt)) = (putStrLn . concat . intersperse "\t" . map show) [x,y,lt, eq, gt]

-- Exercise 11: Three Test cases for Full adder

ex11lt, ex11eq, ex11gt :: (Integer, Integer, Integer)
ex11lt = rippleCmp $ zip [1,0,0] [1,0,1]
ex11eq = rippleCmp $ zip [1,1,1] [1,1,1]
ex11gt = rippleCmp $ zip [1,1,1] [1,1,0]

-- *Main> ex11lt
-- (1,0,0)
-- *Main> ex11eq
-- (0,1,0)
-- *Main> ex11gt
-- (0,0,1)

-- =============================================================================
{- Suggestions for Further Reading

1. Derivation of logarithmic time carry lookahead addition circuit
   by O'Donnell and Runger

2. The hydra computer hardware description language
   (dcs.gla.ac.uk/jtod/hydra/) <- doesn't exist yet
    Go to John O'Donnell's site at dcs.gla.ac.uk/~jtod

-}

-- =============================================================================
-- Review Exercises

--------------------------------------------------------------------------------
-- Exercise 12: implement and4 using and2

and4 :: Signal a => a -> a -> a -> a -> a
and4 a b c d = and2 (and2 a b) (and2 c d)

--------------------------------------------------------------------------------
-- Exercise 13: Test the full adder
-- I did.

--------------------------------------------------------------------------------
{- Exercise 14: 
   Suppose computer has 8 memory locations with addresses 0, 1, 2, ... 7
   We can represent the address with 3 bits.
   Suppose we are using MSB-first.

   Design a circuit that takes in 3 address bits a0, a1, a2 and outputs the select
   signals.

   So, there are 8 select signals, one for each location
   e.g. (1,1,1) means location 7; signal would be 10 000 000
   e.g. (0,1,1) means location 3; signal would be 00 000 100
   e.g. (0,0,1) means location 1; signal would be 00 000 001

   Basically, we're building an 8 way demultiplexer.
-}

-- I'll try to build a 2-bit demux using and gates only first
{-  
  | c1 | c0 | z0 | z1 | z2 | z3 |
  |  0 |  0 |  a |  0 |  0 |  0 |
  |  0 |  1 |  0 |  a |  0 |  0 |
  |  1 |  0 |  0 |  0 |  a |  0 |
  |  1 |  1 |  0 |  0 |  0 |  a |

  a is the value of the input.
  So, z0 = and3 ~c1 ~c0 a
      z1 = and3 ~c1 c0 a
      z2 = and3 c1 ~c0 a
      z3 = and3 c1 c0 a
-}

demux2And :: Signal a => a -> a -> a -> (a, a, a, a)
demux2And a c1 c0 = (and3 nc1 nc0 a,
                     and3 nc1 c0 a,
                     and3 c1 nc0 a,
                     and3 c1 c0 a)
  where nc1 = inv c1
        nc0 = inv c0

-- Building a 8 way demux:
demux3And a c2 c1 c0 = (and4 nc2 nc1 nc0 a,
                        and4 nc2 nc1 c0  a,
                        and4 nc2  c1 nc0 a,
                        and4 nc2  c1 c0  a,
                        and4 c2  nc1 nc0 a,
                        and4 c2  nc1 c0  a,
                        and4 c2   c1 nc0 a,
                        and4 c2   c1 c0  a)
  where nc2 = inv c2
        nc1 = inv c1
        nc0 = inv c0

-- note: my demuxes output in lsb first.

--------------------------------------------------------------------------------
-- Ex 15: Does definition prevent word size to be 0 in ripple Add?
-- No. there is a clause in mscanr for empty list.
-- What does it mean when word size is 0?
-- It's as if we didn't add anything, so the answer is just 0
        
--------------------------------------------------------------------------------
-- Ex 16: Can word size be negative?
-- No. We have to pass a list of bits.
-- The size of a list is 0.. so can't have -ve sized words.
        
--------------------------------------------------------------------------------
-- Ex 17: Why didn't we do complete checking for ripple Adder?
-- Complete checking means checking each of the 2^k combinations
-- For a 64-bit ripple adder, that means checking 2^64 = 10^19 combinations!
-- Even if we could do 1 check every nano seconds, it'd take 10^9 seconds = 31 years
-- But this is embarrassingly parallel, so with 2 computers could do it in 15 years

--------------------------------------------------------------------------------
-- Ex 18: Suppose we're doing comparison or addition on multiword integers (big integers)
-- Then, the ripple adder needs a carry in, but a ripple comparator doesn't need a carry in
-- that is in between lines why?
-- Answer: We don't need a carry in because if we're checking the second word, it means
-- that the previous word (more significant word) must have been equal
-- so the starting case is always Equality.
-- One consequence of this is that we can do multiword comparison in time proportional to 
-- the number of words: compare each word in parallel, then pick the first answer (starting from MSB)
-- that is not EQ.