Clash.Verification

See Clash.Explicit.Verification for an introduction.

The verification API is currently experimental and subject to change.

Types

data Assertion (dom :: Domain)

Instances

AssertionValue dom (Assertion dom)

Result of a property specification

Defined in Clash.Verification.Internal

Methods

toAssertionValue :: Assertion dom -> Assertion dom

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

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

Bootstrapping functions

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

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

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

Functions to build a PSL/SVA expressions

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

Truth table for not:

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

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

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

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

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

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

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

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

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

Same as implies but strictly temporal.

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

Specify assertion should _always_ hold

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

Specify assertion should _never_ hold (not supported by SVA)

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

Specify assertion should _eventually_ hold

Asserts

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

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

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

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

Assertion checking

check

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

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

Print assertions in HDL