Discrete Mathematics using a Comptuter (O’Donnell, Hall, Page) Chapter 13
Discrete Mathematics with Applications - Metric Edition (Epp) Chapter 2.4, 2.5
https://runestone.academy/ns/books/published/ads/s-logic-design.html
https://en.wikipedia.org/wiki/Logic_gate
https://en.wikipedia.org/wiki/Combinational_logic
https://en.wikipedia.org/wiki/Adder_(electronics)
Code-DMUC/Stdm13CircuitDesign.hs
-- # Software Tools for Discrete Mathematics
module Stdm13 where
-- # Chapter 13. Discrete Mathematics in Circuit Design
inv :: Bool -> Bool
inv = not
and2 :: Bool -> Bool -> Bool
and2 = (&&)
and3 :: Bool -> Bool -> Bool -> Bool
and3 True True True = True
and3 _ _ _ = False
or2 :: Bool -> Bool -> Bool
or2 = (||)
-- xor circuit truth table
-- a b | out | long
-- 0 0 0
-- 1 1 0
-- 0 1 1 ¬a ∧ b
-- 1 0 1 a ∧ ¬b
-- Derived from table:
-- (¬a ∧ b) ∨ (a ∧ ¬b)
xor :: Bool -> Bool -> Bool
xor = (/=)
-- Table-derived construction:
xorV0 :: Bool -> Bool -> Bool
xorV0 a b = or2 (and2 (inv a) b) (and2 a (inv b))
-- The xor gate can be made from other gates as well:
-- https://en.wikipedia.org/wiki/XOR_gate#Alternatives
xorV1 :: Bool -> Bool -> Bool
xorV1 a b = and2 (inv (and2 a b)) (or2 a b)
xorV2 :: Bool -> Bool -> Bool
xorV2 a b =
inv
( and2
( inv
( and2
a
(inv (and2 a b))
)
)
( inv
( and2
(inv (and2 a b))
b
)
)
)
xorV3 :: Bool -> Bool -> Bool
xorV3 a b =
or2
( inv
( or2
a
(inv (or2 a b))
)
)
( inv
( or2
(inv (or2 a b))
b
)
)
-- A multiplexor is the hardware equivalent of a conditional (if—then—else) expression.
-- It takes a control input a and two data inputs, x and y.
-- There is one output;
-- if a is 0 then the output is x,
-- but if a is 1 then the output is y.
-- The circuit is implemented using the standard logic gates.
-- | if not True then True else False
-- >>> mux1 True True False
-- False
-- | if not True then False else True
-- >>> mux1 True False True
-- True
-- | if not False then True else False
-- >>> mux1 False True False
-- True
-- | if not False then False else True
-- >>> mux1 False False True
-- False
mux1 :: Bool -> Bool -> Bool -> Bool
mux1 a x y = or2 (and2 (inv a) x) (and2 a y)
-- A demultiplexor is the opposite of a multiplexor.
-- It has a single data input x and a control input a.
-- The circuit produces two outputs (z0, z1).
-- The x input is sent to whichever output is selected by a,
-- and the other output is 0 regardless of the value of x.
-- |
-- >>> demux1 True True
-- (False,True)
-- |
-- >>> demux1 True False
-- (False,False)
-- |
-- >>> demux1 False True
-- (True,False)
-- |
-- >>> demux1 False False
-- (False,False)
demux1 :: Bool -> Bool -> (Bool, Bool)
demux1 a x = (and2 (inv a) x, and2 a x)
-- | Convert True to 1
-- >>> bitValue True
-- 1
-- | Convert False to 0
-- >>> bitValue False
-- 0
bitValue :: Bool -> Int
bitValue x = if x == False then 0 else 1
-- | Convert any array of [Bool] to it's base 10 integer value.
-- >>> wordValue [True,False,False,True,False]
-- 18
-- | Max value in a Byte.
-- >>> wordValue (replicate 8 True)
-- 255
wordValue :: [Bool] -> Int
wordValue [] = 0
wordValue (x : xs) =
let k = length xs
in 2 ^ k * bitValue x + wordValue xs
-- Half adder adds two bits.
-- https://en.wikipedia.org/wiki/Adder_(electronics)#Half_adder
-- Theorem 106 (correctness of half-adder). Let (c, s) = halfAdd a b.
-- Then 2 × bitValue c + bitValue s = bitValue a + bitValue b.
-- Proof. This theorem is easily proved by checking the equation,
-- for each of the four possible combinations of input values.
-- | 0 + 0
-- >>> halfAdd False False
-- (False,False)
-- | 0 + 1
-- >>> halfAdd False True
-- (False,True)
-- | 1 + 0
-- >>> halfAdd True False
-- (False,True)
-- | 1 + 1
-- >>> halfAdd True True
-- (True,False)
halfAdd :: Bool -> Bool -> (Bool, Bool)
halfAdd a b = (and2 a b, xor a b)
-- Full adder adds 3 bits.
-- https://en.wikipedia.org/wiki/Adder_(electronics)#Full_adder
-- Theorem 107 (Correctness of full adder).
-- Let (c' , s) = fullAdd (a, b) c,
-- so that c' is the carry output,
-- and s is the sum output.
-- Then bitValue c' × 2 + bitValue s = bitValue a + bitValue b + bitValue c.
-- | 0 + 0 + 0
-- >>> fullAdd (False, False) False
-- (False,False)
-- | 0 + 0 + 1
-- >>> fullAdd (False, False) True
-- (False,True)
-- | 0 + 1 + 0
-- >>> fullAdd (False, True) False
-- (False,True)
-- | 0 + 1 + 1
-- >>> fullAdd (False, True) True
-- (True,False)
-- | 1 + 0 + 0
-- >>> fullAdd (True, False) False
-- (False,True)
-- | 1 + 0 + 1
-- >>> fullAdd (True, False) True
-- (True,False)
-- | 1 + 1 + 0
-- >>> fullAdd (True, True) False
-- (True,False)
-- | 1 + 1 + 1
-- >>> fullAdd (True, True) True
-- (True,True)
fullAdd :: (Bool, Bool) -> Bool -> (Bool, Bool)
fullAdd (a, b) c =
let (w, x) = halfAdd a b
(y, z) = halfAdd x c
in (or2 w y, z)
-- Ripple carry adders
-- https://en.wikipedia.org/wiki/Adder_(electronics)#Ripple-carry_adder
-- Example: addition of 3 + 8
-- 3 + 8
-- = 0011 ( 2+1 = 3)
-- + 1000 ( 8 = 8)
-- = 1011 (8+2+1 = 11)
-- | 3 + 8
-- >>> add4 False [(False,True),(False,False),(True,False),(True,False)]
-- (False,[True,False,True,True])
add4 :: Bool -> [(Bool, Bool)] -> (Bool, [Bool])
add4 c [(x0, y0), (x1, y1), (x2, y2), (x3, y3)] =
let (c3, s3) = fullAdd (x3, y3) c
(c2, s2) = fullAdd (x2, y2) c3
(c1, s1) = fullAdd (x1, y1) c2
(c0, s0) = fullAdd (x0, y0) c1
in (c0, [s0, s1, s2, s3])
-- Theorem 108 (The n-Bit Ripple Carry Adder).
-- Let xs and ys be k-bit words, so xs, ys :: Signal a ⇒ [a].
-- Define (c, sum) = rippleAdd zero (zip xs ys);
-- thus c :: a is the carry output and ss :: [a] is the sum word. Then:
-- bitValue c * (2 ^ k) + wordValue ss = wordValue xs + wordValue ys.
-- |
-- >>> mscanr fullAdd True [(True,True)]
-- (True,[True])
-- |
-- >>> mscanr fullAdd True [(True,True),(True,True)]
-- (True,[True,True])
mscanr :: ((Bool, Bool) -> Bool -> (Bool, Bool)) -> Bool -> [(Bool, Bool)] -> (Bool, [Bool])
mscanr f a [] = (a, [])
mscanr f a (x : xs) =
let (a', ys) = mscanr f a xs
(a'', y) = f x a'
in (a'', y : ys)
-- Example: addition of 23+11
-- 23 + 11
-- = 010111 (16+4+2+1 = 23)
-- + 001011 ( 8+2+1 = 11) with carry input = 0
-- = 100010 ( 32+2 = 34) with carry output = 0
-- | 23 + 11
-- >>> rippleAdd False [(False,False),(True,False),(False,True),(True,False),(True,True),(True,True)]
-- (False,[True,False,False,False,True,False])
rippleAdd :: Bool -> [(Bool, Bool)] -> (Bool, [Bool])
rippleAdd c zs = mscanr fullAdd c zs
-- Comparison of binary numbers is nearly as fundamental as adding them.
-- It is particularly interesting to consider how to implement a comparison circuit,
-- since this problem has some strong similarities and also some strong differences,
-- to the ripple carry adder.
-- halfCmp that compares two one-bit numbers x and y,
-- with the result of a Boolean in one position, either: (lt, eq, gt).
-- | Compare 0 to 1
-- >>> halfCmp (False, True)
-- (True,False,False)
-- | Compare 0 to 0
-- >>> halfCmp (False, False)
-- (False,True,False)
-- | Compare 1 to 1
-- >>> halfCmp (False, False)
-- (False,True,False)
-- | Compare 1 to 0
-- >>> halfCmp (True, False)
-- (False,False,True)
halfCmp :: (Bool, Bool) -> (Bool, Bool, Bool)
halfCmp (x, y) =
( and2 (inv x) y, -- x<y when x=0,y=1
inv (xor x y), -- x=y when x=0,y=0 or x=1,y=1
and2 x (inv y) -- x>y when x=1,y=0
)
-- Next, we'll build a ripple comparator that takes two words representing binary numbers
-- (the words must have the same size),
-- and returns a triple of three bits (lt, eq, gt)
-- that indicate the result of comparing x and y.
-- Just as you compare two numbers by looking first at the most significant digits,
-- a binary comparison is performed by moving from left to right through the word.
-- Initially we assume the two words are equal;
-- represent this by (lt, eq, gt) = (0, 1, 0).
-- If the next bit position has x = 1 and y = 0,
-- then we know that the final result must be (0, 0, 1),
-- regardless of any bits to the right;
-- conversely if x = 0 and y = 1,
-- then the final result must be (1, 0, 0),
-- regardless of the bit values to the right.
-- However, if x and y have the same value in this bit position,
-- then as far as we know the result is still (0, 1, 0),
-- but that result might be changed later.
-- |
-- >>> foldl fullCmp (False, True, False) [(False,False),(True,False),(False,True),(True,False),(True,True),(True,True)]
-- (False,False,True)
fullCmp :: (Bool, Bool, Bool) -> (Bool, Bool) -> (Bool, Bool, Bool)
fullCmp (lt, eq, gt) (x, y) =
( or2 lt (and3 eq (inv x) y), -- <
and2 eq (inv (xor x y)), -- =
or2 gt (and3 eq x (inv y)) -- >
)
-- | Compare 23 to 11:
-- >>> rippleCmp [(False,False),(True,False),(False,True),(True,False),(True,True),(True,True)]
rippleCmp :: [(Bool, Bool)] -> (Bool, Bool, Bool)
rippleCmp z = foldl fullCmp (False, True, False) z