language.hs

Cores are generated from Confluence a modern logic design language. Confluence is a simple, yet high

-- | The Atom language.

module Language.Atom.Language
  (
    module Language.Atom.Terms
  -- * Primary Language Containers
  , System
  , Action
  -- * Namespace Control
  , scope
  , scopeEnabled
  , scopePeriodic
  -- * System Sample Period
  , samplePeriod
  -- * Compile-time and Runtime Assertions
  , assert
  -- * Rule Declarations and Operations
  , rule
  , rules
  , sequenceActions
  , loopActions
  -- * Action Directives
  , when
  , (<==)
  --, display
  --, finish
  , incrInt
  , decrInt
  -- ** Performance Constraints
  , priority
  , alwaysActiveWhenEnabled
  -- * Variable Declarations
  , bool
  , int
  , float
  , double
  -- * Variable Declarations
  , input

  , Name
  , lift
  , liftIO
  ) where

import Control.Monad.State hiding (when, join)
import Control.Monad.Trans

import Language.Atom.Elaboration hiding (System, Action)
import qualified Language.Atom.Elaboration as E
import Language.Atom.Terms
import Language.Atom.Utils

infixr 1 <==

-- | A System captures various declarations including inputs, variables, rules, and assertions.
type System = E.System

-- | An Action captures rule behavior including enabling conditions (eg. 'when') and variable updates (eg, '<==').
type Action = E.Action

-- | Creates a new namespace.
scope :: Name -> System a -> System a
scope name system = scopeEnabled name true system

