-- Use this file as a starting point. Replace "undefined" with proper
-- definitions and/or add your own definitions and comments as appropriate
-- (see the problem description).

import List
import Lava
import Lava.Patterns
import EFile11
import DrawPP11

--------------------------------------------------------------------------------
-- A1  Verify by exhaustive simulation that fullAdd1 really behaves as full adder.

verifyA1 = undefined


--------------------------------------------------------------------------------
-- A2  Formally verify that fullAdd1 really behaves as full adder.

verifyA2 = undefined -- use smv


--------------------------------------------------------------------------------
-- A3  Checking that the "dot" operator is associative

propAssoc (*) (a,b,c) = undefined

verifyA3 = undefined -- use smv

--------------------------------------------------------------------------------
-- A4 Check that adder0 and adder6 have the same behaviour

verifyA4 = undefined

--------------------------------------------------------------------------------
-- A5 Make an adder that is parameterised on the prefix pattern used 
-- in computing the carries

adder8 :: PP (Bit,Bit) -> [(Bit, Bit)] -> ([Bit], Bit)
adder8 pat = undefined

--------------------------------------------------------------------------------
-- A6  Implement and check the Brent Kung parallel prefix circuit

bKung :: PP a
bKung f [a] = [a]
bKung f as  = undefined

drawA3 = drawPP "bKung" bKung 32
checkA3 = undefined
depthA3 = undefined

--------------------------------------------------------------------------------
-- A7  Counting the number of operators in a prefix network

pattSize patt n = simulate ((patt (mkFan opCount)) ->- sum) (replicate n 0)

opCount :: (Signal Int, Signal Int) -> Signal Int
opCount (a,b) = undefined



--------------------------------------------------------------------------------
-- Generalised Brent Kung

-- A8 

bKungG :: Int -> PP a
bKungG k f as | length as <= k = undefined
bKungG k f as = undefined

-- A9 

bKungG1 :: Int -> PP a -> PP a
bKungG1 k pp f as | length as <= k = undefined
bKungG1 k pp f as= undefined

--------------------------------------------------------------------------------
-- A10   Finding sweet spot



--------------------------------------------------------------------------------
-- A11  Extra task for doctoral students and other students wishing to 
-- raise their grade


--------------------------------------------------------------------------------