{-|
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 :: 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 :: 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 (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 (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)