Wired-0.1: Lava/Model.hs
{-# OPTIONS_GHC -fno-warn-missing-fields #-}
module Lava.Model where
import Control.Monad.Writer
import Control.Monad.State
import Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Hardware.Internal
import qualified Lava2000 as L
data Signal
= Constant ConstId
| PrimInpSig PrimInpId
| CellSig CellId Pin
-- The pins of a cell are numbered consequtively from 0, starting
-- with the outputs.
deriving (Eq, Show, Ord)
data Declaration lib
= PrimInput PrimInpId Name
| Cell CellId lib [Signal]
| Label Tag Signal
deriving (Eq, Show)
data DesignDB lib = DesignDB
{ inputDB :: Map PrimInpId Name
, cellDB :: Map CellId (lib,[Signal])
, fanoutDB :: Map Signal [Signal]
, tagDB :: Map Tag [Signal]
}
deriving (Eq, Show)
-- fanoutDB and tagDB need only be defined if the value is non-empty. Use
-- together with totalLookup. A database is valid if the corresponding list
-- of declarations is (*** it should be possible to reconstruct a list of
-- declarations from a database to make this well-defined).
class CellLibrary lib
where
numConsts :: TypeOf lib -> ConstId
-- Only used for specifying valid circuits (see prop_validDecls).
numIns :: lib -> Int
numOuts :: lib -> Int
-- Number of inputs/outputs of the given cell
pinName :: lib -> Pin -> Name
pinId :: lib -> Name -> Pin
isFlop :: lib -> Bool
-- Tells whether or not the given cell is a flipflop.
lava2000Interp :: Interpretation lib (L.Signal Bool)
-- Requirements:
--
-- * The range of numConsts, numIns and numOuts is a subset of [0..]
--
-- * The domain of (pinName c) is [0 .. numOuts c + numIns c - 1]
--
-- * (pinName c) is one-to-one, and its inverse is (pinId c).
--
-- * lava2000Interp is a valid interpretation (see definition of
-- Interpretation). Moreover, the propagator method should constrain all
-- and only all outputs of each cell.
libraryConstants :: CellLibrary lib => TypeOf lib -> [Signal]
libraryConstants t = map Constant [0 .. numConsts t-1]
cellInputs :: CellLibrary lib => CellId -> lib -> [Signal]
cellInputs cid ct = map (CellSig cid) [no .. no+ni]
where
no = icast (numOuts ct)
ni = icast (numIns ct)
cellOutputs :: CellLibrary lib => CellId -> lib -> [Signal]
cellOutputs cid ct = map (CellSig cid) [0 .. icast (numOuts ct) - 1]
prop_uniquePrimInputs decls = iids == nub iids
where
iids = [iid | PrimInput iid _ <- decls]
-- Each PrimInput has a uniqe PrimInpId.
prop_uniqueCells decls = cids == nub cids
where
cids = [cid | Cell cid _ _ <- decls]
-- Each Cell has a uniqe CellId.
prop_correctCellInputs decls =
and [numIns ct == length ss | Cell _ ct ss <- decls]
-- Each Cell has the correct number of inputs.
prop_validSignals :: forall lib . CellLibrary lib => [Declaration lib] -> Bool
prop_validSignals decls = all (`elem` validSigs) referred
where
primInps = [PrimInpSig iid | PrimInput iid _ <- decls]
cellOuts = [s | Cell cid ct _ <- decls, s <- cellOutputs cid ct]
validSigs = libraryConstants (T::TypeOf lib) ++ primInps ++ cellOuts
referred
= concat [ss | Cell _ _ ss <- decls]
++ [s | Label _ s <- decls]
-- All signals referred to in the declarations
-- Checks that all signals referred to by a Cell or Label are valid. The valid
-- signals are the constants defined by the library, the declared primary
-- inputs and the *outputs* of declared cells. It is not allowed to refer to
-- cell inputs.
prop_validDecls :: CellLibrary lib => [Declaration lib] -> Bool
prop_validDecls decls
= prop_uniquePrimInputs decls
&& prop_uniqueCells decls
&& prop_correctCellInputs decls -- Correct number of inputs for each cell
&& prop_validSignals decls -- No reference to invalid signals
-- A circuit is always defined in the presence of a cell library. This
-- property defines what it means for a list of declarations to be valid with
-- respect to a cell library.
--
-- The properties should be fulfilled as long as the requirements of the
-- CellLibrary class are met and all signals are created using the methods:
-- libraryConstants, input, cell, and label.
--
-- The only thing that can go wrong is if the number of inputs/outputs
-- demanded by the type of a cell is different from what is specified by
-- numIns/numOuts. Difference in the inputs won't be checked at all (and the
-- only place where it might matter is in the propagator method of an
-- interpretation). However, difference in the outputs is checked for by
-- fromListFP (but the error is non-informative).
newtype Lava lib a = Lava
{ unLava :: WriterT [Declaration lib] (State (PrimInpId,CellId)) a }
deriving (Monad, MonadFix)
runLava :: CellLibrary lib => Lava lib a -> (a, DesignDB lib)
runLava (Lava lava) = (a, makeDesignDB decls)
where
((a,decls),_) = runState (runWriterT lava) (0,0)
fanouts decls = Map.fromListWith (++) $ concat
[ zip ins (map return $ cellInputs cid ct) | Cell cid ct ins <- decls ]
makeDesignDB decls = DesignDB iDB cDB (fanouts decls) tDB
where
iDB = Map.fromList [(iid,nm) | PrimInput iid nm <- decls]
cDB = Map.fromList [(cid,(ct,ins)) | Cell cid ct ins <- decls]
tDB = Map.fromListWith (++) [(tag,[sig]) | Label tag sig <- decls]
class (Monad m, CellLibrary lib) => MonadLava lib m | m -> lib
where
newPrimInpId :: m PrimInpId
newCellId :: m CellId
declare :: Declaration lib -> m ()
listenDecls :: m a -> m (a, [Declaration lib])
instance CellLibrary lib => MonadLava lib (Lava lib)
where
newPrimInpId = Lava $ do
(iid,cid) <- get
put (succ iid, cid)
return iid
newCellId = Lava $ do
(iid,cid) <- get
put (iid, succ cid)
return cid
declare = Lava . tell . return
listenDecls = Lava . listen . unLava
inputSig :: MonadLava lib m => Name -> m Signal
inputSig nm = do
iid <- newPrimInpId
declare $ PrimInput iid nm
return (PrimInpSig iid)
-- Declare a primary input
cellList :: MonadLava lib m => lib -> [Signal] -> m [Signal]
cellList ct ins = do
cid <- newCellId
declare $ Cell cid ct ins
return (cellOutputs cid ct)
-- Declare a cell
labelSig :: MonadLava lib m => Tag -> Signal -> m Signal
labelSig tag sig = declare (Label tag sig) >> return sig
-- Declare a label; only side-effect important
data Interpretation lib x = Interp
{ constants :: [x]
, defaultVal :: x
, accumulator :: x -> x -> x
, propagator :: lib -> ([x] -> [Maybe x])
-- The value of pin p appears at position p in the lists (i.e.
-- outputs first).
}
-- Requirements:
--
-- * The length of the constant list is (numConsts (T::TypeOf lib)).
--
-- * The number of elements accepted/returned by the propagator is
-- (numOuts cell + numIns cell).
type InterpDesignDB lib x = (DesignDB lib, Map Signal x)
lookupTag :: Tag -> InterpDesignDB lib x -> [x]
lookupTag tag (db,sigMap) = map (sigMap Map.!) (tag `totalLookup` tagDB db)
depthInterp :: forall lib . CellLibrary lib => Interpretation lib Int
depthInterp = Interp
{ constants = replicate (icast $ numConsts (T::TypeOf lib)) 0
, propagator = prop
}
where
prop ct vals
| isFlop ct = replicate no (Just 0) ++ ins
| otherwise = replicate no (Just (d+1)) ++ ins
where
ni = numIns ct
no = numOuts ct
ins = replicate ni Nothing
d = maximum (drop no vals)