{-|
Copyright  :  (C) 2019, Myrtle Software Ltd
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 NoImplicitPrelude #-}

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           Clash.Annotations.Primitive
  (Primitive(InlinePrimitive), 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." ]))
{-# NOINLINE check #-}
{-# ANN check (InlinePrimitive [Verilog, SystemVerilog, VHDL] "[ { \"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