clash-prelude-1.8.4: Clash: a functional hardware description language - Prelude library

Copyright | (C) 2019 Myrtle Software Ltd
License | BSD2 (see the file LICENSE)
Maintainer | QBayLogic B.V. <devops@qbaylogic.com>
Safe Haskell | None
Language | Haskell2010

Clash.Verification.Internal

Description

Verification

Synopsis

- data AssertionResult = AssertionResult {
  - cvPropName :: !String
  - cvPass :: !Bool
  }
- newtype Property (dom :: Domain) = Property (Property' (Maybe Text, Signal dom Bool))
- data Assertion (dom :: Domain) = Assertion IsTemporal (Assertion' (Maybe Text, Signal dom Bool))
- data RenderAs
  - = PSL
  - | SVA
  - | AutoRenderAs
  - | YosysFormal
- data IsTemporal
  - = IsNotTemporal
  - | IsTemporal
- class AssertionValue (dom :: Domain) a | a -> dom where
  - toAssertionValue :: a -> Assertion dom
- data Assertion' a
  - = CvPure a
  - | CvToTemporal (Assertion' a)
  - | CvLit Bool
  - | CvNot (Assertion' a)
  - | CvAnd (Assertion' a) (Assertion' a)
  - | CvOr (Assertion' a) (Assertion' a)
  - | CvImplies (Assertion' a) (Assertion' a)
  - | CvNext Word (Assertion' a)
  - | CvBefore (Assertion' a) (Assertion' a)
  - | CvTemporalImplies Word (Assertion' a) (Assertion' a)
  - | CvAlways (Assertion' a)
  - | CvNever (Assertion' a)
  - | CvEventually (Assertion' a)
- data Property' a
  - = CvAssert (Assertion' a)
  - | CvCover (Assertion' a)
  - | CvAssume (Assertion' a)
- toTemporal :: forall (dom :: Domain). Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
- isTemporal :: forall (dom :: Domain). Assertion dom -> IsTemporal
- assertion :: forall (dom :: Domain). Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)

# Documentation

data AssertionResult Source #

A result of some property. Besides carrying the actual boolean result, it carries some properties used to make reports.

Constructors

AssertionResult |

Fields

- cvPropName :: !String

  Name of property belonging to this result

- cvPass :: !Bool

  False whenever property is violated, True otherwise

#### Instances

Instances details

Eq AssertionResult Source # |
Instance details Defined in Clash.Verification.Internal Methods (==) :: AssertionResult -> AssertionResult -> Bool Source # (/=) :: AssertionResult -> AssertionResult -> Bool Source #

newtype Property (dom :: Domain) Source #

A property is a temporal or basic assertion that's specified to either used as an _assert_ or _cover_ statement. See `assert` and `cover`.

Constructors

Property (Property' (Maybe Text, Signal dom Bool)) |

data Assertion (dom :: Domain) Source #

Constructors

Assertion IsTemporal (Assertion' (Maybe Text, Signal dom Bool)) |

#### Instances

Instances details

AssertionValue dom (Assertion dom) Source # | Result of a property specification
Instance details Defined in Clash.Verification.Internal Methods toAssertionValue :: Assertion dom -> Assertion dom Source #

data RenderAs Source #

Render target for HDL

Constructors

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;

#### Instances

Instances details

Show RenderAs Source # |
Instance details Defined in Clash.Verification.Internal Methods showsPrec :: Int -> RenderAs -> ShowS Source # show :: RenderAs -> String Source # showList :: [RenderAs] -> ShowS Source #
Eq RenderAs Source # |
Instance details Defined in Clash.Verification.Internal Methods (==) :: RenderAs -> RenderAs -> Bool Source # (/=) :: RenderAs -> RenderAs -> Bool Source #

data IsTemporal Source #

Constructors

IsNotTemporal |
IsTemporal |

#### Instances

Instances details

Eq IsTemporal Source # |
Instance details Defined in Clash.Verification.Internal Methods (==) :: IsTemporal -> IsTemporal -> Bool Source # (/=) :: IsTemporal -> IsTemporal -> Bool Source #
Ord IsTemporal Source # |

Instance details

Defined in Clash.Verification.Internal

Methods

compare :: IsTemporal -> IsTemporal -> Ordering Source #

(<) :: IsTemporal -> IsTemporal -> Bool Source #

(<=) :: IsTemporal -> IsTemporal -> Bool Source #

(>) :: IsTemporal -> IsTemporal -> Bool Source #

(>=) :: IsTemporal -> IsTemporal -> Bool Source #

max :: IsTemporal -> IsTemporal -> IsTemporal Source #

min :: IsTemporal -> IsTemporal -> IsTemporal Source #

class AssertionValue (dom :: Domain) a | a -> dom where Source #

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).

Methods

toAssertionValue :: a -> Assertion dom Source #

Convert given type into a Assertion.

#### Instances

Instances details

AssertionValue dom (Assertion dom) Source # | Result of a property specification
Instance details Defined in Clash.Verification.Internal Methods toAssertionValue :: Assertion dom -> Assertion dom Source #
AssertionValue dom (Signal dom Bool) Source # | Stream of booleans, originating from a circuit
Instance details Defined in Clash.Verification.Internal Methods toAssertionValue :: Signal dom Bool -> Assertion dom Source #

data Assertion' a Source #

Internal version of `Assertion`.

Constructors

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

#### Instances

Instances details

Functor Assertion' Source # |
Instance details Defined in Clash.Verification.Internal Methods fmap :: (a -> b) -> Assertion' a -> Assertion' b Source # (<$) :: a -> Assertion' b -> Assertion' a Source #
Foldable Assertion' Source # |

Instance details

Defined in Clash.Verification.Internal

Methods

fold :: Monoid m => Assertion' m -> m Source #

foldMap :: Monoid m => (a -> m) -> Assertion' a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Assertion' a -> m Source #

foldr :: (a -> b -> b) -> b -> Assertion' a -> b Source #

foldr' :: (a -> b -> b) -> b -> Assertion' a -> b Source #

foldl :: (b -> a -> b) -> b -> Assertion' a -> b Source #

foldl' :: (b -> a -> b) -> b -> Assertion' a -> b Source #

foldr1 :: (a -> a -> a) -> Assertion' a -> a Source #

foldl1 :: (a -> a -> a) -> Assertion' a -> a Source #

toList :: Assertion' a -> [a] Source #

null :: Assertion' a -> Bool Source #

length :: Assertion' a -> Int Source #

elem :: Eq a => a -> Assertion' a -> Bool Source #

maximum :: Ord a => Assertion' a -> a Source #

minimum :: Ord a => Assertion' a -> a Source #

sum :: Num a => Assertion' a -> a Source #

product :: Num a => Assertion' a -> a Source #

Traversable Assertion' Source # |
Instance details Defined in Clash.Verification.Internal Methods traverse :: Applicative f => (a -> f b) -> Assertion' a -> f (Assertion' b) Source # sequenceA :: Applicative f => Assertion' (f a) -> f (Assertion' a) Source # mapM :: Monad m => (a -> m b) -> Assertion' a -> m (Assertion' b) Source # sequence :: Monad m => Assertion' (m a) -> m (Assertion' a) Source #
Show a => Show (Assertion' a) Source # |
Instance details Defined in Clash.Verification.Internal Methods showsPrec :: Int -> Assertion' a -> ShowS Source # show :: Assertion' a -> String Source # showList :: [Assertion' a] -> ShowS Source #

data Property' a Source #

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.

Constructors

CvAssert (Assertion' a) |
CvCover (Assertion' a) |
CvAssume (Assertion' a) |

#### Instances

Instances details

Functor Property' Source # |
Instance details Defined in Clash.Verification.Internal Methods fmap :: (a -> b) -> Property' a -> Property' b Source # (<$) :: a -> Property' b -> Property' a Source #
Foldable Property' Source # |

Instance details

Defined in Clash.Verification.Internal

Methods

fold :: Monoid m => Property' m -> m Source #

foldMap :: Monoid m => (a -> m) -> Property' a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Property' a -> m Source #

foldr :: (a -> b -> b) -> b -> Property' a -> b Source #

foldr' :: (a -> b -> b) -> b -> Property' a -> b Source #

foldl :: (b -> a -> b) -> b -> Property' a -> b Source #

foldl' :: (b -> a -> b) -> b -> Property' a -> b Source #

foldr1 :: (a -> a -> a) -> Property' a -> a Source #

foldl1 :: (a -> a -> a) -> Property' a -> a Source #

toList :: Property' a -> [a] Source #

null :: Property' a -> Bool Source #

length :: Property' a -> Int Source #

elem :: Eq a => a -> Property' a -> Bool Source #

maximum :: Ord a => Property' a -> a Source #

minimum :: Ord a => Property' a -> a Source #

sum :: Num a => Property' a -> a Source #

product :: Num a => Property' a -> a Source #

Traversable Property' Source # |
Instance details Defined in Clash.Verification.Internal Methods traverse :: Applicative f => (a -> f b) -> Property' a -> f (Property' b) Source # sequenceA :: Applicative f => Property' (f a) -> f (Property' a) Source # mapM :: Monad m => (a -> m b) -> Property' a -> m (Property' b) Source # sequence :: Monad m => Property' (m a) -> m (Property' a) Source #
Show a => Show (Property' a) Source # |
Instance details Defined in Clash.Verification.Internal Methods showsPrec :: Int -> Property' a -> ShowS Source # show :: Property' a -> String Source # showList :: [Property' a] -> ShowS Source #

toTemporal :: forall (dom :: Domain). Assertion dom -> Assertion' (Maybe Text, Signal dom Bool) Source #

isTemporal :: forall (dom :: Domain). Assertion dom -> IsTemporal Source #

assertion :: forall (dom :: Domain). Assertion dom -> Assertion' (Maybe Text, Signal dom Bool) Source #