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

    Verification primitives for Clash. Currently implements PSL (Property
    Specification Language) and SVA (SystemVerilog Assertions). For a good overview
    of PSL and an introduction to the concepts of property checking, read
    <https://standards.ieee.org/standard/62531-2012.html>.

    The verification API is currently experimental and subject to change.
    -}

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE NoImplicitPrelude #-}
    {-# LANGUAGE QuasiQuotes #-}

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

        -- * Bootstrapping functions
      , name
      , lit

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

      -- * Asserts
      , assert
      , cover
      , assume

      -- * Assertion checking
      , check
      , checkI

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

    import           Prelude
      (Bool, Word, (.), pure, max, concat)

    import           Data.Text  (Text)
    import           Data.Maybe (Maybe(Just))
    import           Data.String.Interpolate (__i)

    import           Clash.Annotations.Primitive
      (Primitive(InlineYamlPrimitive), HDL(..))
    import           Clash.Signal.Internal (KnownDomain, Signal, Clock, Reset)
    import           Clash.XException      (errorX, hwSeqX)

    import           Clash.Verification.Internal

    -- | Convert a signal to a cv expression with a name hint. Clash will try its
    -- best to use this name in the rendered assertion, but might run into
    -- collisions. You can skip using 'name' altogether. Clash will then try its
    -- best to get a readable name from context.
    name :: Text -> Signal dom Bool -> Assertion dom
    name :: forall (dom :: Domain). Text -> Signal dom Bool -> Assertion dom
    name Text
    nm Signal dom Bool
    signal = IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    forall (dom :: Domain).
    IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    Assertion IsTemporal
    IsNotTemporal ((Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall a. a -> Assertion' a
    CvPure (Text -> Maybe Text
    forall a. a -> Maybe a
    Just Text
    nm, Signal dom Bool
    signal))
    {-# INLINE name #-}

    -- | For using a literal (either True or False) in assertions
    lit :: Bool -> Assertion dom
    lit :: forall (dom :: Domain). Bool -> Assertion dom
    lit = IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    forall (dom :: Domain).
    IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    Assertion IsTemporal
    IsNotTemporal (Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom)
    -> (Bool -> Assertion' (Maybe Text, Signal dom Bool))
    -> Bool
    -> Assertion dom
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Assertion' (Maybe Text, Signal dom Bool)
    forall a. Bool -> Assertion' a
    CvLit
    {-# INLINE lit #-}

    -- | Truth table for 'not':
    --
    -- > a     | not a
    -- > ------------
    -- > True  | False
    -- > False | True
    not :: AssertionValue dom a => a -> Assertion dom
    not :: forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    not (a -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue -> Assertion dom
    a) = IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    forall (dom :: Domain).
    IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    Assertion (Assertion dom -> IsTemporal
    forall (dom :: Domain). Assertion dom -> IsTemporal
    isTemporal Assertion dom
    a) (Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall a. Assertion' a -> Assertion' a
    CvNot (Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    assertion Assertion dom
    a))
    {-# INLINE not #-}

    -- | Truth table for 'and':
    --
    -- > a     | b     | a `and` b
    -- > --------------|----------
    -- > False | False | False
    -- > False | True  | False
    -- > True  | False | False
    -- > True  | True  | True
    and :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
    and :: forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    and (a -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue -> Assertion dom
    a) (b -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue -> Assertion dom
    b) =
      IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    forall (dom :: Domain).
    IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    Assertion
        (IsTemporal -> IsTemporal -> IsTemporal
    forall a. Ord a => a -> a -> a
    max (Assertion dom -> IsTemporal
    forall (dom :: Domain). Assertion dom -> IsTemporal
    isTemporal Assertion dom
    a) (Assertion dom -> IsTemporal
    forall (dom :: Domain). Assertion dom -> IsTemporal
    isTemporal Assertion dom
    b))
        (Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall a. Assertion' a -> Assertion' a -> Assertion' a
    CvAnd (Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    assertion Assertion dom
    a) (Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    assertion Assertion dom
    b))
    {-# INLINE and #-}

    -- | Truth table for 'or':
    --
    -- > a     | b     | a `or` b
    -- > --------------|---------
    -- > False | False | False
    -- > False | True  | True
    -- > True  | False | True
    -- > True  | True  | True
    or :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
    or :: forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    or (a -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue -> Assertion dom
    a) (b -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue -> Assertion dom
    b) =
      IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    forall (dom :: Domain).
    IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    Assertion
        (IsTemporal -> IsTemporal -> IsTemporal
    forall a. Ord a => a -> a -> a
    max (Assertion dom -> IsTemporal
    forall (dom :: Domain). Assertion dom -> IsTemporal
    isTemporal Assertion dom
    a) (Assertion dom -> IsTemporal
    forall (dom :: Domain). Assertion dom -> IsTemporal
    isTemporal Assertion dom
    b))
        (Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall a. Assertion' a -> Assertion' a -> Assertion' a
    CvOr (Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    assertion Assertion dom
    a) (Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    assertion Assertion dom
    b))
    {-# INLINE or #-}

    -- |
    -- Truth table for 'implies':
    --
    -- > a     | b     | a `implies` b
    -- > --------------|--------------
    -- > False | False | True
    -- > False | True  | True
    -- > True  | False | False
    -- > True  | True  | True
    implies :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
    implies :: forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    implies (a -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue -> Assertion IsTemporal
    aTmp Assertion' (Maybe Text, Signal dom Bool)
    a) (b -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue -> Assertion IsTemporal
    bTmp Assertion' (Maybe Text, Signal dom Bool)
    b) =
      IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    forall (dom :: Domain).
    IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    Assertion (IsTemporal -> IsTemporal -> IsTemporal
    forall a. Ord a => a -> a -> a
    max IsTemporal
    aTmp IsTemporal
    bTmp) (Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall a. Assertion' a -> Assertion' a -> Assertion' a
    CvImplies Assertion' (Maybe Text, Signal dom Bool)
    a Assertion' (Maybe Text, Signal dom Bool)
    b)
    {-# INLINE implies #-}

    -- | Truth table for 'next':
    --
    -- > a[n]  | a[n+1] | a `implies` next a
    -- > ---------------|-------------------
    -- > False | False  | True
    -- > False | True   | True
    -- > True  | False  | False
    -- > True  | True   | True
    --
    -- where a[n] represents the value of @a@ at cycle @n@ and @a[n+1]@ represents
    -- the value of @a@ at cycle @n+1@. Cycle n is an arbitrary cycle.
    next :: AssertionValue dom a => a -> Assertion dom
    next :: forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    next = Word -> a -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    Word -> a -> Assertion dom
    nextN Word
    1
    {-# INLINE next #-}

    -- | Truth table for 'nextN':
    --
    -- > a[n]  | a[n+m] | a `implies` next m a
    -- > ---------------|---------------------
    -- > False | False  | True
    -- > False | True   | True
    -- > True  | False  | False
    -- > True  | True   | True
    --
    -- where a[n] represents the value of @a@ at cycle @n@ and a[n+m] represents
    -- the value of @a@ at cycle @n+m@. Cycle n is an arbitrary cycle.
    nextN :: AssertionValue dom a => Word -> a -> Assertion dom
    nextN :: forall (dom :: Domain) a.
    AssertionValue dom a =>
    Word -> a -> Assertion dom
    nextN Word
    n = IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    forall (dom :: Domain).
    IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    Assertion IsTemporal
    IsTemporal (Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom)
    -> (a -> Assertion' (Maybe Text, Signal dom Bool))
    -> a
    -> Assertion dom
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word
    -> Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall a. Word -> Assertion' a -> Assertion' a
    CvNext Word
    n (Assertion' (Maybe Text, Signal dom Bool)
     -> Assertion' (Maybe Text, Signal dom Bool))
    -> (a -> Assertion' (Maybe Text, Signal dom Bool))
    -> a
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    assertion (Assertion dom -> Assertion' (Maybe Text, Signal dom Bool))
    -> (a -> Assertion dom)
    -> a
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue
    {-# INLINE nextN #-}

    -- | Same as @a && next b@ but with a nice syntax. E.g., @a && next b@ could
    -- be written as @a `before` b@. Might be read as "a happens one cycle before b".
    before :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
    before :: forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    before a
    a0 b
    b0 = IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    forall (dom :: Domain).
    IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    Assertion IsTemporal
    IsTemporal (Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall a. Assertion' a -> Assertion' a -> Assertion' a
    CvBefore Assertion' (Maybe Text, Signal dom Bool)
    a1 Assertion' (Maybe Text, Signal dom Bool)
    b1)
     where
      a1 :: Assertion' (Maybe Text, Signal dom Bool)
    a1 = Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    assertion (a -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue a
    a0)
      b1 :: Assertion' (Maybe Text, Signal dom Bool)
    b1 = Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    assertion (b -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue b
    b0)
    {-# INLINE before #-}

    -- | Same as @a `implies` next b@ but with a nice syntax. E.g.,
    -- @a `implies` next b@ could be written as @a `timplies` b@. Might be read
    -- as "a at cycle n implies b at cycle n+1".
    timplies :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
    timplies :: forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    timplies a
    a0 b
    b0 = IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    forall (dom :: Domain).
    IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    Assertion IsTemporal
    IsTemporal (Word
    -> Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall a. Word -> Assertion' a -> Assertion' a -> Assertion' a
    CvTemporalImplies Word
    1 Assertion' (Maybe Text, Signal dom Bool)
    a1 Assertion' (Maybe Text, Signal dom Bool)
    b1)
     where
      a1 :: Assertion' (Maybe Text, Signal dom Bool)
    a1 = Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    toTemporal (a -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue a
    a0)
      b1 :: Assertion' (Maybe Text, Signal dom Bool)
    b1 = Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    toTemporal (b -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue b
    b0)
    {-# INLINE timplies #-}

    -- | Same as 'implies' but strictly temporal.
    timpliesOverlapping
      :: (AssertionValue dom a, AssertionValue dom b)
      => a
      -> b
      -> Assertion dom
    timpliesOverlapping :: forall (dom :: Domain) a b.
    (AssertionValue dom a, AssertionValue dom b) =>
    a -> b -> Assertion dom
    timpliesOverlapping a
    a0 b
    b0 =
      IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    forall (dom :: Domain).
    IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    Assertion IsTemporal
    IsTemporal (Word
    -> Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall a. Word -> Assertion' a -> Assertion' a -> Assertion' a
    CvTemporalImplies Word
    0 Assertion' (Maybe Text, Signal dom Bool)
    a1 Assertion' (Maybe Text, Signal dom Bool)
    b1)
     where
      a1 :: Assertion' (Maybe Text, Signal dom Bool)
    a1 = Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    toTemporal (a -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue a
    a0)
      b1 :: Assertion' (Maybe Text, Signal dom Bool)
    b1 = Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    toTemporal (b -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue b
    b0)
    {-# INLINE timpliesOverlapping #-}

    -- | Specify assertion should _always_ hold
    always :: AssertionValue dom a => a -> Assertion dom
    always :: forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    always = IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    forall (dom :: Domain).
    IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    Assertion IsTemporal
    IsTemporal (Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom)
    -> (a -> Assertion' (Maybe Text, Signal dom Bool))
    -> a
    -> Assertion dom
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall a. Assertion' a -> Assertion' a
    CvAlways (Assertion' (Maybe Text, Signal dom Bool)
     -> Assertion' (Maybe Text, Signal dom Bool))
    -> (a -> Assertion' (Maybe Text, Signal dom Bool))
    -> a
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    assertion (Assertion dom -> Assertion' (Maybe Text, Signal dom Bool))
    -> (a -> Assertion dom)
    -> a
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue
    {-# INLINE always #-}

    -- | Specify assertion should _never_ hold (not supported by SVA)
    never :: AssertionValue dom a => a -> Assertion dom
    never :: forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    never = IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    forall (dom :: Domain).
    IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    Assertion IsTemporal
    IsTemporal (Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom)
    -> (a -> Assertion' (Maybe Text, Signal dom Bool))
    -> a
    -> Assertion dom
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall a. Assertion' a -> Assertion' a
    CvNever (Assertion' (Maybe Text, Signal dom Bool)
     -> Assertion' (Maybe Text, Signal dom Bool))
    -> (a -> Assertion' (Maybe Text, Signal dom Bool))
    -> a
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    assertion (Assertion dom -> Assertion' (Maybe Text, Signal dom Bool))
    -> (a -> Assertion dom)
    -> a
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue
    {-# INLINE never #-}

    -- | Specify assertion should _eventually_ hold
    eventually :: AssertionValue dom a => a -> Assertion dom
    eventually :: forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    eventually = IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    forall (dom :: Domain).
    IsTemporal
    -> Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom
    Assertion IsTemporal
    IsTemporal (Assertion' (Maybe Text, Signal dom Bool) -> Assertion dom)
    -> (a -> Assertion' (Maybe Text, Signal dom Bool))
    -> a
    -> Assertion dom
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Assertion' (Maybe Text, Signal dom Bool)
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall a. Assertion' a -> Assertion' a
    CvEventually (Assertion' (Maybe Text, Signal dom Bool)
     -> Assertion' (Maybe Text, Signal dom Bool))
    -> (a -> Assertion' (Maybe Text, Signal dom Bool))
    -> a
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    assertion (Assertion dom -> Assertion' (Maybe Text, Signal dom Bool))
    -> (a -> Assertion dom)
    -> a
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue
    {-# INLINE eventually #-}

    -- | Check whether given assertion always holds. Results can be collected with
    -- 'check'.
    assert :: AssertionValue dom a => a -> Property dom
    assert :: forall (dom :: Domain) a. AssertionValue dom a => a -> Property dom
    assert = Property' (Maybe Text, Signal dom Bool) -> Property dom
    forall (dom :: Domain).
    Property' (Maybe Text, Signal dom Bool) -> Property dom
    Property (Property' (Maybe Text, Signal dom Bool) -> Property dom)
    -> (a -> Property' (Maybe Text, Signal dom Bool))
    -> a
    -> Property dom
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Assertion' (Maybe Text, Signal dom Bool)
    -> Property' (Maybe Text, Signal dom Bool)
    forall a. Assertion' a -> Property' a
    CvAssert (Assertion' (Maybe Text, Signal dom Bool)
     -> Property' (Maybe Text, Signal dom Bool))
    -> (a -> Assertion' (Maybe Text, Signal dom Bool))
    -> a
    -> Property' (Maybe Text, Signal dom Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    assertion (Assertion dom -> Assertion' (Maybe Text, Signal dom Bool))
    -> (a -> Assertion dom)
    -> a
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue
    {-# INLINE assert #-}

    -- | Check whether given assertion holds for at least a single cycle. Results
    -- can be collected with 'check'.
    cover :: AssertionValue dom a => a -> Property dom
    cover :: forall (dom :: Domain) a. AssertionValue dom a => a -> Property dom
    cover = Property' (Maybe Text, Signal dom Bool) -> Property dom
    forall (dom :: Domain).
    Property' (Maybe Text, Signal dom Bool) -> Property dom
    Property (Property' (Maybe Text, Signal dom Bool) -> Property dom)
    -> (a -> Property' (Maybe Text, Signal dom Bool))
    -> a
    -> Property dom
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Assertion' (Maybe Text, Signal dom Bool)
    -> Property' (Maybe Text, Signal dom Bool)
    forall a. Assertion' a -> Property' a
    CvCover (Assertion' (Maybe Text, Signal dom Bool)
     -> Property' (Maybe Text, Signal dom Bool))
    -> (a -> Assertion' (Maybe Text, Signal dom Bool))
    -> a
    -> Property' (Maybe Text, Signal dom Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    assertion (Assertion dom -> Assertion' (Maybe Text, Signal dom Bool))
    -> (a -> Assertion dom)
    -> a
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue
    {-# INLINE cover #-}

    -- | Inform the prover that this property is true. This is the same as 'assert'
    -- for simulations.
    assume :: AssertionValue dom a => a -> Property dom
    assume :: forall (dom :: Domain) a. AssertionValue dom a => a -> Property dom
    assume = Property' (Maybe Text, Signal dom Bool) -> Property dom
    forall (dom :: Domain).
    Property' (Maybe Text, Signal dom Bool) -> Property dom
    Property (Property' (Maybe Text, Signal dom Bool) -> Property dom)
    -> (a -> Property' (Maybe Text, Signal dom Bool))
    -> a
    -> Property dom
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Assertion' (Maybe Text, Signal dom Bool)
    -> Property' (Maybe Text, Signal dom Bool)
    forall a. Assertion' a -> Property' a
    CvAssume (Assertion' (Maybe Text, Signal dom Bool)
     -> Property' (Maybe Text, Signal dom Bool))
    -> (a -> Assertion' (Maybe Text, Signal dom Bool))
    -> a
    -> Property' (Maybe Text, Signal dom Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    forall (dom :: Domain).
    Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
    assertion (Assertion dom -> Assertion' (Maybe Text, Signal dom Bool))
    -> (a -> Assertion dom)
    -> a
    -> Assertion' (Maybe Text, Signal dom Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Assertion dom
    forall (dom :: Domain) a.
    AssertionValue dom a =>
    a -> Assertion dom
    toAssertionValue
    {-# INLINE assume #-}

    -- | Print property as PSL/SVA in HDL. Clash simulation support not yet
    -- implemented.
    check
      :: KnownDomain dom
      => Clock dom
      -> Reset 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 =>
    Clock dom
    -> Reset dom
    -> Text
    -> RenderAs
    -> Property dom
    -> Signal dom AssertionResult
    check !Clock dom
    _clk !Reset dom
    _rst !Text
    _propName !RenderAs
    _renderAs !Property dom
    _prop =
      AssertionResult -> Signal dom AssertionResult
    forall a. a -> Signal dom a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (String -> AssertionResult
    forall a. HasCallStack => String -> a
    errorX ([String] -> String
    forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
    concat [
          String
    "Simulation for Clash.Verification not yet implemented. If you need this,"
        , String
    " create an issue at https://github.com/clash-compiler/clash-lang/issues." ]))
    -- See: https://github.com/clash-lang/clash-compiler/pull/2511
    {-# CLASH_OPAQUE check #-}
    {-# ANN check (InlineYamlPrimitive [Verilog, SystemVerilog, VHDL] [__i|
      BlackBoxHaskell:
        name: Clash.Explicit.Verification.check
        templateFunction: Clash.Primitives.Verification.checkBBF
      |]) #-}

    -- | Same as 'check', but doesn't require a design to explicitly carried to
    -- top-level.
    checkI
      :: KnownDomain dom
      => Clock dom
      -> Reset 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 =>
    Clock dom
    -> Reset dom
    -> Text
    -> RenderAs
    -> Property dom
    -> Signal dom a
    -> Signal dom a
    checkI Clock dom
    clk Reset dom
    rst Text
    propName RenderAs
    renderAs Property dom
    prop =
      Signal dom AssertionResult -> Signal dom a -> Signal dom a
    forall (dom :: Domain) a.
    Signal dom AssertionResult -> Signal dom a -> Signal dom a
    hideAssertion (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
    check Clock dom
    clk Reset dom
    rst Text
    propName RenderAs
    renderAs Property dom
    prop)

    -- | Print assertions in HDL
    hideAssertion :: Signal dom AssertionResult -> Signal dom a -> Signal dom a
    hideAssertion :: forall (dom :: Domain) a.
    Signal dom AssertionResult -> Signal dom a -> Signal dom a
    hideAssertion = Signal dom AssertionResult -> Signal dom a -> Signal dom a
    forall a b. a -> b -> b
    hwSeqX