{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE OverloadedStrings #-}

module Clash.Primitives.Verification (checkBBF) where

import Data.Either


import qualified Control.Lens                    as Lens
import           Control.Monad.State             (State)
import           Data.Text.Prettyprint.Doc.Extra (Doc)
import qualified Data.Text                       as Text
import           Data.Semigroup.Monad            (getMon)
import           GHC.Stack                       (HasCallStack)

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

import           Clash.Verification.Internal
import           Clash.Verification.PrettyPrinters

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]
-> Identifier
-> Text
-> RenderAs
-> Property' Identifier
-> TemplateFunction
checkTF [Declaration]
decls Identifier
clkId Text
propName RenderAs
renderAs Property' Identifier
cvProperty2)))
 where
  -- TODO: Improve error handling; currently errors don't indicate what
  -- TODO: blackbox generated them.
  (Var (Id -> Identifier
id2identifier -> Identifier
clkId)) = 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
  (Var (Id -> Identifier
id2identifier -> Identifier
_clkId)) = 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 NetlistState TyConMap -> NetlistMonad TyConMap
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
Lens.use Getting TyConMap NetlistState TyConMap
Lens' NetlistState 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
termType 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]
  -> Identifier
  -> Text.Text
  -> RenderAs
  -> Property' Identifier
  -> TemplateFunction
checkTF :: [Declaration]
-> Identifier
-> Text
-> RenderAs
-> Property' Identifier
-> TemplateFunction
checkTF [Declaration]
decls Identifier
clkId 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]
-> Identifier
-> Text
-> RenderAs
-> Property' Identifier
-> BlackBoxContext
-> State s Doc
forall s.
(HasCallStack, Backend s) =>
[Declaration]
-> Identifier
-> Text
-> RenderAs
-> Property' Identifier
-> BlackBoxContext
-> State s Doc
checkTF' [Declaration]
decls Identifier
clkId Text
propName RenderAs
renderAs Property' Identifier
prop)

checkTF'
  :: forall s
   . (HasCallStack, Backend s)
  => [Declaration]
  -- ^ Extra decls needed
  -> Identifier
  -- ^ Clock
  -> Text.Text
  -- ^ Prop name
  -> RenderAs
  -> Property' Identifier
  -> BlackBoxContext
  -> State s Doc
checkTF' :: [Declaration]
-> Identifier
-> Text
-> RenderAs
-> Property' Identifier
-> BlackBoxContext
-> State s Doc
checkTF' [Declaration]
decls 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")
  Mon (State s) Doc -> State s Doc
forall (f :: Type -> Type) m. Mon f m -> f m
getMon (Identifier -> [Declaration] -> Mon (State s) Doc
forall state.
Backend state =>
Identifier -> [Declaration] -> Mon (State state) Doc
blockDecl Identifier
blockName (Text -> Declaration
TickDecl Text
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 :: Text
renderedPslProperty
    | RenderAs
renderAs RenderAs -> RenderAs -> Bool
forall a. Eq a => a -> a -> Bool
== RenderAs
SVA Bool -> Bool -> Bool
|| HDL
hdl HDL -> HDL -> Bool
forall a. Eq a => a -> a -> Bool
== HDL
SystemVerilog = Text
sva
    | Bool
otherwise = Text
psl
   where
    sva :: Text
sva = Text -> Text -> ActiveEdge -> Property' Text -> Text
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)
    psl :: Text
psl = HDL -> Text -> Text -> ActiveEdge -> Property' Text -> Text
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)