Wired-0.1: Lava/Internal.hs

module Lava.Internal
  ( module Lava.Model
  , module Lava.Patterns
  , module Lava.Loop
  , module Lava.Port
  , module Lava.Interpret
  , input
  , inputList
  , cell
  , label
  , toLava2000
  , simulateSeq
  , simulate
  , verify
  , depth
  , fanout
  , size
  ) where



import Control.Monad
import qualified Data.Foldable as Fold
import qualified Data.Map as Map

import Data.Hardware.Internal
import Lava.Model
import Lava.Patterns
import Lava.Loop
import Lava.Port
import Lava.Interpret

import qualified Lava2000 as L
import qualified Lava2000.Ref as L



input :: forall lib m p . (MonadLava lib m, PortFixed p Signal) => Name -> m p
input nm = liftM fromListFP $ replicateM (lengthFP (T::TypeOf p)) (inputSig nm)
  -- Declare a primary input

inputList :: (MonadLava lib m, PortFixed p Signal) => Int -> Name -> m [p]
inputList n nm = replicateM n $ input nm



cell
    :: forall m lib pi po
     . ( MonadLava lib m
       , PortFixed pi Signal
       , PortFixed po Signal
       , CellLibrary lib
       )
    => lib -> pi -> m po

cell cid pi = liftM fromListFP $ cellList cid ins
  where
    ins = Fold.toList $ port pi
  -- Declare a cell



label :: (MonadLava lib m, PortStruct p Signal t) => Tag -> p -> m p
label tag = mapPortM (labelSig tag)
  -- Declare a label; only side-effect important.



toLava2000
    :: ( CellLibrary lib
       , PortStruct pli (L.Signal Bool) ti
       , PortStruct psi Signal          ti
       , PortStruct pso Signal          to
       , PortStruct plo (L.Signal Bool) to
       )
    => (psi -> Lava lib pso)
    -> (pli -> plo)

toLava2000 circ = fst . interpretFunc lava2000Interp circ



simulateSeq
    :: ( CellLibrary lib
       , PortStruct pni Int    ti
       , PortStruct psi Signal ti
       , PortStruct pso Signal to
       , PortStruct pno Int    to
       )
    => (psi -> Lava lib pso)
    -> ([pni] -> [pno])

simulateSeq circ
    = map (unport . fmap sigToInt)
    . L.simulateSeq circP
    . map (fmap intToSig . port)
  where
    circP = fst . interpretFuncP lava2000Interp (liftM port . circ . unport)

    intToSig 0 = L.low
    intToSig 1 = L.high
    intToSig _ = error "Only values 0 and 1 allowed"

    sigToInt (L.Signal (L.Symbol r)) = case L.deref r of
        L.Bool False -> 0
        L.Bool True  -> 1



simulate
    :: ( CellLibrary lib
       , PortStruct pni Int    ti
       , PortStruct psi Signal ti
       , PortStruct pso Signal to
       , PortStruct pno Int    to
       )
    => (psi -> Lava lib pso)
    -> (pni -> pno)

simulate circ = head . simulateSeq circ . return



verify
    :: forall lib ps
     . (CellLibrary lib, PortFixed ps Signal)
    => (ps -> Lava lib Signal) -> IO ()

verify circ = L.smv (L.forAll (L.list n) circP) >> return ()
  where
    n = lengthFP (T::TypeOf ps)

    circP = toLava2000 (circ . fromListFP)



depth :: (CellLibrary lib, PortStruct ps Signal t, PortStruct pd Int t) =>
    Lava lib ps -> (pd, InterpDesignDB lib Int)
depth circ
    | hasLoopDB True db = error "depth: Combinational feedback loop"
    | otherwise         = pd_idb
  where
    pd_idb@(_,(db,_)) = interpret depthInterp circ

fanout :: CellLibrary lib => Lava lib a -> InterpDesignDB lib Int
fanout circ = (db, fmap length $ fanoutDB db)
  where
    (_,db) = runLava circ

size :: CellLibrary lib => Lava lib p -> Int
size = length . Map.toList . cellDB . snd . runLava