{-|
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 (Int -> RenderAs -> ShowS
[RenderAs] -> ShowS
RenderAs -> String
(Int -> RenderAs -> ShowS)
-> (RenderAs -> String) -> ([RenderAs] -> ShowS) -> Show RenderAs
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RenderAs -> ShowS
showsPrec :: Int -> RenderAs -> ShowS
$cshow :: RenderAs -> String
show :: RenderAs -> String
$cshowList :: [RenderAs] -> ShowS
showList :: [RenderAs] -> ShowS
Show, RenderAs -> RenderAs -> Bool
(RenderAs -> RenderAs -> Bool)
-> (RenderAs -> RenderAs -> Bool) -> Eq RenderAs
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RenderAs -> RenderAs -> Bool
== :: RenderAs -> RenderAs -> Bool
$c/= :: RenderAs -> RenderAs -> Bool
/= :: RenderAs -> RenderAs -> Bool
Eq)

data IsTemporal
  = IsNotTemporal
  | IsTemporal
  deriving (IsTemporal -> IsTemporal -> Bool
(IsTemporal -> IsTemporal -> Bool)
-> (IsTemporal -> IsTemporal -> Bool) -> Eq IsTemporal
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IsTemporal -> IsTemporal -> Bool
== :: IsTemporal -> IsTemporal -> Bool
$c/= :: IsTemporal -> IsTemporal -> Bool
/= :: IsTemporal -> IsTemporal -> Bool
Eq, Eq IsTemporal
Eq IsTemporal =>
(IsTemporal -> IsTemporal -> Ordering)
-> (IsTemporal -> IsTemporal -> Bool)
-> (IsTemporal -> IsTemporal -> Bool)
-> (IsTemporal -> IsTemporal -> Bool)
-> (IsTemporal -> IsTemporal -> Bool)
-> (IsTemporal -> IsTemporal -> IsTemporal)
-> (IsTemporal -> IsTemporal -> IsTemporal)
-> Ord IsTemporal
IsTemporal -> IsTemporal -> Bool
IsTemporal -> IsTemporal -> Ordering
IsTemporal -> IsTemporal -> IsTemporal
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: IsTemporal -> IsTemporal -> Ordering
compare :: IsTemporal -> IsTemporal -> Ordering
$c< :: IsTemporal -> IsTemporal -> Bool
< :: IsTemporal -> IsTemporal -> Bool
$c<= :: IsTemporal -> IsTemporal -> Bool
<= :: IsTemporal -> IsTemporal -> Bool
$c> :: IsTemporal -> IsTemporal -> Bool
> :: IsTemporal -> IsTemporal -> Bool
$c>= :: IsTemporal -> IsTemporal -> Bool
>= :: IsTemporal -> IsTemporal -> Bool
$cmax :: IsTemporal -> IsTemporal -> IsTemporal
max :: IsTemporal -> IsTemporal -> IsTemporal
$cmin :: IsTemporal -> IsTemporal -> IsTemporal
min :: IsTemporal -> IsTemporal -> IsTemporal
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 (Int -> Assertion' a -> ShowS
[Assertion' a] -> ShowS
Assertion' a -> String
(Int -> Assertion' a -> ShowS)
-> (Assertion' a -> String)
-> ([Assertion' a] -> ShowS)
-> Show (Assertion' a)
forall a. Show a => Int -> Assertion' a -> ShowS
forall a. Show a => [Assertion' a] -> ShowS
forall a. Show a => Assertion' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Assertion' a -> ShowS
showsPrec :: Int -> Assertion' a -> ShowS
$cshow :: forall a. Show a => Assertion' a -> String
show :: Assertion' a -> String
$cshowList :: forall a. Show a => [Assertion' a] -> ShowS
showList :: [Assertion' a] -> ShowS
Show, (forall a b. (a -> b) -> Assertion' a -> Assertion' b)
-> (forall a b. a -> Assertion' b -> Assertion' a)
-> Functor Assertion'
forall a b. a -> Assertion' b -> Assertion' a
forall a b. (a -> b) -> Assertion' a -> Assertion' b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Assertion' a -> Assertion' b
fmap :: forall a b. (a -> b) -> Assertion' a -> Assertion' b
$c<$ :: forall a b. a -> Assertion' b -> Assertion' a
<$ :: forall a b. a -> Assertion' b -> Assertion' a
Functor, (forall m. Monoid m => Assertion' m -> m)
-> (forall m a. Monoid m => (a -> m) -> Assertion' a -> m)
-> (forall m a. Monoid m => (a -> m) -> Assertion' a -> m)
-> (forall a b. (a -> b -> b) -> b -> Assertion' a -> b)
-> (forall a b. (a -> b -> b) -> b -> Assertion' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Assertion' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Assertion' a -> b)
-> (forall a. (a -> a -> a) -> Assertion' a -> a)
-> (forall a. (a -> a -> a) -> Assertion' a -> a)
-> (forall a. Assertion' a -> [a])
-> (forall a. Assertion' a -> Bool)
-> (forall a. Assertion' a -> Int)
-> (forall a. Eq a => a -> Assertion' a -> Bool)
-> (forall a. Ord a => Assertion' a -> a)
-> (forall a. Ord a => Assertion' a -> a)
-> (forall a. Num a => Assertion' a -> a)
-> (forall a. Num a => Assertion' a -> a)
-> Foldable Assertion'
forall a. Eq a => a -> Assertion' a -> Bool
forall a. Num a => Assertion' a -> a
forall a. Ord a => Assertion' a -> a
forall m. Monoid m => Assertion' m -> m
forall a. Assertion' a -> Bool
forall a. Assertion' a -> Int
forall a. Assertion' a -> [a]
forall a. (a -> a -> a) -> Assertion' a -> a
forall m a. Monoid m => (a -> m) -> Assertion' a -> m
forall b a. (b -> a -> b) -> b -> Assertion' a -> b
forall a b. (a -> b -> b) -> b -> Assertion' a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Assertion' m -> m
fold :: forall m. Monoid m => Assertion' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Assertion' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Assertion' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Assertion' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Assertion' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Assertion' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Assertion' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Assertion' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Assertion' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Assertion' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Assertion' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Assertion' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Assertion' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Assertion' a -> a
foldr1 :: forall a. (a -> a -> a) -> Assertion' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Assertion' a -> a
foldl1 :: forall a. (a -> a -> a) -> Assertion' a -> a
$ctoList :: forall a. Assertion' a -> [a]
toList :: forall a. Assertion' a -> [a]
$cnull :: forall a. Assertion' a -> Bool
null :: forall a. Assertion' a -> Bool
$clength :: forall a. Assertion' a -> Int
length :: forall a. Assertion' a -> Int
$celem :: forall a. Eq a => a -> Assertion' a -> Bool
elem :: forall a. Eq a => a -> Assertion' a -> Bool
$cmaximum :: forall a. Ord a => Assertion' a -> a
maximum :: forall a. Ord a => Assertion' a -> a
$cminimum :: forall a. Ord a => Assertion' a -> a
minimum :: forall a. Ord a => Assertion' a -> a
$csum :: forall a. Num a => Assertion' a -> a
sum :: forall a. Num a => Assertion' a -> a
$cproduct :: forall a. Num a => Assertion' a -> a
product :: forall a. Num a => Assertion' a -> a
Foldable, Functor Assertion'
Foldable Assertion'
(Functor Assertion', Foldable Assertion') =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> Assertion' a -> f (Assertion' b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    Assertion' (f a) -> f (Assertion' a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Assertion' a -> m (Assertion' b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    Assertion' (m a) -> m (Assertion' a))
-> Traversable Assertion'
forall (t :: Type -> Type).
(Functor t, Foldable t) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    t (f a) -> f (t a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: Type -> Type) a.
Monad m =>
Assertion' (m a) -> m (Assertion' a)
forall (f :: Type -> Type) a.
Applicative f =>
Assertion' (f a) -> f (Assertion' a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Assertion' a -> m (Assertion' b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Assertion' a -> f (Assertion' b)
$ctraverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Assertion' a -> f (Assertion' b)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Assertion' a -> f (Assertion' b)
$csequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
Assertion' (f a) -> f (Assertion' a)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
Assertion' (f a) -> f (Assertion' a)
$cmapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Assertion' a -> m (Assertion' b)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Assertion' a -> m (Assertion' b)
$csequence :: forall (m :: Type -> Type) a.
Monad m =>
Assertion' (m a) -> m (Assertion' a)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
Assertion' (m a) -> m (Assertion' a)
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 (Int -> Property' a -> ShowS
[Property' a] -> ShowS
Property' a -> String
(Int -> Property' a -> ShowS)
-> (Property' a -> String)
-> ([Property' a] -> ShowS)
-> Show (Property' a)
forall a. Show a => Int -> Property' a -> ShowS
forall a. Show a => [Property' a] -> ShowS
forall a. Show a => Property' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Property' a -> ShowS
showsPrec :: Int -> Property' a -> ShowS
$cshow :: forall a. Show a => Property' a -> String
show :: Property' a -> String
$cshowList :: forall a. Show a => [Property' a] -> ShowS
showList :: [Property' a] -> ShowS
Show, (forall a b. (a -> b) -> Property' a -> Property' b)
-> (forall a b. a -> Property' b -> Property' a)
-> Functor Property'
forall a b. a -> Property' b -> Property' a
forall a b. (a -> b) -> Property' a -> Property' b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Property' a -> Property' b
fmap :: forall a b. (a -> b) -> Property' a -> Property' b
$c<$ :: forall a b. a -> Property' b -> Property' a
<$ :: forall a b. a -> Property' b -> Property' a
Functor, (forall m. Monoid m => Property' m -> m)
-> (forall m a. Monoid m => (a -> m) -> Property' a -> m)
-> (forall m a. Monoid m => (a -> m) -> Property' a -> m)
-> (forall a b. (a -> b -> b) -> b -> Property' a -> b)
-> (forall a b. (a -> b -> b) -> b -> Property' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Property' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Property' a -> b)
-> (forall a. (a -> a -> a) -> Property' a -> a)
-> (forall a. (a -> a -> a) -> Property' a -> a)
-> (forall a. Property' a -> [a])
-> (forall a. Property' a -> Bool)
-> (forall a. Property' a -> Int)
-> (forall a. Eq a => a -> Property' a -> Bool)
-> (forall a. Ord a => Property' a -> a)
-> (forall a. Ord a => Property' a -> a)
-> (forall a. Num a => Property' a -> a)
-> (forall a. Num a => Property' a -> a)
-> Foldable Property'
forall a. Eq a => a -> Property' a -> Bool
forall a. Num a => Property' a -> a
forall a. Ord a => Property' a -> a
forall m. Monoid m => Property' m -> m
forall a. Property' a -> Bool
forall a. Property' a -> Int
forall a. Property' a -> [a]
forall a. (a -> a -> a) -> Property' a -> a
forall m a. Monoid m => (a -> m) -> Property' a -> m
forall b a. (b -> a -> b) -> b -> Property' a -> b
forall a b. (a -> b -> b) -> b -> Property' a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Property' m -> m
fold :: forall m. Monoid m => Property' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Property' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Property' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Property' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Property' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Property' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Property' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Property' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Property' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Property' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Property' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Property' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Property' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Property' a -> a
foldr1 :: forall a. (a -> a -> a) -> Property' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Property' a -> a
foldl1 :: forall a. (a -> a -> a) -> Property' a -> a
$ctoList :: forall a. Property' a -> [a]
toList :: forall a. Property' a -> [a]
$cnull :: forall a. Property' a -> Bool
null :: forall a. Property' a -> Bool
$clength :: forall a. Property' a -> Int
length :: forall a. Property' a -> Int
$celem :: forall a. Eq a => a -> Property' a -> Bool
elem :: forall a. Eq a => a -> Property' a -> Bool
$cmaximum :: forall a. Ord a => Property' a -> a
maximum :: forall a. Ord a => Property' a -> a
$cminimum :: forall a. Ord a => Property' a -> a
minimum :: forall a. Ord a => Property' a -> a
$csum :: forall a. Num a => Property' a -> a
sum :: forall a. Num a => Property' a -> a
$cproduct :: forall a. Num a => Property' a -> a
product :: forall a. Num a => Property' a -> a
Foldable, Functor Property'
Foldable Property'
(Functor Property', Foldable Property') =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> Property' a -> f (Property' b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    Property' (f a) -> f (Property' a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Property' a -> m (Property' b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    Property' (m a) -> m (Property' a))
-> Traversable Property'
forall (t :: Type -> Type).
(Functor t, Foldable t) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    t (f a) -> f (t a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: Type -> Type) a.
Monad m =>
Property' (m a) -> m (Property' a)
forall (f :: Type -> Type) a.
Applicative f =>
Property' (f a) -> f (Property' a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Property' a -> m (Property' b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Property' a -> f (Property' b)
$ctraverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Property' a -> f (Property' b)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Property' a -> f (Property' b)
$csequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
Property' (f a) -> f (Property' a)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
Property' (f a) -> f (Property' a)
$cmapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Property' a -> m (Property' b)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Property' a -> m (Property' b)
$csequence :: forall (m :: Type -> Type) a.
Monad m =>
Property' (m a) -> m (Property' a)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
Property' (m a) -> m (Property' a)
Traversable)

data Assertion (dom :: Domain) =
  Assertion IsTemporal (Assertion' (Maybe Text, Signal dom Bool))

toTemporal :: Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
toTemporal :: forall (dom :: Domain).
Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
toTemporal (Assertion IsTemporal
IsTemporal Assertion' (Maybe Text, Signal dom Bool)
a) = Assertion' (Maybe Text, Signal dom Bool)
a
toTemporal (Assertion IsTemporal
IsNotTemporal Assertion' (Maybe Text, Signal dom Bool)
a) = Assertion' (Maybe Text, Signal dom Bool)
-> Assertion' (Maybe Text, Signal dom Bool)
forall a. Assertion' a -> Assertion' a
CvToTemporal Assertion' (Maybe Text, Signal dom Bool)
a
{-# INLINE toTemporal #-}

isTemporal :: Assertion dom -> IsTemporal
isTemporal :: forall (dom :: Domain). Assertion dom -> IsTemporal
isTemporal (Assertion IsTemporal
it Assertion' (Maybe Text, Signal dom Bool)
_assert) = IsTemporal
it
{-# INLINE isTemporal #-}

assertion :: Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
assertion :: forall (dom :: Domain).
Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
assertion (Assertion IsTemporal
_it Assertion' (Maybe Text, Signal dom Bool)
assert) = Assertion' (Maybe Text, Signal dom Bool)
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
  { AssertionResult -> String
cvPropName :: !String  -- I'd like text, but Clash complains :[
  -- ^ Name of property belonging to this result
  , AssertionResult -> Bool
cvPass :: !Bool
  -- ^ False whenever property is violated, True otherwise
  }
  deriving (AssertionResult -> AssertionResult -> Bool
(AssertionResult -> AssertionResult -> Bool)
-> (AssertionResult -> AssertionResult -> Bool)
-> Eq AssertionResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AssertionResult -> AssertionResult -> Bool
== :: AssertionResult -> AssertionResult -> Bool
$c/= :: AssertionResult -> AssertionResult -> Bool
/= :: AssertionResult -> AssertionResult -> Bool
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 :: Signal dom Bool -> Assertion dom
toAssertionValue Signal dom Bool
s = 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 (Maybe Text
forall a. Maybe a
Nothing, Signal dom Bool
s))
  {-# INLINE toAssertionValue #-}

-- | Result of a property specification
instance AssertionValue dom (Assertion dom) where
  toAssertionValue :: Assertion dom -> Assertion dom
toAssertionValue = Assertion dom -> Assertion dom
forall a. a -> a
id
  {-# INLINE toAssertionValue #-}