{-# LANGUAGE OverloadedStrings #-}

module Clash.Primitives.Verification (checkBBF) where

import Data.Either


import qualified Control.Lens                    as Lens
import           Control.Monad.State             (State)
import           Data.List.Infinite              (Infinite(..), (...))
import           Data.Maybe                      (listToMaybe)
import           Data.Monoid                     (Ap(getAp))
import           Data.Text.Prettyprint.Doc.Extra (Doc)
import qualified Data.Text                       as Text
import           GHC.Stack                       (HasCallStack)

import           Clash.Annotations.Primitive     (HDL(..))
import           Clash.Backend
  (Backend, blockDecl, hdlKind)
import           Clash.Core.HasType
import           Clash.Core.Term                 (Term(Var), varToId)
import           Clash.Core.TermLiteral          (termToDataError)
import           Clash.Util                      (indexNote)
import           Clash.Netlist                   (mkExpr)
import           Clash.Netlist.Util              (stripVoid)
import qualified Clash.Netlist.Id                as Id
import           Clash.Netlist.Types
  (BlackBox(BBFunction), TemplateFunction(..), BlackBoxContext, Identifier,
   NetlistMonad, Declaration(Assignment, NetDecl), Usage(Cont),
   HWType(Bool, KnownDomain), NetlistId(..),
   DeclarationType(Concurrent), tcCache, bbInputs, Expr(Identifier))
import           Clash.Netlist.BlackBox.Types
  (BlackBoxFunction, BlackBoxMeta(..), TemplateKind(TDecl), RenderVoid(..),
   emptyBlackBoxMeta)

import           Clash.Verification.Internal
import           Clash.Verification.Pretty

checkBBF :: BlackBoxFunction
checkBBF :: BlackBoxFunction
checkBBF Bool
_isD Text
_primName [Either Term Type]
args [Type]
_ty =
  case Either String (Text, RenderAs, Property' (Maybe String, Term))
litArgs of
    Left String
err -> Either String (BlackBoxMeta, BlackBox)
-> NetlistMonad (Either String (BlackBoxMeta, BlackBox))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (String -> Either String (BlackBoxMeta, BlackBox)
forall a b. a -> Either a b
Left String
err)
    Right (Text
propName, RenderAs
renderAs, Property' (Maybe String, Term)
cvProperty0) -> do
      Property' (Identifier, [Declaration])
cvProperty1 <- ((Maybe String, Term) -> NetlistMonad (Identifier, [Declaration]))
-> Property' (Maybe String, Term)
-> NetlistMonad (Property' (Identifier, [Declaration]))
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Maybe String -> Term -> NetlistMonad (Identifier, [Declaration]))
-> (Maybe String, Term) -> NetlistMonad (Identifier, [Declaration])
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Maybe String -> Term -> NetlistMonad (Identifier, [Declaration])
bindMaybe) Property' (Maybe String, Term)
cvProperty0
      let decls :: [Declaration]
decls = ((Identifier, [Declaration]) -> [Declaration])
-> Property' (Identifier, [Declaration]) -> [Declaration]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap (Identifier, [Declaration]) -> [Declaration]
forall a b. (a, b) -> b
snd Property' (Identifier, [Declaration])
cvProperty1
          cvProperty2 :: Property' Identifier
cvProperty2 = ((Identifier, [Declaration]) -> Identifier)
-> Property' (Identifier, [Declaration]) -> Property' Identifier
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Identifier, [Declaration]) -> Identifier
forall a b. (a, b) -> a
fst Property' (Identifier, [Declaration])
cvProperty1
      Either String (BlackBoxMeta, BlackBox)
-> NetlistMonad (Either String (BlackBoxMeta, BlackBox))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((BlackBoxMeta, BlackBox) -> Either String (BlackBoxMeta, BlackBox)
forall a b. b -> Either a b
Right (BlackBoxMeta
meta, TemplateFunction -> BlackBox
bb ([Declaration]
-> (Expr, Identifier)
-> Text
-> RenderAs
-> Property' Identifier
-> TemplateFunction
checkTF [Declaration]
decls (Expr
clkExpr, Identifier
clkId) Text
propName RenderAs
renderAs Property' Identifier
cvProperty2)))
 where
  -- TODO: Improve error handling; currently errors don't indicate what
  -- TODO: blackbox generated them.
  Int
_knownDomainArg
    :< Int
clkArg
    :< Int
_rstArg
    :< Int
propNameArg
    :< Int
renderAsArg
    :< Int
propArg
    :< Infinite Int
_ = ((Int
0 :: Int)Int -> Infinite Int
forall a. Enum a => a -> Infinite a
...)
  (HasCallStack => Id -> Identifier
Id -> Identifier
Id.unsafeFromCoreId -> Identifier
clkId) = Term -> Id
varToId (String -> [Term] -> Int -> Term
forall a. HasCallStack => String -> [a] -> Int -> a
indexNote String
"clk" ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
lefts [Either Term Type]
args) Int
clkArg)
  clkExpr :: Expr
