Clash.Verification.Internal

Verification

Documentation

data AssertionResult

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

Eq AssertionResult

Defined in Clash.Verification.Internal

Methods

(==) :: AssertionResult -> AssertionResult -> Bool

(/=) :: AssertionResult -> AssertionResult -> Bool

newtype Property (dom :: Domain)

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)

Constructors

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

Instances

AssertionValue dom (Assertion dom)

Result of a property specification

Defined in Clash.Verification.Internal

Methods

toAssertionValue :: Assertion dom -> Assertion dom

data RenderAs

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

Eq RenderAs

Defined in Clash.Verification.Internal

Methods

(==) :: RenderAs -> RenderAs -> Bool

(/=) :: RenderAs -> RenderAs -> Bool

Show RenderAs

Defined in Clash.Verification.Internal

Methods

showsPrec :: Int -> RenderAs -> ShowS

show :: RenderAs -> String

showList :: [RenderAs] -> ShowS

data IsTemporal

Constructors

IsNotTemporal

IsTemporal

Instances

Eq IsTemporal

Defined in Clash.Verification.Internal

Methods

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

(/=) :: IsTemporal -> IsTemporal -> Bool

Ord IsTemporal

Defined in Clash.Verification.Internal

Methods

compare :: IsTemporal -> IsTemporal -> Ordering

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

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

(>) :: IsTemporal -> IsTemporal -> Bool

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

max :: IsTemporal -> IsTemporal -> IsTemporal

min :: IsTemporal -> IsTemporal -> IsTemporal

class AssertionValue dom a | a -> dom where

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

Convert given type into a Assertion.

Instances

AssertionValue dom (Assertion dom)

Result of a property specification

Defined in Clash.Verification.Internal

Methods

toAssertionValue :: Assertion dom -> Assertion dom

AssertionValue dom (Signal dom Bool)

Stream of booleans, originating from a circuit

Defined in Clash.Verification.Internal

Methods

toAssertionValue :: Signal dom Bool -> Assertion dom

data Assertion' a

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

Functor Assertion'

Defined in Clash.Verification.Internal

Methods

fmap :: (a -> b) -> Assertion' a -> Assertion' b

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

Foldable Assertion'

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'

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)

Defined in Clash.Verification.Internal

Methods

showsPrec :: Int -> Assertion' a -> ShowS

show :: Assertion' a -> String

showList :: [Assertion' a] -> ShowS

data Property' a

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

Functor Property'

Defined in Clash.Verification.Internal

Methods

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

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

Foldable Property'

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'

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)

Defined in Clash.Verification.Internal

Methods

showsPrec :: Int -> Property' a -> ShowS

show :: Property' a -> String

showList :: [Property' a] -> ShowS

toTemporal :: Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)

isTemporal :: Assertion dom -> IsTemporal

assertion :: Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)