--
-- MiniFlash Hardware Compiler
--
-- rewritten for the one week intensive course
-- "Hardware Description Languages for Synchronous 
-- Circuits", 4-8 September 2000 at Chalmers 
-- Technical University, Gothenburg, Sweden.
--
-- Gordon Pace & Koen Claessen
-- 24 August 2000
--
module MiniFlash where

import Lava

data MiniFlash = 
        Skip
      | Delay
      | Emit
      | MiniFlash :>> MiniFlash      -- sequential composition
      | IfThenElse (Signal Bool) (MiniFlash, MiniFlash)
      | While (Signal Bool) MiniFlash
      | MiniFlash :|| MiniFlash      -- fork .. join
  
type Circuit = Signal Bool -> (Signal Bool, Signal Bool)

compile :: MiniFlash -> Circuit

compile Skip start = (finish, low)
  where 
    finish = start
       
compile Delay start = (finish, low)
  where 
    finish = delay low start

compile Emit start = (finish, emit)
  where 
    finish = start
    emit = start

compile (p :>> q) start = (finish, emit)
  where 
    (middle, emit_p) = compile p start 
    (finish, emit_q) = compile q middle
    emit = or2(emit_p, emit_q)

compile (IfThenElse c (p, q)) start = (finish, emit)
  where 
    start_p = and2 (start, c)
    start_q = and2 (start, inv c)
    (finish_p, emit_p) = compile p start_p
    (finish_q, emit_q) = compile q start_q
    finish = or2 (finish_p, finish_q)
    emit = or2(emit_p, emit_q)

compile (While c p) start = (finish, emit)
  where 
    start' = or2 (start, finish_p)
    start_p = and2 (start', c)
    (finish_p, emit) = compile p start_p
    finish = and2 (start', inv c)

compile (p :|| q) start = (finish, emit)
  where 
    (finish_p, emit_p) = compile p start
    (finish_q, emit_q) = compile q start
    finish = synchronise (finish_p, finish_q)
    emit = or2 (emit_p, emit_q)

    synchronise (f1,f2) = f
      where
        both = and2 (f1, f2)
	one  = xor2 (f1, f2)
	wait = delay low (xor2 (one, wait))
	f    = or2 (both, and2 (wait, one))


emit1 :: MiniFlash
emit1 = Emit :>> Delay

forever :: MiniFlash -> MiniFlash
forever p = While high p

wait :: (Signal Bool) -> MiniFlash
wait c = While (inv c) Delay

repeatUntil :: (Signal Bool) -> MiniFlash -> MiniFlash
repeatUntil c p = p :>> (While (inv c) p)

-----------------
clock = 
  forever ( Delay :>> emit1 ) 

copy wire  = 
  forever (
    IfThenElse wire
      ( emit1
      , Delay
      )
  )
	    
mask wire = 
  forever ( 
    IfThenElse wire 
      ( emit1 :>> Delay
      , Delay
      )
  )

andFlash (w1,w2) = 
  forever (
        While (inv (and2(w1,w2))) Delay 
    :>> emit1
  )

orFlash (w1,w2) = 
  (copy w1) :|| (copy w2)

rising wire = 
  forever (
    wait (inv wire) :>>
    wait (wire)     :>>
    emit1
  )

falling wire = rising (inv wire)

edge wire = 
  (falling wire) :|| (rising wire)

sequenceFlash (a,b) = (wait a) :>> (wait b)

detonator (a,b) = (sequenceFlash (a,b)) :>> Emit

detonator2 (a,b,c,d) = 
  (   (sequenceFlash (a,b))
  :|| (sequenceFlash (c,d))
  ) :>> Emit

-- simulate the circuit for n time units
run c n = simulateCon (compile c) (high:[low | i<-[1..n-1]])