    {-|
    Copyright  :  (C) 2019, Myrtle Software Ltd
    License    :  BSD2 (see the file LICENSE)
    Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>

    See "Clash.Explicit.Verification" for an introduction.

    The verification API is currently experimental and subject to change.

    -}

    module Clash.Verification
      ( -- * Types
        Assertion
      , Property
      , RenderAs(..)

        -- * Bootstrapping functions
      , EV.name
      , EV.lit

        -- * Functions to build a PSL/SVA expressions
      , EV.not
      , EV.and
      , EV.or
      , EV.implies
      , EV.next
      , EV.nextN
      , EV.before
      , EV.timplies
      , EV.timpliesOverlapping
      , EV.always
      , EV.never
      , EV.eventually

      -- * Asserts
      , EV.assert
      , EV.cover

      -- * Assertion checking
      , check
      , checkI

      -- * Functions to deal with assertion results
      , EV.hideAssertion
      ) where

    import qualified Clash.Explicit.Verification     as EV
    import           Clash.Signal
      (KnownDomain, HiddenClock, HiddenReset, Signal, hasClock, hasReset)
    import           Clash.Verification.Internal
    import           Data.Text                       (Text)

    check
      :: ( KnownDomain dom
         , HiddenClock dom
         , HiddenReset dom
         )
      => Text
      -- ^ Property name (used in reports and error messages)
      -> RenderAs
      -- ^ Assertion language to use in HDL
      -> Property dom
      -> Signal dom AssertionResult
    check :: forall (dom :: Domain).
    (KnownDomain dom, HiddenClock dom, HiddenReset dom) =>
    Text -> RenderAs -> Property dom -> Signal dom AssertionResult
    check = Clock dom
    -> Reset dom
    -> Text
    -> RenderAs
    -> Property dom
    -> Signal dom AssertionResult
    forall (dom :: Domain).
    KnownDomain dom =>
    Clock dom
    -> Reset dom
    -> Text
    -> RenderAs
    -> Property dom
    -> Signal dom AssertionResult
    EV.check Clock dom
    forall (dom :: Domain). HiddenClock dom => Clock dom
    hasClock Reset dom
    forall (dom :: Domain). HiddenReset dom => Reset dom
    hasReset

    checkI
      :: ( KnownDomain dom
         , HiddenClock dom
         , HiddenReset dom
         )
      => Text
      -- ^ Property name (used in reports and error messages)
      -> RenderAs
      -- ^ Assertion language to use in HDL
      -> Property dom
      -> Signal dom a
      -> Signal dom a
    checkI :: forall (dom :: Domain) a.
    (KnownDomain dom, HiddenClock dom, HiddenReset dom) =>
    Text -> RenderAs -> Property dom -> Signal dom a -> Signal dom a
    checkI = Clock dom
    -> Reset dom
    -> Text
    -> RenderAs
    -> Property dom
    -> Signal dom a
    -> Signal dom a
    forall (dom :: Domain) a.
    KnownDomain dom =>
    Clock dom
    -> Reset dom
    -> Text
    -> RenderAs
    -> Property dom
    -> Signal dom a
    -> Signal dom a
    EV.checkI Clock dom
    forall (dom :: Domain). HiddenClock dom => Clock dom
    hasClock Reset dom
    forall (dom :: Domain). HiddenReset dom => Reset dom
    hasReset