clash-prelude-1.6.3: Clash: a functional hardware description language - Prelude library
Copyright(C) 2019 Myrtle Software Ltd
LicenseBSD2 (see the file LICENSE)
MaintainerQBayLogic B.V. <devops@qbaylogic.com>
Safe HaskellNone
LanguageHaskell2010

Clash.Explicit.Verification

Description

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.

Synopsis

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

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.

class AssertionValue dom a | a -> dom 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).

Minimal complete definition

toAssertionValue

Instances

Instances details
AssertionValue dom (Assertion dom) Source #

Result of a property specification

Instance details

Defined in Clash.Verification.Internal

AssertionValue dom (Signal dom Bool) Source #

Stream of booleans, originating from a circuit

Instance details

Defined in Clash.Verification.Internal

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

Show RenderAs Source # 
Instance details

Defined in Clash.Verification.Internal

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.

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

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

Assertion checking

check Source #

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 Source #

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 Source #

Print assertions in HDL