-- | Creates a new namespace with an enabling condition.
scopeEnabled :: Name -> Term Bool -> System a -> System a
scopeEnabled name enable system = do
  sys <- get
  put sys
    { sysPath    = name : sysPath sys
    , sysEnable  = sysEnable sys &&. enable
    , sysContent = []
    }
  a <- system
  sys' <- get
  put sys'
    { sysPath    = sysPath sys
    , sysEnable  = sysEnable sys
    , sysContent = SystemScope name (sysContent sys') : sysContent sys
    }
  return a

-- | Creates a new namespace with a periodic enabling condition.
scopePeriodic :: Name -> Int -> Int -> System a -> System a
scopePeriodic name period offset system = if period < 0 || offset < 0 then error ("Invalid period of offset for periodic scope: " ++ name) else do
  clock <- int (name ++ "_clock") offset
  rule (name ++ "_clock_tick") $ do
    alwaysActiveWhenEnabled
    clock <== mux (value clock ==. 0) (intC $ period - 1) (value clock - 1)
  sys <- get
  put sys { sysPeriod = sysPeriod sys * fromIntegral period }
  a <- scopeEnabled name (value clock ==. 0) system
  sys' <- get
  put sys' { sysPeriod = sysPeriod sys }
  return a

-- | Returns the sample period (sec) of the current 'System' scope.
--   The sample period is altered with system scopes created with 'scopePeriodic'.
samplePeriod :: System Double
samplePeriod = do
  sys <- get
  return $ sysPeriod sys

class Assert a where
  -- | Asserts a property is always true.  Supports compile-time assertions (ie. Bool)
  --   and runtime assertsion (ie. Term Bool).
  assert :: Name -> a -> System ()

instance Assert Bool where
  assert name a = do
    sys <- get
    if not a
      then error $ "ASSERT ERROR: " ++ join (reverse (name : sysPath sys)) "."
      else return ()

instance Assert (Term Bool) where
  assert name a = do
    sys <- get
    let t = (reverse (name : sysPath sys), a)
    put sys
      { sysAsserts = t : sysAsserts sys
      , sysContent = SystemAssert name t : sysContent sys
      }

nextId :: System Int
nextId = do
  sys <- get
  put $ sys { sysNextId = sysNextId sys + 1 }
  return $ sysNextId sys

{-
-- | Addition.
(+.) :: Signal -> Signal -> Signal
(+.) a b | width a /= width b = error "(+.): Signals do not have same width."
(+.) a b = x where (x,_) = fullAdd (bits a) (bits b)

fullAdd :: [Signal] -> [Signal] -> (Signal,Signal)
fullAdd (a:as) (b:bs) = ((a ^. b ^. c) ++ x, ((a ^. b) &. c) |. (a &. b)) where (x,c) = fullAdd as bs
fullAdd _ _ = ([],false)

-- | Subtraction.
(-.) :: Signal -> Signal -> Signal
(-.) a b | width a /= width b = error "(-.): Signals do not have same width."
(-.) a b = x where (x,_) = fullSub (bits a) (bits b)

fullSub :: [Signal] -> [Signal] -> (Signal,Signal)
fullSub (a:as) (b:bs) = ((a ^. b ^. c) ++ x, (inv (a ^. b) &. c) |. (inv a &. b)) where (x,c) = fullSub as bs
fullSub _ _ = ([],false)
-}

{-
-- | Logical XOR.
(^^.) :: Term Bool -> Term Bool -> Term Bool
(^^.) a b = (a &&. inv b) ||. (inv a &&. b)

-- | Implication.
imply :: Term Bool -> Term Bool -> Term Bool
imply a b = inv a ||. b

-- | Equivalence.
equiv :: Term Bool -> Term Bool -> Term Bool
equiv a b = inv (a ^^. b)
-}

{-
-- | A 2-input mux.
--
-- > mux ctrl onHigh onLow  -- Verilog equivalent:  ctrl ? onHigh : onLow
--mux :: Signal -> Signal -> Signal -> Signal
--mux c _ _ | width c /= 1 = error "mux: Control signal is not a single bit."
--mux _ h l | width h /= width l = error "mux: Data do not have the same width."
--mux c h l = concatMap mux' $ zip (bits h) (bits l)
  --where
  --mux' (h,l) | h == l = h
  --mux' (h,l) = (c &. h) |. (inv c &. l)

-- | A tree of muxs to select data from a list of signals.
--muxs :: Signal -> [Signal] -> Signal
--muxs _ []  = error "muxs: Can not mux an empty list."
--muxs _ [s] = s
--muxs c _ | null c = error "muxs: Not enough control bits to select data."
--muxs c s = muxs (msbs c) (muxRow s)
  --where
  --muxRow :: [Signal] -> [Signal]
  --muxRow [] = []
  --muxRow [a] = [a]
  --muxRow (a:b:r) = mux (lsb c) b a : muxRow r 
-}

-- | Boolean variable declaration.
bool :: Name -> Bool -> System (Var Bool)
bool name init = do
  sys <- get
  let v = Var (reverse (name : sysPath sys)) init
      uv = UVarBool v
  put sys
    { sysVars = uv : sysVars sys
    , sysContent = SystemVar name uv : sysContent sys
    }
  return v

-- | Int variable declaration.
int :: Name -> Int -> System (Var Int)
int name init = do
  sys <- get
  let v = Var (reverse (name : sysPath sys)) init
      uv = UVarInt v
  put sys
    { sysVars = uv : sysVars sys
    , sysContent = SystemVar name uv : sysContent sys
    }
  return v

-- | Float variable declaration.
float :: Name -> Float -> System (Var Float)
float name init = do
  sys <- get
  let v = Var (reverse (name : sysPath sys)) init
      uv = UVarFloat v
  put sys
    { sysVars = uv : sysVars sys
    , sysContent = SystemVar name uv : sysContent sys
    }
  return v

-- | Double variable declaration.
double :: Name -> Double -> System (Var Double)
double name init = do
  sys <- get
  let v = Var (reverse (name : sysPath sys)) init
      uv = UVarDouble v
  put sys
    { sysVars = uv : sysVars sys
    , sysContent = SystemVar name uv : sysContent sys
    }
  return v

-- | Declare a primary input.  Use variable declarions without initial values.
--
--   > a <- input bool   "a"
--   > b <- input int    "b"
--   > c <- input float  "c"
--   > d <- input double "d"
--
input :: TermT a => (Name -> a -> System (Var a)) -> Name -> System (Term a)
input f name = do
  Var n _ <- f name zeroConst
  let input = Input n
  sys <- get
  put sys
    { sysVars = tail (sysVars sys)
    , sysIns  = uterm input : sysIns sys
    , sysContent = SystemInput name (uterm input) : tail (sysContent sys)
    }
  return input

-- | Increments a 'Var Int'.
incrInt :: Var Int -> Action ()
incrInt a = a <== value a + 1

-- | Decrements a 'Var Int'.
decrInt :: Var Int -> Action ()
decrInt a = a <== value a - 1


-- | Given a name and an 'Action', adds a transition rule to the 'System'.
--
-- > rule "ruleName" action
rule :: Name -> Action () -> System ()
rule name action = do
  i <- nextId
  act <- buildAction action
  sys <- get
  let rule = Rule { ruleUID = i
                  , ruleName = reverse (name : sysPath sys)
                  , ruleEnable = sysEnable sys &&. actEnable act
                  , ruleAssigns           = actAssigns           act
                  , ruleActiveWhenEnabled = actActiveWhenEnabled act
                  , ruleRelations         = actRelations         act
                  }
  put sys { sysRules = rule : sysRules sys }

-- | Defines a rule for each action.
rules :: Name -> [Action ()] -> System ()
rules name actions = mapM_ (\ (a,n) -> rule (name ++ show n) a) $ zip actions [0..]

class Assign a where
  -- | Assigns a 'Term' to a 'Var'.
  (<==) :: Var a -> Term a -> Action ()
instance Assign Bool where
  v <== t = do
    act <- get
    put $ act { actAssigns = (UVarBool v, UTermBool t) : actAssigns act }
instance Assign Int where
  v <== t = do
    act <- get
    put $ act { actAssigns = (UVarInt v, UTermInt t) : actAssigns act }
instance Assign Float where
  v <== t = do
    act <- get
    put $ act { actAssigns = (UVarFloat v, UTermFloat t) : actAssigns act }
instance Assign Double where
  v <== t = do
    act <- get
    put $ act { actAssigns = (UVarDouble v, UTermDouble t) : actAssigns act }

-- | Adds an enabling condition to an action.
when :: Term Bool -> Action ()
when c = do
  act <- get
  put $ act { actEnable = actEnable act &&. c }

-- | Sequences 'Action's in consecutive cycles.
sequenceActions :: Name -> [Action ()] -> System ()
sequenceActions name actions = do
  count <- int (name ++ "SequenceCount") 0
  mapM_ (sequenceRule count) $ zip [0..] actions
  where
  sequenceRule :: Var Int -> (Int, Action ()) -> System ()
  sequenceRule count (n,a) = rule (name ++ show n) $ do
      when (value count ==. intC n)
      a
      incrInt count
  
-- | Loops through a list of 'Action's in consecutive cycles.  Goes back to first once last is finished.
loopActions :: Name -> [Action ()] -> System ()
loopActions name actions = do
  count <- int (name ++ "LoopCount") 0
  mapM_ (loopRule count) $ zip [0..] actions
  where
  loopRule :: Var Int -> (Int, Action ()) -> System ()
  loopRule count (n,a) = rule (name ++ show n) $ do
      when (value count ==. intC n)
      a
      if n == length actions - 1
        then count <== 0
        else incrInt count

-- | Used to define priority between rules.  Returns two 'Action's.  The first should be called in the higher priority rule.
--   The second should be called in the lower priority rule.
--
-- > (higherPriority, lowerPriority) <- priority
priority :: System (Action (), Action ())
priority = do
  i <- nextId
  let higher = do
        act <- get
        put $ act { actRelations = Higher i : actRelations act }
      lower  = do
        act <- get
        put $ act { actRelations = Lower  i : actRelations act }
  return (higher,lower)

-- | Asserts the current 'Action' must always be active when enabled.
alwaysActiveWhenEnabled :: Action ()
alwaysActiveWhenEnabled = do
  act <- get
  put $ act { actActiveWhenEnabled = True }