Pretty.hs

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

Verification
-}

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}

module Clash.Verification.Pretty
  ( pprPslProperty
  , pprSvaProperty
  , pprYosysSvaProperty

  -- * Debugging functions
  , pprProperty
  ) where

import           Clash.Annotations.Primitive      (HDL(..))
import           Clash.Signal.Internal            (ActiveEdge, ActiveEdge(..))
import           Clash.Verification.Internal      hiding (assertion)
import           Clash.Netlist.Types              (Declaration(..), Seq(..), Expr, CommentOrDirective(..))
import           Data.Maybe                       (fromMaybe)
import           Data.Text                        (Text)
import qualified Data.Text as Text                (pack)

data Symbol
  = TImpliesOverlapping
  | TImplies
  | Implies
  | BiImplies
  | Not
  | And
  | Or
  | To
  | Equals
  -- + [] ?
  | Assign
  | Is

------------------------------------------
--                 UTIL                 --
------------------------------------------
-- | Collapse constructs such as `next (next a)` down to `next[2] a`
squashBefore :: Assertion' a -> [Assertion' a]
squashBefore (CvBefore e1 e2) = e1s ++ e2s
 where
  e1s = case squashBefore e1 of {[] -> [e1]; es -> es}
  e2s = case squashBefore e2 of {[] -> [e2]; es -> es}
squashBefore _ = []

parensIf :: Bool -> Text -> Text
parensIf True s = "(" <> s <> ")"
parensIf False s = s

---------------------------------------
--                PSL                --
---------------------------------------
pslBinOp
  :: HDL
  -> Bool
  -> Symbol
  -> Assertion' Text
  -> Assertion' Text
  -> Text
pslBinOp hdl parens op e1 e2 =
  parensIf parens (e1' <> symbol hdl op <> e2')
 where
  e1' = pprPslAssertion hdl True e1
  e2' = pprPslAssertion hdl True e2

pslEdge :: HDL -> ActiveEdge -> Text -> Text
pslEdge SystemVerilog activeEdge clkId = pslEdge Verilog activeEdge clkId
pslEdge Verilog Rising clkId = "posedge " <> clkId
pslEdge Verilog Falling clkId = "negedge " <> clkId
pslEdge VHDL Rising clkId = "rising_edge(" <> clkId <> ")"
pslEdge VHDL Falling clkId = "falling_edge(" <> clkId <> ")"

-- | Taken from IEEE Std 1850-2010a, Annex B.1, p149
symbol :: HDL -> Symbol -> Text
symbol SystemVerilog = symbol Verilog
symbol Verilog = \case
  TImpliesOverlapping -> "|->"
  TImplies  -> "|=>"
  Implies   -> "->"
  BiImplies -> "<->"
  Not       -> "!"
  And       -> "&&"
  Or        -> "||"
  To        -> ":"
  Assign    -> "<="
  Is        -> "="
  Equals    -> "=="

symbol VHDL = \case
  TImpliesOverlapping -> "|->"
  TImplies  -> "|=>"
  Implies   -> " -> "
  BiImplies -> " <-> "
  Not       -> "not"
  And       -> " and "
  Or        -> " or "
  To        -> " to "
  Assign    -> "<="
  Is        -> "is"
  Equals    -> "="

-- | Pretty print Property. Doesn't print valid HDL, but can be used for
-- debugging purposes.
pprProperty :: Property dom -> Declaration
pprProperty (Property prop0) =
  let prop1 = fromMaybe "__autogen__" . fst <$> prop0 in
  pprPslProperty VHDL "prop" "clk" Rising prop1

pprPslProperty
  :: HDL
  -- ^ HDL to generate PSL expression for
  -> Text
  -- ^ Property name
  -> Text
  -- ^ Clock name
  -> ActiveEdge
  -- ^ Edge property should be sensitive to
  -> Property' Text
  -- ^ Assertion / Cover statement
  -> Declaration
pprPslProperty hdl propName clkId edge assertion = TickDecl . Comment $
  "psl property " <> propName <> " " <> symbol hdl Is <> "\n" <>
  "(" <> prop <> ") @(" <> pslEdge hdl edge clkId <> ")" <>
  ";\n" <> "psl " <> coverOrAssert <> " " <>
  propName <> ";"
 where
  (coverOrAssert, prop) =
    case assertion of
      CvCover e -> ("cover", pprPslAssertion hdl False e)
      CvAssert e -> ("assert", pprPslAssertion hdl False e)
      CvAssume e -> ("assume", pprPslAssertion hdl False e)

