Verification.hs

{-|
Copyright  :  (C) 2019, Myrtle Software Ltd
                  2022, QBayLogic B.V.
License    :  BSD2 (see the file LICENSE)
Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>

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

{-# LANGUAGE CPP #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE QuasiQuotes #-}

module Clash.Explicit.Verification
  ( -- * Types
    Assertion
  , Property
  , AssertionValue
  , RenderAs(..)

    -- * Bootstrapping functions
  , name
  , lit

    -- * Functions to build a PSL/SVA expressions
  , not
  , and
  , or
  , implies
  , next
  , nextN
  , before
  , timplies
  , timpliesOverlapping
  , always
  , never
  , eventually

  -- * Asserts
  , assert
  , cover
  , assume

  -- * Assertion checking
  , check
  , checkI

  -- * Functions to deal with assertion results
  , hideAssertion
  )
 where

import           Prelude
  (Bool, Word, (.), pure, max, concat)

import           Data.Text  (Text)
import           Data.Maybe (Maybe(Just))
import           Data.String.Interpolate (__i)

import           Clash.Annotations.Primitive
  (Primitive(InlineYamlPrimitive), HDL(..))
import           Clash.Signal.Internal (KnownDomain, Signal, Clock, Reset)
import           Clash.XException      (errorX, hwSeqX)

import           Clash.Verification.Internal

-- | 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.
name :: Text -> Signal dom Bool -> Assertion dom
name nm signal = Assertion IsNotTemporal (CvPure (Just nm, signal))
{-# INLINE name #-}

-- | For using a literal (either True or False) in assertions
lit :: Bool -> Assertion dom
lit = Assertion IsNotTemporal . CvLit
{-# INLINE lit #-}

-- | Truth table for 'not':
--
-- > a     | not a
-- > ------------
-- > True  | False
-- > False | True
not :: AssertionValue dom a => a -> Assertion dom
not (toAssertionValue -> a) = Assertion (isTemporal a) (CvNot (assertion a))
{-# INLINE not #-}

-- | Truth table for 'and':
--
-- > a     | b     | a `and` b
-- > --------------|----------
-- > False | False | False
-- > False | True  | False
-- > True  | False | False
-- > True  | True  | True
and :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
and (toAssertionValue -> a) (toAssertionValue -> b) =
  Assertion
    (max (isTemporal a) (isTemporal b))
    (CvAnd (assertion a) (assertion b))
{-# INLINE and #-}

-- | Truth table for 'or':
--
-- > a     | b     | a `or` b
-- > --------------|---------
-- > False | False | False
-- > False | True  | True
-- > True  | False | True
-- > True  | True  | True
or :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
or (toAssertionValue -> a) (toAssertionValue -> b) =
  Assertion
    (max (isTemporal a) (isTemporal b))
    (CvOr (assertion a) (assertion b))
{-# INLINE or #-}

-- |
-- Truth table for 'implies':
--
-- > a     | b     | a `implies` b
-- > --------------|--------------
-- > False | False | True
-- > False | True  | True
-- > True  | False | False
-- > True  | True  | True
implies :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
implies (toAssertionValue -> Assertion aTmp a) (toAssertionValue -> Assertion bTmp b) =
  Assertion (max aTmp bTmp) (CvImplies a b)
{-# INLINE implies #-}

-- | 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.
next :: AssertionValue dom a => a -> Assertion dom
next = nextN 1
{-# INLINE next #-}

-- | 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.
nextN :: AssertionValue dom a => Word -> a -> Assertion dom
nextN n = Assertion IsTemporal . CvNext n . assertion . toAssertionValue
{-# INLINE nextN #-}

-- | 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".
before :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
before a0 b0 = Assertion IsTemporal (CvBefore a1 b1)
 where
  a1 = assertion (toAssertionValue a0)
  b1 = assertion (toAssertionValue b0)
{-# INLINE before #-}

-- | 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".
timplies :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
timplies a0 b0 = Assertion IsTemporal (CvTemporalImplies 1 a1 b1)
 where
  a1 = toTemporal (toAssertionValue a0)
  b1 = toTemporal (toAssertionValue b0)
{-# INLINE timplies #-}

-- | Same as 'implies' but strictly temporal.
timpliesOverlapping
  :: (AssertionValue dom a, AssertionValue dom b)
  => a
  -> b
  -> Assertion dom
timpliesOverlapping a0 b0 =
  Assertion IsTemporal (CvTemporalImplies 0 a1 b1)
 where
  a1 = toTemporal (toAssertionValue a0)
  b1 = toTemporal (toAssertionValue b0)
{-# INLINE timpliesOverlapping #-}

-- | Specify assertion should _always_ hold
always :: AssertionValue dom a => a -> Assertion dom
always = Assertion IsTemporal . CvAlways . assertion . toAssertionValue
{-# INLINE always #-}

-- | Specify assertion should _never_ hold (not supported by SVA)
never :: AssertionValue dom a => a -> Assertion dom
never = Assertion IsTemporal . CvNever . assertion . toAssertionValue
{-# INLINE never #-}

-- | Specify assertion should _eventually_ hold
eventually :: AssertionValue dom a => a -> Assertion dom
eventually = Assertion IsTemporal . CvEventually . assertion . toAssertionValue
{-# INLINE eventually #-}

-- | Check whether given assertion always holds. Results can be collected with
-- 'check'.
assert :: AssertionValue dom a => a -> Property dom
assert = Property . CvAssert . assertion . toAssertionValue
{-# INLINE assert #-}

-- | Check whether given assertion holds for at least a single cycle. Results
-- can be collected with 'check'.
cover :: AssertionValue dom a => a -> Property dom
cover = Property . CvCover . assertion . toAssertionValue
{-# INLINE cover #-}

-- | Inform the prover that this property is true. This is the same as 'assert'
-- for simulations.
assume :: AssertionValue dom a => a -> Property dom
assume = Property . CvAssume . assertion . toAssertionValue
{-# INLINE assume #-}


-- | Print property as PSL/SVA in HDL. Clash simulation support not yet
-- implemented.
check
  :: 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
check !_clk !_rst !_propName !_renderAs !_prop =
  pure (errorX (concat [
      "Simulation for Clash.Verification not yet implemented. If you need this,"
    , " create an issue at https://github.com/clash-compiler/clash-lang/issues." ]))
-- See: https://github.com/clash-lang/clash-compiler/pull/2511
{-# CLASH_OPAQUE check #-}
{-# ANN check (InlineYamlPrimitive [Verilog, SystemVerilog, VHDL] [__i|
  BlackBoxHaskell:
    name: Clash.Explicit.Verification.check
    templateFunction: Clash.Primitives.Verification.checkBBF
  |]) #-}

-- | Same as 'check', but doesn't require a design to explicitly carried to
-- top-level.
checkI
  :: 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
checkI clk rst propName renderAs prop =
  hideAssertion (check clk rst propName renderAs prop)

-- | Print assertions in HDL
hideAssertion :: Signal dom AssertionResult -> Signal dom a -> Signal dom a
hideAssertion = hwSeqX