Clash.Explicit.Verification

Verification primitives for Clash. Currently implements PSL (Property Specification Language) and SVA (SystemVerilog Assertions). For a good overview of PSL and an introduction to the concepts of property checking, read https://standards.ieee.org/standard/62531-2012.html.

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.

class AssertionValue dom a | a -> dom

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

Minimal complete definition

toAssertionValue

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

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

Inform the prover that this property is true. This is the same as assert for simulations.

Assertion checking

check

Arguments

:: KnownDomain dom

=> Clock dom

-> Reset dom

-> Text

Property name (used in reports and error messages)

-> RenderAs

Assertion language to use in HDL

-> Property dom

-> Signal dom AssertionResult

Print property as PSL/SVA in HDL. Clash simulation support not yet implemented.

checkI

Arguments

:: KnownDomain dom

=> Clock dom

-> Reset 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

Same as check, but doesn't require a design to explicitly carried to top-level.

Functions to deal with assertion results

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

Print assertions in HDL