{-|
Copyright  :  (C) 2019, Myrtle Software Ltd
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 NoImplicitPrelude #-}

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

  -- * Asserts
  , assert
  , cover

  -- * 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           Clash.Annotations.Primitive
  (Primitive(InlinePrimitive), 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
never :: AssertionValue dom a => a -> Assertion dom
never = Assertion IsTemporal . CvNever . assertion . toAssertionValue
{-# INLINE never #-}

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

-- | 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." ]))
{-# NOINLINE check #-}
{-# ANN check (InlinePrimitive [Verilog, SystemVerilog, VHDL] "[ { \"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