clash-prelude-1.8.4: Clash: a functional hardware description language - Prelude library

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 :: forall (dom :: Domain). Text -> Signal dom Bool -> Assertion dom
- lit :: forall (dom :: Domain). Bool -> Assertion dom
- not :: forall (dom :: Domain) a. AssertionValue dom a => a -> Assertion dom
- and :: forall (dom :: Domain) a b. (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
- or :: forall (dom :: Domain) a b. (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
- implies :: forall (dom :: Domain) a b. (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
- next :: forall (dom :: Domain) a. AssertionValue dom a => a -> Assertion dom
- nextN :: forall (dom :: Domain) a. AssertionValue dom a => Word -> a -> Assertion dom
- before :: forall (dom :: Domain) a b. (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
- timplies :: forall (dom :: Domain) a b. (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
- timpliesOverlapping :: forall (dom :: Domain) a b. (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
- always :: forall (dom :: Domain) a. AssertionValue dom a => a -> Assertion dom
- never :: forall (dom :: Domain) a. AssertionValue dom a => a -> Assertion dom
- eventually :: forall (dom :: Domain) a. AssertionValue dom a => a -> Assertion dom
- assert :: forall (dom :: Domain) a. AssertionValue dom a => a -> Property dom
- cover :: forall (dom :: Domain) a. AssertionValue dom a => a -> Property dom
- check :: forall (dom :: Domain). (KnownDomain dom, HiddenClock dom, HiddenReset dom) => Text -> RenderAs -> Property dom -> Signal dom AssertionResult
- checkI :: forall (dom :: Domain) a. (KnownDomain dom, HiddenClock dom, HiddenReset dom) => Text -> RenderAs -> Property dom -> Signal dom a -> Signal dom a
- hideAssertion :: forall (dom :: Domain) a. 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

Show RenderAs Source # |
Instance details Defined in Clash.Verification.Internal Methods showsPrec :: Int -> RenderAs -> ShowS Source # show :: RenderAs -> String Source # showList :: [RenderAs] -> ShowS Source #
Eq RenderAs Source # |
Instance details Defined in Clash.Verification.Internal Methods (==) :: RenderAs -> RenderAs -> Bool Source # (/=) :: RenderAs -> RenderAs -> Bool Source #

# Bootstrapping functions

name :: forall (dom :: Domain). 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 :: forall (dom :: Domain). Bool -> Assertion dom Source #

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

# Functions to build a PSL/SVA expressions

not :: forall (dom :: Domain) a. AssertionValue dom a => a -> Assertion dom Source #

Truth table for `not`:

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

and :: forall (dom :: Domain) a b. (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 :: forall (dom :: Domain) a b. (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 :: forall (dom :: Domain) a b. (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 :: forall (dom :: Domain) a. 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 :: forall (dom :: Domain) a. 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 :: forall (dom :: Domain) a b. (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 :: forall (dom :: Domain) a b. (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 :: forall (dom :: Domain) a b. (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom Source #

Same as `implies` but strictly temporal.

always :: forall (dom :: Domain) a. AssertionValue dom a => a -> Assertion dom Source #

Specify assertion should _always_ hold

never :: forall (dom :: Domain) a. AssertionValue dom a => a -> Assertion dom Source #

Specify assertion should _never_ hold (not supported by SVA)

eventually :: forall (dom :: Domain) a. AssertionValue dom a => a -> Assertion dom Source #

Specify assertion should _eventually_ hold

# Asserts

assert :: forall (dom :: Domain) a. AssertionValue dom a => a -> Property dom Source #

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

cover :: forall (dom :: Domain) a. 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

:: forall (dom :: Domain). (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

:: forall (dom :: Domain) a. (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 :: forall (dom :: Domain) a. Signal dom AssertionResult -> Signal dom a -> Signal dom a Source #

Print assertions in HDL