content: {-|
  Copyright  :  (C) 2019, Myrtle Software Ltd
  License    :  BSD2 (see the file LICENSE)
  Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>
  
  Verification
  -}
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE FunctionalDependencies #-}
  {-# LANGUAGE QuasiQuotes #-}
  {-# LANGUAGE TemplateHaskell #-}
  
  module Clash.Verification.Internal
   ( AssertionResult(..)
   , Property(..)
   , Assertion(..)
   , RenderAs(..)
   , IsTemporal(..)
   , AssertionValue(toAssertionValue)
   , Assertion'(..)
   , Property'(..)
   , toTemporal
   , isTemporal
   , assertion
   )
   where
  
  import           Data.Text                      (Text)
  
  import Clash.Annotations.BitRepresentation
    (ConstrRepr(..), DataReprAnn(..), liftQ)
  import           Clash.Signal.Internal          (Domain, Signal)
  
  -- | Render target for HDL
  data RenderAs
    = PSL
    -- ^ Property Specification Language
    | SVA
    -- ^ SystemVerilog Assertions
    | AutoRenderAs
    -- ^ Use SVA for SystemVerilog, PSL for others
    | YosysFormal
    -- ^ Yosys Formal Extensions for Verilog and SystemVerilog. See:
    -- https://symbiyosys.readthedocs.io/en/latest/verilog.html and
    -- https://symbiyosys.readthedocs.io/en/latest/verific.html
    --
    -- Falls back to PSL for VHDL, however currently Clash's PSL syntax isn't
    -- suported by GHDL+SymbiYosys;
    deriving (Show, Eq)
  
  data IsTemporal
    = IsNotTemporal
    | IsTemporal
    deriving (Eq, Ord)
  
  -- | Internal version of 'Assertion'.
  data Assertion' a
    = CvPure a
    -- ^ (Bootstrapping) signal of booleans
    | CvToTemporal (Assertion' a)
    -- ^ Tag to force a non-temporal assertion to a temporal one
    | CvLit Bool
    -- ^ Boolean literal
  
    | CvNot (Assertion' a)
    -- ^ Logical not
    | CvAnd (Assertion' a) (Assertion' a)
    -- ^ Logical and
    | CvOr (Assertion' a) (Assertion' a)
    -- ^ Logical or
    | CvImplies (Assertion' a) (Assertion' a)
    -- ^ Logical implies
  
    | CvNext Word (Assertion' a)
    -- ^ Moves start point of assertion /n/ cycles forward
    | CvBefore (Assertion' a) (Assertion' a)
    -- ^ Before @CvBefore a b@ is the same as @CvAnd a (CvNext 1 b)@
    | CvTemporalImplies Word (Assertion' a) (Assertion' a)
    -- ^ Temporal implies @CvTemporalImplies n a b@:
    --
    --   n | n == 0    -> same as @CvImplies a b@
    --     | otherwise -> same as @CvImplies a (CvNextN n b)@
    --
    | CvAlways (Assertion' a)
    -- ^ Assertion should _always_ hold
    | CvNever (Assertion' a)
    -- ^ Assertion should _never_ hold (not supported by SVA)
    | CvEventually (Assertion' a)
    -- ^ Assertion should _eventually_ hold
    deriving (Show, Functor, Foldable, Traversable)
  
  -- | Internal version of 'Property'. All user facing will instantiate @a@
  -- with @(Maybe Text, Signal dom Bool)@. Blackboxes will instantiate it with
  -- @(Maybe Text, Term)@ instead.
  data Property' a
    = CvAssert (Assertion' a)
    | CvCover (Assertion' a)
    | CvAssume (Assertion' a)
    deriving (Show, Functor, Foldable, Traversable)
  
  data Assertion (dom :: Domain) =
    Assertion IsTemporal (Assertion' (Maybe Text, Signal dom Bool))
  
  toTemporal :: Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
  toTemporal (Assertion IsTemporal a) = a
  toTemporal (Assertion IsNotTemporal a) = CvToTemporal a
  {-# INLINE toTemporal #-}
  
  isTemporal :: Assertion dom -> IsTemporal
  isTemporal (Assertion it _assert) = it
  {-# INLINE isTemporal #-}
  
  assertion :: Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
  assertion (Assertion _it assert) = assert
  {-# INLINE assertion #-}
  
  -- | A property is a temporal or basic assertion that's specified to either
  -- used as an _assert_ or _cover_ statement. See
  -- 'Clash.Explicit.Verification.assert' and 'Clash.Explicit.Verification.cover'.
  newtype Property (dom :: Domain) =
    Property (Property' (Maybe Text, Signal dom Bool))
  
  -- | A result of some property. Besides carrying the actual boolean result, it
  -- carries some properties used to make reports.
  data AssertionResult = AssertionResult
    { cvPropName :: !String  -- I'd like text, but Clash complains :[
    -- ^ Name of property belonging to this result
    , cvPass :: !Bool
    -- ^ False whenever property is violated, True otherwise
    }
    deriving (Eq)
  {-# ANN module (
    DataReprAnn
      $(liftQ [t| AssertionResult |])
      0
      [ ConstrRepr 'AssertionResult 0 0 [0b0, 0b0]
      ]) #-}
  {- Marked as zero-width so Clash won't stumble on the fact it's unrepresentable. ^ -}
  
  -- | An AssertionValue is a bool-like value or stream that can be used in
  -- property specifications. Clash implements two: a stream of booleans
  -- (Signal dom Bool), and the result of a property expression (Assertion
  -- dom).
  class AssertionValue dom a | a -> dom where
    -- | Convert given type into a Assertion.
    toAssertionValue :: a -> Assertion dom
  
  -- | Stream of booleans, originating from a circuit
  instance AssertionValue dom (Signal dom Bool) where
    toAssertionValue s = Assertion IsNotTemporal (CvPure (Nothing, s))
    {-# INLINE toAssertionValue #-}
  
  -- | Result of a property specification
  instance AssertionValue dom (Assertion dom) where
    toAssertionValue = id
    {-# INLINE toAssertionValue #-}
  