clkExpr = Identifier -> Maybe Modifier -> Expr
Identifier Identifier
clkId Maybe Modifier
forall a. Maybe a
Nothing

  litArgs :: Either String (Text, RenderAs, Property' (Maybe String, Term))
litArgs = do
    Text
propName <- Term -> Either String Text
forall a. TermLiteral a => Term -> Either String a
termToDataError (String -> [Term] -> Int -> Term
forall a. HasCallStack => String -> [a] -> Int -> a
indexNote String
"propName" ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
lefts [Either Term Type]
args) Int
propNameArg)
    RenderAs
renderAs <- Term -> Either String RenderAs
forall a. TermLiteral a => Term -> Either String a
termToDataError (String -> [Term] -> Int -> Term
forall a. HasCallStack => String -> [a] -> Int -> a
indexNote String
"renderAs" ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
lefts [Either Term Type]
args) Int
renderAsArg)
    Property' (Maybe String, Term)
cvProperty <- Term -> Either String (Property' (Maybe String, Term))
forall a. TermLiteral a => Term -> Either String a
termToDataError (String -> [Term] -> Int -> Term
forall a. HasCallStack => String -> [a] -> Int -> a
indexNote String
"propArg" ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
lefts [Either Term Type]
args) Int
propArg)
    (Text, RenderAs, Property' (Maybe String, Term))
-> Either String (Text, RenderAs, Property' (Maybe String, Term))
forall a b. b -> Either a b
Right (Text
propName, RenderAs
renderAs, Property' (Maybe String, Term)
cvProperty)

  bb :: TemplateFunction -> BlackBox
bb = String -> Int -> TemplateFunction -> BlackBox
BBFunction String
"Clash.Primitives.Verification.checkTF" Int
0
  meta :: BlackBoxMeta
meta = BlackBoxMeta
emptyBlackBoxMeta {bbKind :: TemplateKind
bbKind=TemplateKind
TDecl, bbRenderVoid :: RenderVoid
bbRenderVoid=RenderVoid
RenderVoid}

  bindMaybe
    :: Maybe String
    -- ^ Hint for new identifier
    -> Term
    -- ^ Term to bind. Does not bind if it's already a reference to a signal
    -> NetlistMonad (Identifier, [Declaration])
    -- ^ ([new] reference to signal, [declarations need to get it in scope])
  bindMaybe :: Maybe String -> Term -> NetlistMonad (Identifier, [Declaration])
bindMaybe Maybe String
_ (Var Id
vId) = (Identifier, [Declaration])
-> NetlistMonad (Identifier, [Declaration])
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (HasCallStack => Id -> Identifier
Id -> Identifier
Id.unsafeFromCoreId Id
vId, [])
  bindMaybe Maybe String
Nothing Term
t = Maybe String -> Term -> NetlistMonad (Identifier, [Declaration])
bindMaybe (String -> Maybe String
forall a. a -> Maybe a
Just String
"s") Term
t
  bindMaybe (Just String
nm) Term
t = do
    TyConMap
tcm <- Getting TyConMap NetlistEnv TyConMap -> NetlistMonad TyConMap
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
Lens.view Getting TyConMap NetlistEnv TyConMap
Getter NetlistEnv TyConMap
tcCache
    Identifier
newId <- Text -> NetlistMonad Identifier
forall (m :: Type -> Type).
(HasCallStack, IdentifierSetMonad m) =>
Text -> m Identifier
Id.make (String -> Text
Text.pack String
nm)
    (Expr
expr0, [Declaration]
decls) <- HasCallStack =>
Bool
-> DeclarationType
-> NetlistId
-> Term
-> NetlistMonad (Expr, [Declaration])
Bool
-> DeclarationType
-> NetlistId
-> Term
-> NetlistMonad (Expr, [Declaration])
mkExpr Bool
False DeclarationType
Concurrent (Identifier -> Type -> NetlistId
NetlistId Identifier
newId (TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
t)) Term
t
    (Identifier, [Declaration])
-> NetlistMonad (Identifier, [Declaration])
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure
      ( Identifier
newId
      , [Declaration]
decls [Declaration] -> [Declaration] -> [Declaration]
forall a. [a] -> [a] -> [a]
++ [HWType -> Identifier -> Declaration
sigDecl HWType
Bool Identifier
newId, Identifier -> Usage -> Expr -> Declaration
Assignment Identifier
newId Usage
Cont Expr
expr0] )

  -- Simple wire without comment
  sigDecl :: HWType -> Identifier -> Declaration
  sigDecl :: HWType -> Identifier -> Declaration
sigDecl HWType
typ Identifier
nm = Maybe Text -> Identifier -> HWType -> Declaration
NetDecl Maybe Text
forall a. Maybe a
Nothing Identifier
nm HWType
typ

checkTF
  :: [Declaration]
  -> (Expr, Identifier)
  -> Text.Text
  -> RenderAs
  -> Property' Identifier
  -> TemplateFunction
checkTF :: [Declaration]
-> (Expr, Identifier)
-> Text
-> RenderAs
-> Property' Identifier
-> TemplateFunction
checkTF [Declaration]
decls (Expr, Identifier)
clk Text
propName RenderAs
renderAs Property' Identifier
prop =
  [Int]
-> (BlackBoxContext -> Bool)
-> (forall s. Backend s => BlackBoxContext -> State s Doc)
-> TemplateFunction
TemplateFunction [] (Bool -> BlackBoxContext -> Bool
forall a b. a -> b -> a
const Bool
True) ([Declaration]
-> (Expr, Identifier)
-> Text
-> RenderAs
-> Property' Identifier
-> BlackBoxContext
-> State s Doc
forall s.
(HasCallStack, Backend s) =>
[Declaration]
-> (Expr, Identifier)
-> Text
-> RenderAs
-> Property' Identifier
-> BlackBoxContext
-> State s Doc
checkTF' [Declaration]
decls (Expr, Identifier)
clk Text
propName RenderAs
renderAs Property' Identifier
prop)

checkTF'
  :: forall s
   . (HasCallStack, Backend s)
  => [Declaration]
  -- ^ Extra decls needed
  -> (Expr, Identifier)
  -- ^ Clock
  -> Text.Text
  -- ^ Prop name
  -> RenderAs
  -> Property' Identifier
  -> BlackBoxContext
  -> State s Doc
checkTF' :: [Declaration]
-> (Expr, Identifier)
-> Text
-> RenderAs
-> Property' Identifier
-> BlackBoxContext
-> State s Doc
checkTF' [Declaration]
decls (Expr
clk, Identifier
clkId) Text
propName RenderAs
renderAs Property' Identifier
prop BlackBoxContext
bbCtx = do
  Identifier
blockName <- Text -> StateT s Identity Identifier
forall (m :: Type -> Type).
(HasCallStack, IdentifierSetMonad m) =>
Text -> m Identifier
Id.makeBasic (Text
propName Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_block")
  Ap (State s) Doc -> State s Doc
forall k (f :: k -> Type) (a :: k). Ap f a -> f a
getAp (Identifier -> [Declaration] -> Ap (State s) Doc
forall state.
Backend state =>
Identifier -> [Declaration] -> Ap (State state) Doc
blockDecl Identifier
blockName (Declaration
renderedPslProperty Declaration -> [Declaration] -> [Declaration]
forall a. a -> [a] -> [a]
: [Declaration]
decls))

 where
  hdl :: HDL
hdl = s -> HDL
forall state. Backend state => state -> HDL
hdlKind (s
forall a. HasCallStack => a
undefined :: s)

  edge :: ActiveEdge
edge =
    case BlackBoxContext -> [(Expr, HWType, Bool)]
bbInputs BlackBoxContext
bbCtx of
      (Expr
_, HWType -> HWType
stripVoid -> KnownDomain Text
_nm Integer
_period ActiveEdge
e ResetKind
_rst InitBehavior
_init ResetPolarity
_polarity, Bool
_):[(Expr, HWType, Bool)]
_ -> ActiveEdge
e
      [(Expr, HWType, Bool)]
_ -> String -> ActiveEdge
forall a. HasCallStack => String -> a
error (String -> ActiveEdge) -> String -> ActiveEdge
forall a b. (a -> b) -> a -> b
$ String
"Unexpected first argument: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe (Expr, HWType, Bool) -> String
forall a. Show a => a -> String
show ([(Expr, HWType, Bool)] -> Maybe (Expr, HWType, Bool)
forall a. [a] -> Maybe a
listToMaybe (BlackBoxContext -> [(Expr, HWType, Bool)]
bbInputs BlackBoxContext
bbCtx))

  renderedPslProperty :: Declaration
renderedPslProperty = case RenderAs
renderAs of
    RenderAs
PSL          -> Declaration
psl
    RenderAs
SVA          -> Declaration
sva
    RenderAs
AutoRenderAs -> case HDL
hdl of
      HDL
SystemVerilog -> Declaration
sva
      HDL
_             -> Declaration
psl
    RenderAs
YosysFormal -> case HDL
hdl of
      HDL
VHDL -> Declaration
psl
      HDL
_    -> Declaration
ysva

   where
    sva :: Declaration
sva = Text -> Text -> ActiveEdge -> Property' Text -> Declaration
pprSvaProperty Text
propName (Identifier -> Text
Id.toText Identifier
clkId) ActiveEdge
edge ((Identifier -> Text) -> Property' Identifier -> Property' Text
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Identifier -> Text
Id.toText Property' Identifier
prop)
    ysva :: Declaration
ysva = Text -> Expr -> ActiveEdge -> Property' Text -> Declaration
pprYosysSvaProperty Text
propName Expr
clk ActiveEdge
edge ((Identifier -> Text) -> Property' Identifier -> Property' Text
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Identifier -> Text
Id.toText Property' Identifier
prop)
    psl :: Declaration
psl = HDL -> Text -> Text -> ActiveEdge -> Property' Text -> Declaration
pprPslProperty HDL
hdl Text
propName (Identifier -> Text
Id.toText Identifier
clkId) ActiveEdge
edge ((Identifier -> Text) -> Property' Identifier -> Property' Text
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Identifier -> Text
Id.toText Property' Identifier
prop)