Copyright	(C) 2019 Myrtle Software Ltd 2022 QBayLogic B.V.
License	BSD2 (see the file LICENSE)
Maintainer	QBayLogic B.V. <devops@qbaylogic.com>
Safe Haskell	None
Language	Haskell2010

Clash.Explicit.Verification

Contents

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

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

data Assertion (dom :: Domain)
data Property (dom :: Domain)
class AssertionValue dom a | a -> dom
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
assume :: AssertionValue dom a => a -> Property dom
check :: KnownDomain dom => Clock dom -> Reset dom -> Text -> RenderAs -> Property dom -> Signal dom AssertionResult
checkI :: KnownDomain dom => Clock dom -> Reset 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.

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

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