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 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 :: Assertion dom -> Assertion' (Maybe Text, Signal dom Bool)
isTemporal :: Assertion dom -> IsTemporal
assertion :: 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

Eq RenderAs Source #
Instance details Defined in Clash.Verification.Internal Methods (==) :: RenderAs -> RenderAs -> Bool Source # (/=) :: RenderAs -> RenderAs -> Bool Source #
Show RenderAs Source #
Instance details Defined in Clash.Verification.Internal Methods showsPrec :: Int -> RenderAs -> ShowS Source # show :: RenderAs -> String Source # showList :: [RenderAs] -> ShowS 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 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 :: Assertion dom -> Assertion' (Maybe Text, Signal dom Bool) Source #

isTemporal :: Assertion dom -> IsTemporal Source #

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