{- Joel Kelso (c) University of Western Australia 2002 -}

module GateProcesses(
  invGate, andGate, orGate, dffGate
  ) where

--
-- Processes for modelling digital logic
--

import CircalLTS
import Compose hiding (compose)
import Structures
import Test

-- Level-based

invGate, andGate, orGate :: SDef
dffGate :: Bool -> SDef

invGate [a0,a1,x0,x1] = 
  relabel [("_a0",a0),("_a1",a1),("_x0",x0),("_x1",x1)]
  (SBSrc "Inv" ("Inv",sfs "_a0,_a1,_x0,_x1",
    [("Inv",sfs "_a0,_x1","Inv"),("Inv",sfs "_a1,_x0","Inv")]))

andGate [a0,a1,b0,b1,x0,x1] =
  relabel [("_a0",a0),("_a1",a1),("_b0",b0),("_b1",b1),
    ("_x0",x0),("_x1",x1)] (SBSrc "And" 
      ("And",sfs "_a0,_a1,_b0,_b1,_x0,_x1",
        [("And",sfs "_a0,_b0,_x0","And"),
         ("And",sfs "_a1,_b0,_x0","And"),
         ("And",sfs "_a0,_b1,_x0","And"),
         ("And",sfs "_a1,_b1,_x1","And")]))

orGate [a0,a1,b0,b1,x0,x1] = 
  relabel [("_a0",a0),("_a1",a1),("_b0",b0),("_b1",b1),
    ("_x0",x0),("_x1",x1)] (SBSrc "Or" 
      ("Or",sfs "_a0,_a1,_b0,_b1,_x0,_x1",
        [("Or",sfs "_a0,_b0,_x0","Or"),
         ("Or",sfs "_a1,_b0,_x1","Or"),
         ("Or",sfs "_a0,_b1,_x1","Or"),
         ("Or",sfs "_a1,_b1,_x1","Or")]))

dffGate startHigh [d0,d1,clk,q0,q1] = 
  relabel [("_d0",d0),("_d1",d1),("_clk",clk),
    ("_q0",q0),("_q1",q1)] (SBSrc startState
      ("DFF",sfs "_d0,_d1,_clk,_q0,_q1",
        [("D00",sfs "_d0,_q0","D00"),("D00",sfs "_d1,_q0","D10"),
         ("D00",sfs "_clk,_d0,_q0","D00"),
         ("D10",sfs "_d0,_q0","D00"),("D10",sfs "_d1,_q0","D10"),
         ("D10",sfs "_clk,_d1,_q0","D11"),
         ("D01",sfs "_d1,_q1","D11"),("D01",sfs "_d0,_q1","D01"),
         ("D01",sfs "_d0,_clk,_q1","D00"),
         ("D11",sfs "_d1,_q1","D11"), ("D11",sfs "_d0,_q1","D01"),
         ("D11",sfs "_d1,_clk,_q1","D11")])) where
           startState = if startHigh then "D11" else "D00"

--
-- Testing
--

-- AND and INV making NAND

t1 = andGate (afs "a0,a1,b0,b1,x0,x1")
t2 = invGate (afs "x0,x1,y0,y1")
t3 = abstract ["x0","x1"] (compose [t1,t2])

-- Clocked occilator thing from:
-- "Sequential Circuit Analysis with a BDD based Process Algebra System"
-- paper by George McCaskill and George Milne (p7 in my copy).

t4 = compose [
  dffGate False (afs "i0,i1,clk,o0,o1"),
  invGate (afs "i0,i1,o0,o1")]