pprPslAssertion :: HDL -> Bool -> Assertion' Text -> Text
pprPslAssertion hdl parens e =
  case e of
    (CvPure p) -> p

    -- ModelSim/QuastaSim doesn't support booleans in PSL. Anytime we want to
    -- use a boolean literal we use (0 == 0) or (0 == 1) instead.
    (CvLit False) -> parensIf parens ("0" <> symbol hdl Equals <> "1")
    (CvLit True) -> parensIf parens ("0" <> symbol hdl Equals <> "0")

    (CvNot e1) ->
      parensIf parens (symbol hdl Not <> " " <> pprPslAssertion hdl True e1)
    (CvAnd e1 e2) -> pslBinOp1 And e1 e2
    (CvOr e1 e2) -> pslBinOp1 Or e1 e2
    (CvImplies e1 e2) -> pslBinOp1 Implies e1 e2

    (CvToTemporal e1) -> "{" <> pprPslAssertion hdl False e1 <> "}"

    (CvNext 0 e1) -> pprPslAssertion hdl parens e1
    (CvNext 1 e1) -> " ## " <> pprPslAssertion hdl True e1
    (CvNext n e1) -> " ##" <> Text.pack (show n) <> " " <> pprPslAssertion hdl False e1

    (CvBefore _ _) -> "{" <> afters1 <> "}"
     where
      afters0 = map (pprPslAssertion hdl False) (squashBefore e)
      afters1 = foldl1 (\e1 e2 -> e1 <> "; " <> e2) afters0

    (CvTemporalImplies 0 e1 e2) -> pslBinOp1 TImpliesOverlapping e1 e2
    (CvTemporalImplies 1 e1 e2) -> pslBinOp1 TImplies e1 e2
    (CvTemporalImplies n e1 e2) -> pslBinOp1 TImplies e1 (CvNext n e2)

    (CvAlways e1) -> "always " <> pprPslAssertion hdl True e1
    (CvNever e1) -> "never " <> pprPslAssertion hdl True e1
    (CvEventually e1) -> "eventually! " <> pprPslAssertion hdl True e1
 where
  pslBinOp1 = pslBinOp hdl True


---------------------------------------
--                SVA                --
---------------------------------------
svaEdge :: ActiveEdge -> Text -> Text
svaEdge Rising clkId = "posedge " <> clkId
svaEdge Falling clkId = "negedge " <> clkId

svaBinOp
  :: Bool
  -> Symbol
  -> Assertion' Text
  -> Assertion' Text
  -> Text
svaBinOp parens op e1 e2 =
  parensIf parens (e1' <> symbol SystemVerilog op <> e2')
 where
  e1' = pprSvaAssertion True e1
  e2' = pprSvaAssertion True e2

pprSvaAssertion :: Bool -> Assertion' Text -> Text
pprSvaAssertion parens e =
  case e of
    (CvPure p) -> p
    (CvLit False) -> "false"
    (CvLit True) -> "true"

    (CvNot e1) ->
      parensIf parens (symbol' Not <> pprSvaAssertion True e1)
    (CvAnd e1 e2) -> svaBinOp1 And e1 e2
    (CvOr e1 e2) -> svaBinOp1 Or e1 e2
    (CvImplies e1 e2) -> svaBinOp1 Implies e1 e2

    (CvToTemporal e1) -> "{" <> pprSvaAssertion False e1 <> "}"

    (CvNext 0 e1) -> pprSvaAssertion parens e1
    (CvNext n e1) -> "nexttime[" <> Text.pack (show n) <> "] " <> pprSvaAssertion False e1

    (CvBefore _ _) -> "{" <> afters1 <> "}"
     where
      afters0 = map (pprSvaAssertion False) (squashBefore e)
      afters1 = foldl1 (\e1 e2 -> "(" <> e1 <> ") ##1 (" <> e2 <> ")") afters0

    (CvTemporalImplies 0 e1 e2) -> svaBinOp1 TImpliesOverlapping e1 e2
    (CvTemporalImplies 1 e1 e2) -> svaBinOp1 TImplies e1 e2
    (CvTemporalImplies n e1 e2) -> svaBinOp1 TImplies e1 (CvNext n e2)

    (CvAlways e1) -> "always (" <> pprSvaAssertion False e1 <> ")"
    (CvNever _e) -> error "'never' not supported in SVA"
    (CvEventually e1) -> "s_eventually (" <> pprSvaAssertion False e1 <> ")"
 where
  svaBinOp1 = svaBinOp parens
  symbol' = symbol SystemVerilog

pprSvaProperty
  :: Text
  -- ^ Property name
  -> Text
  -- ^ Clock name
  -> ActiveEdge
  -- ^ Edge property should be sensitive to
  -> Property' Text
  -- ^ Assertion / Cover statement
  -> Declaration
pprSvaProperty propName clkId edge assertion = TickDecl . Comment $
  propName <> ": " <> coverOrAssert <> " property (@(" <>
  svaEdge edge clkId <> ") " <> prop <> ");"
 where
  (coverOrAssert, prop) =
    case assertion of
      CvCover e -> ("cover", pprSvaAssertion False e)
      CvAssert e -> ("assert", pprSvaAssertion False e)
      CvAssume e -> ("assume", pprSvaAssertion False e)

---------------------------------------
--     Yosys Formal Extensions       --
---------------------------------------

-- | Generate something like:
-- @always @(posedge clk_i) isOn: cover (result);@
pprYosysSvaProperty
  :: Text
  -- ^ Property name
  -> Expr
  -- ^ Clock expression
  -> ActiveEdge
  -- ^ Edge property should be sensitive to
  -> Property' Text
  -- ^ Assertion / Cover statement
  -> Declaration
pprYosysSvaProperty propName clk edge assertion = ConditionalDecl
  "FORMAL"
  [Seq [AlwaysClocked edge clk [SeqDecl (TickDecl directive)]]]
 where
  directive = Directive
    (propName <> ": " <> coverOrAssert <> " property (" <> prop <> ")")

  (coverOrAssert, prop) = case assertion of
    CvCover  e -> ("cover", pprSvaAssertion False e)
    CvAssert e -> ("assert", pprSvaAssertion False e)
    CvAssume e -> ("assume", pprSvaAssertion False e)