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

Contents

Types
Bootstrapping functions
Functions to build a PSL/SVA expressions
Asserts
Assertion checking
Functions to deal with assertion results

Description

See Clash.Explicit.Verification for an introduction.

The verification API is currently experimental and subject to change.

Synopsis

data Assertion (dom :: Domain)
data Property (dom :: Domain)
data RenderAs
- = PSL
- | SVA
- | AutoRenderAs
- | YosysFormal
name :: Text -> Signal dom Bool -> Assertion dom
lit :: Bool -> Assertion dom
not :: AssertionValue dom a => a -> Assertion dom
and :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
or :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
implies :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
next :: AssertionValue dom a => a -> Assertion dom
nextN :: AssertionValue dom a => Word -> a -> Assertion dom
before :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
timplies :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
timpliesOverlapping :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
always :: AssertionValue dom a => a -> Assertion dom
never :: AssertionValue dom a => a -> Assertion dom
eventually :: AssertionValue dom a => a -> Assertion dom
assert :: AssertionValue dom a => a -> Property dom
cover :: AssertionValue dom a => a -> Property dom
check :: (KnownDomain dom, HiddenClock dom, HiddenReset dom) => Text -> RenderAs -> Property dom -> Signal dom AssertionResult
checkI :: (KnownDomain dom, HiddenClock dom, HiddenReset dom) => Text -> RenderAs -> Property dom -> Signal dom a -> Signal dom a
hideAssertion :: Signal dom AssertionResult -> Signal dom a -> Signal dom a

Types

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 Methods toAssertionValue :: Assertion dom -> Assertion dom Source #

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

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 #

Bootstrapping functions

name :: Text -> Signal dom Bool -> Assertion dom Source #

Convert a signal to a cv expression with a name hint. Clash will try its best to use this name in the rendered assertion, but might run into collisions. You can skip using name altogether. Clash will then try its best to get a readable name from context.

lit :: Bool -> Assertion dom Source #

For using a literal (either True or False) in assertions

Functions to build a PSL/SVA expressions

not :: AssertionValue dom a => a -> Assertion dom Source #

Truth table for not:

a     | not a
------------
True  | False
False | True

and :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom Source #

Truth table for and:

a     | b     | a `and` b
--------------|----------
False | False | False
False | True  | False
True  | False | False
True  | True  | True

or :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom Source #

Truth table for or:

a     | b     | a `or` b
--------------|---------
False | False | False
False | True  | True
True  | False | True
True  | True  | True

implies :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom Source #

Truth table for implies:

a     | b     | a `implies` b
--------------|--------------
False | False | True
False | True  | True
True  | False | False
True  | True  | True

next :: AssertionValue dom a => a -> Assertion dom Source #

Truth table for next:

a[n]  | a[n+1] | a `implies` next a
---------------|-------------------
False | False  | True
False | True   | True
True  | False  | False
True  | True   | True

where a[n] represents the value of a at cycle n and a[n+1] represents the value of a at cycle n+1. Cycle n is an arbitrary cycle.

nextN :: AssertionValue dom a => Word -> a -> Assertion dom Source #

Truth table for nextN:

a[n]  | a[n+m] | a `implies` next m a
---------------|---------------------
False | False  | True
False | True   | True
True  | False  | False
True  | True   | True

where a[n] represents the value of a at cycle n and a[n+m] represents the value of a at cycle n+m. Cycle n is an arbitrary cycle.

before :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom Source #

Same as a && next b but with a nice syntax. E.g., a && next b could be written as a before b. Might be read as "a happens one cycle before b".

timplies :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom Source #

Same as a implies next b but with a nice syntax. E.g., a implies next b could be written as a timplies b. Might be read as "a at cycle n implies b at cycle n+1".

timpliesOverlapping :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom Source #

Same as implies but strictly temporal.

always :: AssertionValue dom a => a -> Assertion dom Source #

Specify assertion should _always_ hold

never :: AssertionValue dom a => a -> Assertion dom Source #

Specify assertion should _never_ hold (not supported by SVA)

eventually :: AssertionValue dom a => a -> Assertion dom Source #

Specify assertion should _eventually_ hold

Asserts

assert :: AssertionValue dom a => a -> Property dom Source #

Check whether given assertion always holds. Results can be collected with check.

cover :: AssertionValue dom a => a -> Property dom Source #

Check whether given assertion holds for at least a single cycle. Results can be collected with check.

Assertion checking

check Source #

Arguments

:: (KnownDomain dom, HiddenClock dom, HiddenReset dom)
=> Text	Property name (used in reports and error messages)
-> RenderAs	Assertion language to use in HDL
-> Property dom
-> Signal dom AssertionResult

checkI Source #

Arguments

:: (KnownDomain dom, HiddenClock dom, HiddenReset dom)
=> Text	Property name (used in reports and error messages)
-> RenderAs	Assertion language to use in HDL
-> Property dom
-> Signal dom a
-> Signal dom a

Functions to deal with assertion results

hideAssertion :: Signal dom AssertionResult -> Signal dom a -> Signal dom a Source #

Print assertions in HDL