clash-prelude-1.8.0: Clash: a functional hardware description language - Prelude library
Copyright(C) 2019 Myrtle Software Ltd
LicenseBSD2 (see the file LICENSE)
MaintainerQBayLogic B.V. <devops@qbaylogic.com>
Safe HaskellNone
LanguageHaskell2010

Clash.Verification.Internal

Description

Verification

Synopsis

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

Instances

Instances details
Eq AssertionResult Source # 
Instance details

Defined in Clash.Verification.Internal

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 #

Instances

Instances details
AssertionValue dom (Assertion dom) Source #

Result of a property specification

Instance details

Defined in Clash.Verification.Internal

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
Eq RenderAs Source # 
Instance details

Defined in Clash.Verification.Internal

Show RenderAs Source # 
Instance details

Defined in Clash.Verification.Internal

class AssertionValue dom 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

AssertionValue dom (Signal dom Bool) Source #

Stream of booleans, originating from a circuit

Instance details

Defined in Clash.Verification.Internal

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 #

(<$) :: a -> Assertion' b -> Assertion' a #

Foldable Assertion' Source # 
Instance details

Defined in Clash.Verification.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: Assertion' a -> Bool #

length :: Assertion' a -> Int #

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

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

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

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

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

Traversable Assertion' Source # 
Instance details

Defined in Clash.Verification.Internal

Methods

traverse :: Applicative f => (a -> f b) -> Assertion' a -> f (Assertion' b) #

sequenceA :: Applicative f => Assertion' (f a) -> f (Assertion' a) #

mapM :: Monad m => (a -> m b) -> Assertion' a -> m (Assertion' b) #

sequence :: Monad m => Assertion' (m a) -> m (Assertion' a) #

Show a => Show (Assertion' a) Source # 
Instance details

Defined in Clash.Verification.Internal

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.

Instances

Instances details
Functor Property' Source # 
Instance details

Defined in Clash.Verification.Internal

Methods

fmap :: (a -> b) -> Property' a -> Property' b #

(<$) :: a -> Property' b -> Property' a #

Foldable Property' Source # 
Instance details

Defined in Clash.Verification.Internal

Methods

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

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

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

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

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

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

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

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

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

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

null :: Property' a -> Bool #

length :: Property' a -> Int #

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

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

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

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

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

Traversable Property' Source # 
Instance details

Defined in Clash.Verification.Internal

Methods

traverse :: Applicative f => (a -> f b) -> Property' a -> f (Property' b) #

sequenceA :: Applicative f => Property' (f a) -> f (Property' a) #

mapM :: Monad m => (a -> m b) -> Property' a -> m (Property' b) #

sequence :: Monad m => Property' (m a) -> m (Property' a) #

Show a => Show (Property' a) Source # 
Instance details

Defined in Clash.Verification.Internal