{-# LANGUAGE OverloadedStrings #-}

module Clash.Primitives.Verification (checkBBF) where

import Data.Either


import qualified Control.Lens                    as Lens
import           Control.Monad.State             (State)
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, id2identifier)
import qualified Clash.Netlist.Id                as Id
import           Clash.Netlist.Types
  (BlackBox(BBFunction), TemplateFunction(..), BlackBoxContext, Identifier,
   NetlistMonad, Declaration(Assignment, NetDecl'),
   HWType(Bool, KnownDomain), WireOrReg(Wire), 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.
  clk :: Term
clk = 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
1
  clkExpr :: Expr
clkExpr = Identifier -> Maybe Modifier -> Expr
Identifier Identifier
clkId Maybe Modifier
forall a. Maybe a
Nothing
  (Id -> Identifier
id2identifier -> Identifier
clkId) = Term -> Id
varToId Term
clk
  (Id -> Identifier
id2identifier -> Identifier
_clkId) = Term -> Id
varToId (String -> [Term] -> Int -> Term
forall a. HasCallStack => String -> [a] -> Int -> a
indexNote String
"rst" ([Either Term Type] -> [Term]
forall a b. [Either a b] -> [a]
lefts [Either Term Type]
args) Int
2)

  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
3)
    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
4)
    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
5)
    (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 (Id -> Identifier
id2identifier 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 -> Expr -> Declaration
Assignment Identifier
newId Expr
expr0] )

  -- Simple wire without comment
  sigDecl :: HWType -> Identifier -> Declaration
  sigDecl :: HWType -> Identifier -> Declaration
sigDecl HWType
typ Identifier
nm = Maybe Text
-> WireOrReg
-> Identifier
-> Either Text HWType
-> Maybe Expr
-> Declaration
NetDecl' Maybe Text
forall a. Maybe a
Nothing WireOrReg
Wire Identifier
nm (HWType -> Either Text HWType
forall a b. b -> Either a b
Right HWType
typ) Maybe Expr
forall a. Maybe a
Nothing

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 [(Expr, HWType, Bool)] -> (Expr, HWType, Bool)
forall a. [a] -> a
head (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
_) -> 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]
++ (Expr, HWType, Bool) -> String
forall a. Show a => a -> String
show ([(Expr, HWType, Bool)] -> (Expr, HWType, Bool)
forall a. [a] -> a
head (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)