    {-|
    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 :: forall a. Assertion' a -> [Assertion' a]
    squashBefore (CvBefore Assertion' a
    e1 Assertion' a
    e2) = [Assertion' a]
    e1s [Assertion' a] -> [Assertion' a] -> [Assertion' a]
    forall a. [a] -> [a] -> [a]
    ++ [Assertion' a]
    e2s
     where
      e1s :: [Assertion' a]
    e1s = case Assertion' a -> [Assertion' a]
    forall a. Assertion' a -> [Assertion' a]
    squashBefore Assertion' a
    e1 of {[] -> [Assertion' a
    e1]; [Assertion' a]
    es -> [Assertion' a]
    es}
      e2s :: [Assertion' a]
    e2s = case Assertion' a -> [Assertion' a]
    forall a. Assertion' a -> [Assertion' a]
    squashBefore Assertion' a
    e2 of {[] -> [Assertion' a
    e2]; [Assertion' a]
    es -> [Assertion' a]
    es}
    squashBefore Assertion' a
    _ = []

    parensIf :: Bool -> Text -> Text
    parensIf :: Bool -> Text -> Text
    parensIf Bool
    True Text
    s = Text
    "(" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    s Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    ")"
    parensIf Bool
    False Text
    s = Text
    s

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

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

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

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

    -- | Pretty print Property. Doesn't print valid HDL, but can be used for
    -- debugging purposes.
    pprProperty :: Property dom -> Declaration
    pprProperty :: forall (dom :: Domain). Property dom -> Declaration
    pprProperty (Property Property' (Maybe Text, Signal dom Bool)
    prop0) =
      let prop1 :: Property' Text
    prop1 = Text -> Maybe Text -> Text
    forall a. a -> Maybe a -> a
    fromMaybe Text
    "__autogen__" (Maybe Text -> Text)
    -> ((Maybe Text, Signal dom Bool) -> Maybe Text)
    -> (Maybe Text, Signal dom Bool)
    -> Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Maybe Text, Signal dom Bool) -> Maybe Text
    forall a b. (a, b) -> a
    fst ((Maybe Text, Signal dom Bool) -> Text)
    -> Property' (Maybe Text, Signal dom Bool) -> Property' Text
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Property' (Maybe Text, Signal dom Bool)
    prop0 in
      HDL -> Text -> Text -> ActiveEdge -> Property' Text -> Declaration
    pprPslProperty HDL
    VHDL Text
    "prop" Text
    "clk" ActiveEdge
    Rising Property' Text
    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 -> Text -> Text -> ActiveEdge -> Property' Text -> Declaration
    pprPslProperty HDL
    hdl Text
    propName Text
    clkId ActiveEdge
    edge Property' Text
    assertion = CommentOrDirective -> Declaration
    TickDecl (CommentOrDirective -> Declaration)
    -> (Text -> CommentOrDirective) -> Text -> Declaration
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> CommentOrDirective
    Comment (Text -> Declaration) -> Text -> Declaration
    forall a b. (a -> b) -> a -> b
    $
      Text
    "psl property " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    propName Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    " " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> HDL -> Symbol -> Text
    symbol HDL
    hdl Symbol
    Is Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "\n" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <>
      Text
    "(" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    prop Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    ") @(" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> HDL -> ActiveEdge -> Text -> Text
    pslEdge HDL
    hdl ActiveEdge
    edge Text
    clkId Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    ")" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <>
      Text
    ";\n" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "psl " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    coverOrAssert Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    " " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <>
      Text
    propName Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    ";"
     where
      (Text
    coverOrAssert, Text
    prop) =
        case Property' Text
    assertion of
          CvCover Assertion' Text
    e -> (Text
    "cover", HDL -> Bool -> Assertion' Text -> Text
    pprPslAssertion HDL
    hdl Bool
    False Assertion' Text
    e)
          CvAssert Assertion' Text
    e -> (Text
    "assert", HDL -> Bool -> Assertion' Text -> Text
    pprPslAssertion HDL
    hdl Bool
    False Assertion' Text
    e)
          CvAssume Assertion' Text
    e -> (Text
    "assume", HDL -> Bool -> Assertion' Text -> Text
    pprPslAssertion HDL
    hdl Bool
    False Assertion' Text
    e)

    pprPslAssertion :: HDL -> Bool -> Assertion' Text -> Text
    pprPslAssertion :: HDL -> Bool -> Assertion' Text -> Text
    pprPslAssertion HDL
    hdl Bool
    parens Assertion' Text
    e =
      case Assertion' Text
    e of
        (CvPure Text
    p) -> Text
    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 Bool
    False) -> Bool -> Text -> Text
    parensIf Bool
    parens (Text
    "0" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> HDL -> Symbol -> Text
    symbol HDL
    hdl Symbol
    Equals Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "1")
        (CvLit Bool
    True) -> Bool -> Text -> Text
    parensIf Bool
    parens (Text
    "0" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> HDL -> Symbol -> Text
    symbol HDL
    hdl Symbol
    Equals Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "0")

        (CvNot Assertion' Text
    e1) ->
          Bool -> Text -> Text
    parensIf Bool
    parens (HDL -> Symbol -> Text
    symbol HDL
    hdl Symbol
    Not Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    " " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> HDL -> Bool -> Assertion' Text -> Text
    pprPslAssertion HDL
    hdl Bool
    True Assertion' Text
    e1)
        (CvAnd Assertion' Text
    e1 Assertion' Text
    e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
    pslBinOp1 Symbol
    And Assertion' Text
    e1 Assertion' Text
    e2
        (CvOr Assertion' Text
    e1 Assertion' Text
    e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
    pslBinOp1 Symbol
    Or Assertion' Text
    e1 Assertion' Text
    e2
        (CvImplies Assertion' Text
    e1 Assertion' Text
    e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
    pslBinOp1 Symbol
    Implies Assertion' Text
    e1 Assertion' Text
    e2

        (CvToTemporal Assertion' Text
    e1) -> Text
    "{" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> HDL -> Bool -> Assertion' Text -> Text
    pprPslAssertion HDL
    hdl Bool
    False Assertion' Text
    e1 Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "}"

        (CvNext Word
    0 Assertion' Text
    e1) -> HDL -> Bool -> Assertion' Text -> Text
    pprPslAssertion HDL
    hdl Bool
    parens Assertion' Text
    e1
        (CvNext Word
    1 Assertion' Text
    e1) -> Text
    " ## " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> HDL -> Bool -> Assertion' Text -> Text
    pprPslAssertion HDL
    hdl Bool
    True Assertion' Text
    e1
        (CvNext Word
    n Assertion' Text
    e1) -> Text
    " ##" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> String -> Text
    Text.pack (Word -> String
    forall a. Show a => a -> String
    show Word
    n) Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    " " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> HDL -> Bool -> Assertion' Text -> Text
    pprPslAssertion HDL
    hdl Bool
    False Assertion' Text
    e1

        (CvBefore Assertion' Text
    _ Assertion' Text
    _) -> Text
    "{" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    afters1 Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "}"
         where
          afters0 :: [Text]
    afters0 = (Assertion' Text -> Text) -> [Assertion' Text] -> [Text]
    forall a b. (a -> b) -> [a] -> [b]
    map (HDL -> Bool -> Assertion' Text -> Text
    pprPslAssertion HDL
    hdl Bool
    False) (Assertion' Text -> [Assertion' Text]
    forall a. Assertion' a -> [Assertion' a]
    squashBefore Assertion' Text
    e)
          afters1 :: Text
    afters1 = (Text -> Text -> Text) -> [Text] -> Text
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: Type -> Type) a.
    Foldable t =>
    (a -> a -> a) -> t a -> a
    foldl1 (\Text
    e1 Text
    e2 -> Text
    e1 Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "; " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    e2) [Text]
    afters0

        (CvTemporalImplies Word
    0 Assertion' Text
    e1 Assertion' Text
    e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
    pslBinOp1 Symbol
    TImpliesOverlapping Assertion' Text
    e1 Assertion' Text
    e2
        (CvTemporalImplies Word
    1 Assertion' Text
    e1 Assertion' Text
    e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
    pslBinOp1 Symbol
    TImplies Assertion' Text
    e1 Assertion' Text
    e2
        (CvTemporalImplies Word
    n Assertion' Text
    e1 Assertion' Text
    e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
    pslBinOp1 Symbol
    TImplies Assertion' Text
    e1 (Word -> Assertion' Text -> Assertion' Text
    forall a. Word -> Assertion' a -> Assertion' a
    CvNext Word
    n Assertion' Text
    e2)

        (CvAlways Assertion' Text
    e1) -> Text
    "always " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> HDL -> Bool -> Assertion' Text -> Text
    pprPslAssertion HDL
    hdl Bool
    True Assertion' Text
    e1
        (CvNever Assertion' Text
    e1) -> Text
    "never " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> HDL -> Bool -> Assertion' Text -> Text
    pprPslAssertion HDL
    hdl Bool
    True Assertion' Text
    e1
        (CvEventually Assertion' Text
    e1) -> Text
    "eventually! " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> HDL -> Bool -> Assertion' Text -> Text
    pprPslAssertion HDL
    hdl Bool
    True Assertion' Text
    e1
     where
      pslBinOp1 :: Symbol -> Assertion' Text -> Assertion' Text -> Text
    pslBinOp1 = HDL -> Bool -> Symbol -> Assertion' Text -> Assertion' Text -> Text
    pslBinOp HDL
    hdl Bool
    True

    ---------------------------------------
    --                SVA                --
    ---------------------------------------
    svaEdge :: ActiveEdge -> Text -> Text
    svaEdge :: ActiveEdge -> Text -> Text
    svaEdge ActiveEdge
    Rising Text
    clkId = Text
    "posedge " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    clkId
    svaEdge ActiveEdge
    Falling Text
    clkId = Text
    "negedge " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    clkId

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

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

        (CvNot Assertion' Text
    e1) ->
          Bool -> Text -> Text
    parensIf Bool
    parens (Symbol -> Text
    symbol' Symbol
    Not Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Bool -> Assertion' Text -> Text
    pprSvaAssertion Bool
    True Assertion' Text
    e1)
        (CvAnd Assertion' Text
    e1 Assertion' Text
    e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
    svaBinOp1 Symbol
    And Assertion' Text
    e1 Assertion' Text
    e2
        (CvOr Assertion' Text
    e1 Assertion' Text
    e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
    svaBinOp1 Symbol
    Or Assertion' Text
    e1 Assertion' Text
    e2
        (CvImplies Assertion' Text
    e1 Assertion' Text
    e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
    svaBinOp1 Symbol
    Implies Assertion' Text
    e1 Assertion' Text
    e2

        (CvToTemporal Assertion' Text
    e1) -> Text
    "{" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Bool -> Assertion' Text -> Text
    pprSvaAssertion Bool
    False Assertion' Text
    e1 Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "}"

        (CvNext Word
    0 Assertion' Text
    e1) -> Bool -> Assertion' Text -> Text
    pprSvaAssertion Bool
    parens Assertion' Text
    e1
        (CvNext Word
    n Assertion' Text
    e1) -> Text
    "nexttime[" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> String -> Text
    Text.pack (Word -> String
    forall a. Show a => a -> String
    show Word
    n) Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "] " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Bool -> Assertion' Text -> Text
    pprSvaAssertion Bool
    False Assertion' Text
    e1

        (CvBefore Assertion' Text
    _ Assertion' Text
    _) -> Text
    "{" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    afters1 Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "}"
         where
          afters0 :: [Text]
    afters0 = (Assertion' Text -> Text) -> [Assertion' Text] -> [Text]
    forall a b. (a -> b) -> [a] -> [b]
    map (Bool -> Assertion' Text -> Text
    pprSvaAssertion Bool
    False) (Assertion' Text -> [Assertion' Text]
    forall a. Assertion' a -> [Assertion' a]
    squashBefore Assertion' Text
    e)
          afters1 :: Text
    afters1 = (Text -> Text -> Text) -> [Text] -> Text
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: Type -> Type) a.
    Foldable t =>
    (a -> a -> a) -> t a -> a
    foldl1 (\Text
    e1 Text
    e2 -> Text
    "(" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    e1 Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    ") ##1 (" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    e2 Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    ")") [Text]
    afters0

        (CvTemporalImplies Word
    0 Assertion' Text
    e1 Assertion' Text
    e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
    svaBinOp1 Symbol
    TImpliesOverlapping Assertion' Text
    e1 Assertion' Text
    e2
        (CvTemporalImplies Word
    1 Assertion' Text
    e1 Assertion' Text
    e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
    svaBinOp1 Symbol
    TImplies Assertion' Text
    e1 Assertion' Text
    e2
        (CvTemporalImplies Word
    n Assertion' Text
    e1 Assertion' Text
    e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
    svaBinOp1 Symbol
    TImplies Assertion' Text
    e1 (Word -> Assertion' Text -> Assertion' Text
    forall a. Word -> Assertion' a -> Assertion' a
    CvNext Word
    n Assertion' Text
    e2)

        (CvAlways Assertion' Text
    e1) -> Text
    "always (" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Bool -> Assertion' Text -> Text
    pprSvaAssertion Bool
    False Assertion' Text
    e1 Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    ")"
        (CvNever Assertion' Text
    _e) -> String -> Text
    forall a. HasCallStack => String -> a
    error String
    "'never' not supported in SVA"
        (CvEventually Assertion' Text
    e1) -> Text
    "s_eventually (" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Bool -> Assertion' Text -> Text
    pprSvaAssertion Bool
    False Assertion' Text
    e1 Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    ")"
     where
      svaBinOp1 :: Symbol -> Assertion' Text -> Assertion' Text -> Text
    svaBinOp1 = Bool -> Symbol -> Assertion' Text -> Assertion' Text -> Text
    svaBinOp Bool
    parens
      symbol' :: Symbol -> Text
    symbol' = HDL -> Symbol -> Text
    symbol HDL
    SystemVerilog

    pprSvaProperty
      :: Text
      -- ^ Property name
      -> Text
      -- ^ Clock name
      -> ActiveEdge
      -- ^ Edge property should be sensitive to
      -> Property' Text
      -- ^ Assertion / Cover statement
      -> Declaration
    pprSvaProperty :: Text -> Text -> ActiveEdge -> Property' Text -> Declaration
    pprSvaProperty Text
    propName Text
    clkId ActiveEdge
    edge Property' Text
    assertion = CommentOrDirective -> Declaration
    TickDecl (CommentOrDirective -> Declaration)
    -> (Text -> CommentOrDirective) -> Text -> Declaration
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> CommentOrDirective
    Comment (Text -> Declaration) -> Text -> Declaration
    forall a b. (a -> b) -> a -> b
    $
      Text
    propName Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    ": " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    coverOrAssert Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    " property (@(" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <>
      ActiveEdge -> Text -> Text
    svaEdge ActiveEdge
    edge Text
    clkId Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    ") " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    prop Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    ");"
     where
      (Text
    coverOrAssert, Text
    prop) =
        case Property' Text
    assertion of
          CvCover Assertion' Text
    e -> (Text
    "cover", Bool -> Assertion' Text -> Text
    pprSvaAssertion Bool
    False Assertion' Text
    e)
          CvAssert Assertion' Text
    e -> (Text
    "assert", Bool -> Assertion' Text -> Text
    pprSvaAssertion Bool
    False Assertion' Text
    e)
          CvAssume Assertion' Text
    e -> (Text
    "assume", Bool -> Assertion' Text -> Text
    pprSvaAssertion Bool
    False Assertion' Text
    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 :: Text -> Expr -> ActiveEdge -> Property' Text -> Declaration
    pprYosysSvaProperty Text
    propName Expr
    clk ActiveEdge
    edge Property' Text
    assertion = Text -> [Declaration] -> Declaration
    ConditionalDecl
      Text
    "FORMAL"
      [[Seq] -> Declaration
    Seq [ActiveEdge -> Expr -> [Seq] -> Seq
    AlwaysClocked ActiveEdge
    edge Expr
    clk [Declaration -> Seq
    SeqDecl (CommentOrDirective -> Declaration
    TickDecl CommentOrDirective
    directive)]]]
     where
      directive :: CommentOrDirective
    directive = Text -> CommentOrDirective
    Directive
        (Text
    propName Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    ": " Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    coverOrAssert Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    " property (" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    prop Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    ")")

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