{-|
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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 (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 :: 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 :: 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