{-# LANGUAGE QuasiQuotes #-}

-- |
-- Module      : Verismith.EMI
-- Description : Definition of the circuit graph.
-- Copyright   : (c) 2021, Yann Herklotz
-- License     : GPL-3
-- Maintainer  : yann [at] yannherklotz [dot] com
-- Stability   : experimental
-- Portability : POSIX
--
-- Equivalence modulo inputs (EMI) testing.  This file should get an existing design, and spit out a
-- modified design that is equivalent under some specific values of the extra inputs.
module Verismith.EMI where

import Control.Lens hiding (Context)
import Control.Monad (replicateM)
import Control.Monad.Reader
import Control.Monad.State.Strict
import Data.List (intercalate)
import Data.Maybe (fromMaybe)
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.Text.IO as T
import Hedgehog (Gen, GenT, MonadGen)
import qualified Hedgehog as Hog
import qualified Hedgehog.Gen as Hog
import qualified Hedgehog.Range as HogR
import Verismith.Config
import Verismith.Generate
import Verismith.Utils
import Verismith.Verilog.AST
import Verismith.Verilog.BitVec
import Verismith.Verilog.CodeGen
import Verismith.Verilog.Eval
import Verismith.Verilog.Internal
import Verismith.Verilog.Mutate
import Verismith.Verilog.Quote

data EMIInputs a
  = EMIInputs [Identifier]
  | EMIOrig a
  deriving (EMIInputs a -> EMIInputs a -> Bool
(EMIInputs a -> EMIInputs a -> Bool)
-> (EMIInputs a -> EMIInputs a -> Bool) -> Eq (EMIInputs a)
forall a. Eq a => EMIInputs a -> EMIInputs a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => EMIInputs a -> EMIInputs a -> Bool
== :: EMIInputs a -> EMIInputs a -> Bool
$c/= :: forall a. Eq a => EMIInputs a -> EMIInputs a -> Bool
/= :: EMIInputs a -> EMIInputs a -> Bool
Eq, Eq (EMIInputs a)
Eq (EMIInputs a) =>
(EMIInputs a -> EMIInputs a -> Ordering)
-> (EMIInputs a -> EMIInputs a -> Bool)
-> (EMIInputs a -> EMIInputs a -> Bool)
-> (EMIInputs a -> EMIInputs a -> Bool)
-> (EMIInputs a -> EMIInputs a -> Bool)
-> (EMIInputs a -> EMIInputs a -> EMIInputs a)
-> (EMIInputs a -> EMIInputs a -> EMIInputs a)
-> Ord (EMIInputs a)
EMIInputs a -> EMIInputs a -> Bool
EMIInputs a -> EMIInputs a -> Ordering
EMIInputs a -> EMIInputs a -> EMIInputs a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (EMIInputs a)
forall a. Ord a => EMIInputs a -> EMIInputs a -> Bool
forall a. Ord a => EMIInputs a -> EMIInputs a -> Ordering
forall a. Ord a => EMIInputs a -> EMIInputs a -> EMIInputs a
$ccompare :: forall a. Ord a => EMIInputs a -> EMIInputs a -> Ordering
compare :: EMIInputs a -> EMIInputs a -> Ordering
$c< :: forall a. Ord a => EMIInputs a -> EMIInputs a -> Bool
< :: EMIInputs a -> EMIInputs a -> Bool
$c<= :: forall a. Ord a => EMIInputs a -> EMIInputs a -> Bool
<= :: EMIInputs a -> EMIInputs a -> Bool
$c> :: forall a. Ord a => EMIInputs a -> EMIInputs a -> Bool
> :: EMIInputs a -> EMIInputs a -> Bool
$c>= :: forall a. Ord a => EMIInputs a -> EMIInputs a -> Bool
>= :: EMIInputs a -> EMIInputs a -> Bool
$cmax :: forall a. Ord a => EMIInputs a -> EMIInputs a -> EMIInputs a
max :: EMIInputs a -> EMIInputs a -> EMIInputs a
$cmin :: forall a. Ord a => EMIInputs a -> EMIInputs a -> EMIInputs a
min :: EMIInputs a -> EMIInputs a -> EMIInputs a
Ord)

instance (Show a) => Show (EMIInputs a) where
  show :: EMIInputs a -> String
show (EMIInputs [Identifier]
i) = String
"EMI: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (Text -> String
T.unpack (Text -> String) -> (Identifier -> Text) -> Identifier -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identifier -> Text
getIdentifier (Identifier -> String) -> [Identifier] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Identifier]
i)
  show (EMIOrig a
a) = a -> String
forall a. Show a => a -> String
show a
a

newPort' :: Identifier -> StateGen a Port
newPort' :: forall a. Identifier -> StateGen a Port
newPort' Identifier
ident = do
  Identifier
hex <- Text -> Identifier
Identifier (Text -> Identifier) -> (String -> Text) -> String -> Identifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
T.toLower (Text -> Text) -> (String -> Text) -> String -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack (String -> Identifier)
-> ReaderT Config (GenT (State (Context a))) String
-> ReaderT Config (GenT (State (Context a))) Identifier
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range Int
-> ReaderT Config (GenT (State (Context a))) Char
-> ReaderT Config (GenT (State (Context a))) String
forall (m :: * -> *) a. MonadGen m => Range Int -> m a -> m [a]
Hog.list (Int -> Int -> Range Int
forall a. a -> a -> Range a
HogR.constant Int
10 Int
10) ReaderT Config (GenT (State (Context a))) Char
forall (m :: * -> *). MonadGen m => m Char
Hog.hexit
  let p :: Port
p = PortType -> Bool -> Range -> Identifier -> Port
Port PortType
Wire Bool
False (ConstExpr -> ConstExpr -> Range
Range ConstExpr
0 ConstExpr
0) (Identifier
ident Identifier -> Identifier -> Identifier
forall a. Semigroup a => a -> a -> a
<> Identifier
hex)
  (Maybe EMIContext -> Identity (Maybe EMIContext))
-> Context a -> Identity (Context a)
forall a (f :: * -> *).
Functor f =>
(Maybe EMIContext -> f (Maybe EMIContext))
-> Context a -> f (Context a)
emiContext ((Maybe EMIContext -> Identity (Maybe EMIContext))
 -> Context a -> Identity (Context a))
-> (([Port] -> Identity [Port])
    -> Maybe EMIContext -> Identity (Maybe EMIContext))
-> ([Port] -> Identity [Port])
-> Context a
-> Identity (Context a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EMIContext -> Identity EMIContext)
-> Maybe EMIContext -> Identity (Maybe EMIContext)
forall a b (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f b) -> p (Maybe a) (f (Maybe b))
_Just ((EMIContext -> Identity EMIContext)
 -> Maybe EMIContext -> Identity (Maybe EMIContext))
-> (([Port] -> Identity [Port])
    -> EMIContext -> Identity EMIContext)
-> ([Port] -> Identity [Port])
-> Maybe EMIContext
-> Identity (Maybe EMIContext)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Port] -> Identity [Port]) -> EMIContext -> Identity EMIContext
Iso' EMIContext [Port]
emiNewInputs (([Port] -> Identity [Port]) -> Context a -> Identity (Context a))
-> ([Port] -> [Port])
-> ReaderT Config (GenT (State (Context a))) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (Port
p Port -> [Port] -> [Port]
forall a. a -> [a] -> [a]
:)
  Port -> StateGen a Port
forall a. a -> ReaderT Config (GenT (State (Context a))) a
forall (m :: * -> *) a. Monad m => a -> m a
return Port
p

nstatementEMI :: StateGen a (Maybe (Statement a))
nstatementEMI :: forall a. StateGen a (Maybe (Statement a))
nstatementEMI = do
  Config
config <- ReaderT Config (GenT (State (Context a))) Config
forall r (m :: * -> *). MonadReader r m => m r
ask
  [(Int, StateGen a (Maybe (Statement a)))]
-> StateGen a (Maybe (Statement a))
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
Hog.frequency
    [ ( Config
config Config -> Getting Int Config Int -> Int
forall s a. s -> Getting a s a -> a
^. (ConfEMI -> Const Int ConfEMI) -> Config -> Const Int Config
Lens' Config ConfEMI
configEMI ((ConfEMI -> Const Int ConfEMI) -> Config -> Const Int Config)
-> ((Int -> Const Int Int) -> ConfEMI -> Const Int ConfEMI)
-> Getting Int Config Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Const Int Int) -> ConfEMI -> Const Int ConfEMI
Lens' ConfEMI Int
confEMIGenerateProb,
        do
          Statement a
s' <- StateGen a (Statement a)
forall ann. StateGen ann (Statement ann)
statement
          Port
n <- Identifier -> StateGen a Port
forall a. Identifier -> StateGen a Port
newPort' Identifier
"emi_"
          Maybe (Statement a) -> StateGen a (Maybe (Statement a))
forall a. a -> ReaderT Config (GenT (State (Context a))) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Statement a -> Maybe (Statement a)
forall a. a -> Maybe a
Just (Expr -> Maybe (Statement a) -> Maybe (Statement a) -> Statement a
forall a.
Expr -> Maybe (Statement a) -> Maybe (Statement a) -> Statement a
CondStmnt (Identifier -> Expr
Id (Port
n Port -> Getting Identifier Port Identifier -> Identifier
forall s a. s -> Getting a s a -> a
^. Getting Identifier Port Identifier
Lens' Port Identifier
portName)) (Statement a -> Maybe (Statement a)
forall a. a -> Maybe a
Just Statement a
s') Maybe (Statement a)
forall a. Maybe a
Nothing))
      ),
      (Config
config Config -> Getting Int Config Int -> Int
forall s a. s -> Getting a s a -> a
^. (ConfEMI -> Const Int ConfEMI) -> Config -> Const Int Config
Lens' Config ConfEMI
configEMI ((ConfEMI -> Const Int ConfEMI) -> Config -> Const Int Config)
-> ((Int -> Const Int Int) -> ConfEMI -> Const Int ConfEMI)
-> Getting Int Config Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Const Int Int) -> ConfEMI -> Const Int ConfEMI
Lens' ConfEMI Int
confEMINoGenerateProb, Maybe (Statement a) -> StateGen a (Maybe (Statement a))
forall a. a -> ReaderT Config (GenT (State (Context a))) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Statement a)
forall a. Maybe a
Nothing)
    ]

statementEMI :: Statement a -> StateGen a (Statement a)
statementEMI :: forall a. Statement a -> StateGen a (Statement a)
statementEMI (SeqBlock [Statement a]
s) = do
  Maybe (Statement a)
s'' <- StateGen a (Maybe (Statement a))
forall a. StateGen a (Maybe (Statement a))
nstatementEMI
  Statement a -> StateGen a (Statement a)
forall a. a -> ReaderT Config (GenT (State (Context a))) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Statement a -> StateGen a (Statement a))
-> Statement a -> StateGen a (Statement a)
forall a b. (a -> b) -> a -> b
$ [Statement a] -> Statement a
forall a. [Statement a] -> Statement a
SeqBlock ((Maybe (Statement a)
s'' Maybe (Statement a)
-> Getting (Endo [Statement a]) (Maybe (Statement a)) (Statement a)
-> [Statement a]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. Getting (Endo [Statement a]) (Maybe (Statement a)) (Statement a)
forall a b (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f b) -> p (Maybe a) (f (Maybe b))
_Just) [Statement a] -> [Statement a] -> [Statement a]
forall a. [a] -> [a] -> [a]
++ [Statement a]
s)
statementEMI Statement a
s = Statement a -> StateGen a (Statement a)
forall a. a -> ReaderT Config (GenT (State (Context a))) a
forall (m :: * -> *) a. Monad m => a -> m a
return Statement a
s

moditemEMI :: ModItem a -> StateGen a (ModItem a)
moditemEMI :: forall a. ModItem a -> StateGen a (ModItem a)
moditemEMI (Always Statement a
s) = Statement a -> ModItem a
forall a. Statement a -> ModItem a
Always (Statement a -> ModItem a)
-> ReaderT Config (GenT (State (Context a))) (Statement a)
-> ReaderT Config (GenT (State (Context a))) (ModItem a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Statement a
 -> ReaderT Config (GenT (State (Context a))) (Statement a))
-> Statement a
-> ReaderT Config (GenT (State (Context a))) (Statement a)
forall (m :: * -> *) a.
(Monad m, Plated a) =>
(a -> m a) -> a -> m a
transformM Statement a
-> ReaderT Config (GenT (State (Context a))) (Statement a)
forall a. Statement a -> StateGen a (Statement a)
statementEMI Statement a
s
moditemEMI ModItem a
m = ModItem a -> ReaderT Config (GenT (State (Context a))) (ModItem a)
forall a. a -> ReaderT Config (GenT (State (Context a))) a
forall (m :: * -> *) a. Monad m => a -> m a
return ModItem a
m

moddeclEMI :: ModDecl a -> StateGen a (ModDecl (EMIInputs a))
moddeclEMI :: forall a. ModDecl a -> StateGen a (ModDecl (EMIInputs a))
moddeclEMI ModDecl a
m = do
  (Maybe EMIContext -> Identity (Maybe EMIContext))
-> Context a -> Identity (Context a)
forall a (f :: * -> *).
Functor f =>
(Maybe EMIContext -> f (Maybe EMIContext))
-> Context a -> f (Context a)
emiContext ((Maybe EMIContext -> Identity (Maybe EMIContext))
 -> Context a -> Identity (Context a))
-> (([Port] -> Identity [Port])
    -> Maybe EMIContext -> Identity (Maybe EMIContext))
-> ([Port] -> Identity [Port])
-> Context a
-> Identity (Context a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EMIContext -> Identity EMIContext)
-> Maybe EMIContext -> Identity (Maybe EMIContext)
forall a b (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f b) -> p (Maybe a) (f (Maybe b))
_Just ((EMIContext -> Identity EMIContext)
 -> Maybe EMIContext -> Identity (Maybe EMIContext))
-> (([Port] -> Identity [Port])
    -> EMIContext -> Identity EMIContext)
-> ([Port] -> Identity [Port])
-> Maybe EMIContext
-> Identity (Maybe EMIContext)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Port] -> Identity [Port]) -> EMIContext -> Identity EMIContext
Iso' EMIContext [Port]
emiNewInputs (([Port] -> Identity [Port]) -> Context a -> Identity (Context a))
-> [Port] -> ReaderT Config (GenT (State (Context a))) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= []
  ([Port] -> Identity [Port]) -> Context a -> Identity (Context a)
forall a (f :: * -> *).
Functor f =>
([Port] -> f [Port]) -> Context a -> f (Context a)
blocking (([Port] -> Identity [Port]) -> Context a -> Identity (Context a))
-> [Port] -> ReaderT Config (GenT (State (Context a))) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= []
  ([Port] -> Identity [Port]) -> Context a -> Identity (Context a)
forall a (f :: * -> *).
Functor f =>
([Port] -> f [Port]) -> Context a -> f (Context a)
nonblocking (([Port] -> Identity [Port]) -> Context a -> Identity (Context a))
-> [Port] -> ReaderT Config (GenT (State (Context a))) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= []
  ([Port] -> Identity [Port]) -> Context a -> Identity (Context a)
forall a (f :: * -> *).
Functor f =>
([Port] -> f [Port]) -> Context a -> f (Context a)
wires (([Port] -> Identity [Port]) -> Context a -> Identity (Context a))
-> [Port] -> ReaderT Config (GenT (State (Context a))) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= []
  ModDecl a
m' <- LensLike
  (ReaderT Config (GenT (State (Context a))))
  (ModDecl a)
  (ModDecl a)
  (ModItem a)
  (ModItem a)
-> LensLike
     (ReaderT Config (GenT (State (Context a))))
     (ModDecl a)
     (ModDecl a)
     (ModItem a)
     (ModItem a)
forall (f :: * -> *) s t a b.
LensLike f s t a b -> LensLike f s t a b
traverseOf (([ModItem a]
 -> ReaderT Config (GenT (State (Context a))) [ModItem a])
-> ModDecl a
-> ReaderT Config (GenT (State (Context a))) (ModDecl a)
forall a (f :: * -> *).
Applicative f =>
([ModItem a] -> f [ModItem a]) -> ModDecl a -> f (ModDecl a)
modItems (([ModItem a]
  -> ReaderT Config (GenT (State (Context a))) [ModItem a])
 -> ModDecl a
 -> ReaderT Config (GenT (State (Context a))) (ModDecl a))
-> ((ModItem a
     -> ReaderT Config (GenT (State (Context a))) (ModItem a))
    -> [ModItem a]
    -> ReaderT Config (GenT (State (Context a))) [ModItem a])
-> LensLike
     (ReaderT Config (GenT (State (Context a))))
     (ModDecl a)
     (ModDecl a)
     (ModItem a)
     (ModItem a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModItem a
 -> ReaderT Config (GenT (State (Context a))) (ModItem a))
-> [ModItem a]
-> ReaderT Config (GenT (State (Context a))) [ModItem a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse) ModItem a -> ReaderT Config (GenT (State (Context a))) (ModItem a)
forall a. ModItem a -> StateGen a (ModItem a)
moditemEMI ModDecl a
m
  [Port]
c <- Getting [Port] (Context a) [Port]
-> ReaderT Config (GenT (State (Context a))) [Port]
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use ((Maybe EMIContext -> Const [Port] (Maybe EMIContext))
-> Context a -> Const [Port] (Context a)
forall a (f :: * -> *).
Functor f =>
(Maybe EMIContext -> f (Maybe EMIContext))
-> Context a -> f (Context a)
emiContext ((Maybe EMIContext -> Const [Port] (Maybe EMIContext))
 -> Context a -> Const [Port] (Context a))
-> (([Port] -> Const [Port] [Port])
    -> Maybe EMIContext -> Const [Port] (Maybe EMIContext))
-> Getting [Port] (Context a) [Port]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EMIContext -> Const [Port] EMIContext)
-> Maybe EMIContext -> Const [Port] (Maybe EMIContext)
forall a b (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f b) -> p (Maybe a) (f (Maybe b))
_Just ((EMIContext -> Const [Port] EMIContext)
 -> Maybe EMIContext -> Const [Port] (Maybe EMIContext))
-> (([Port] -> Const [Port] [Port])
    -> EMIContext -> Const [Port] EMIContext)
-> ([Port] -> Const [Port] [Port])
-> Maybe EMIContext
-> Const [Port] (Maybe EMIContext)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Port] -> Const [Port] [Port])
-> EMIContext -> Const [Port] EMIContext
Iso' EMIContext [Port]
emiNewInputs)
  [Port]
b <- Getting [Port] (Context a) [Port]
-> ReaderT Config (GenT (State (Context a))) [Port]
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting [Port] (Context a) [Port]
forall a (f :: * -> *).
Functor f =>
([Port] -> f [Port]) -> Context a -> f (Context a)
blocking
  [Port]
nb <- Getting [Port] (Context a) [Port]
-> ReaderT Config (GenT (State (Context a))) [Port]
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting [Port] (Context a) [Port]
forall a (f :: * -> *).
Functor f =>
([Port] -> f [Port]) -> Context a -> f (Context a)
nonblocking
  [Port]
w <- Getting [Port] (Context a) [Port]
-> ReaderT Config (GenT (State (Context a))) [Port]
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting [Port] (Context a) [Port]
forall a (f :: * -> *).
Functor f =>
([Port] -> f [Port]) -> Context a -> f (Context a)
wires
  let m'' :: ModDecl a
m'' = ModDecl a
m' ModDecl a -> (ModDecl a -> ModDecl a) -> ModDecl a
forall a b. a -> (a -> b) -> b
& ([Port] -> Identity [Port]) -> ModDecl a -> Identity (ModDecl a)
forall a (f :: * -> *).
Applicative f =>
([Port] -> f [Port]) -> ModDecl a -> f (ModDecl a)
modInPorts (([Port] -> Identity [Port]) -> ModDecl a -> Identity (ModDecl a))
-> ([Port] -> [Port]) -> ModDecl a -> ModDecl a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ([Port]
c [Port] -> [Port] -> [Port]
forall a. [a] -> [a] -> [a]
++) ModDecl a -> (ModDecl a -> ModDecl a) -> ModDecl a
forall a b. a -> (a -> b) -> b
& [Port] -> ModDecl a -> ModDecl a
forall a. [Port] -> ModDecl a -> ModDecl a
initNewRegs [Port]
c ModDecl a -> (ModDecl a -> ModDecl a) -> ModDecl a
forall a b. a -> (a -> b) -> b
& [Port] -> ModDecl a -> ModDecl a
forall a. [Port] -> ModDecl a -> ModDecl a
initNewInnerRegs ([Port]
b [Port] -> [Port] -> [Port]
forall a. Semigroup a => a -> a -> a
<> [Port]
nb [Port] -> [Port] -> [Port]
forall a. Semigroup a => a -> a -> a
<> [Port]
w)
  ModDecl (EMIInputs a) -> StateGen a (ModDecl (EMIInputs a))
forall a. a -> ReaderT Config (GenT (State (Context a))) a
forall (m :: * -> *) a. Monad m => a -> m a
return (EMIInputs a -> ModDecl (EMIInputs a) -> ModDecl (EMIInputs a)
forall a. a -> ModDecl a -> ModDecl a
ModDeclAnn ([Identifier] -> EMIInputs a
forall a. [Identifier] -> EMIInputs a
EMIInputs ([Port]
c [Port]
-> Getting (Endo [Identifier]) [Port] Identifier -> [Identifier]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (Port -> Const (Endo [Identifier]) Port)
-> [Port] -> Const (Endo [Identifier]) [Port]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((Port -> Const (Endo [Identifier]) Port)
 -> [Port] -> Const (Endo [Identifier]) [Port])
-> ((Identifier -> Const (Endo [Identifier]) Identifier)
    -> Port -> Const (Endo [Identifier]) Port)
-> Getting (Endo [Identifier]) [Port] Identifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Identifier -> Const (Endo [Identifier]) Identifier)
-> Port -> Const (Endo [Identifier]) Port
Lens' Port Identifier
portName)) ((a -> EMIInputs a) -> ModDecl a -> ModDecl (EMIInputs a)
forall a b. (a -> b) -> ModDecl a -> ModDecl b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
x -> a -> EMIInputs a
forall a. a -> EMIInputs a
EMIOrig a
x) ModDecl a
m''))

sourceEMI :: (SourceInfo a) -> StateGen a (SourceInfo (EMIInputs a))
sourceEMI :: forall a. SourceInfo a -> StateGen a (SourceInfo (EMIInputs a))
sourceEMI SourceInfo a
s =
  LensLike
  (ReaderT Config (GenT (State (Context a))))
  (SourceInfo a)
  (SourceInfo (EMIInputs a))
  (ModDecl a)
  (ModDecl (EMIInputs a))
-> LensLike
     (ReaderT Config (GenT (State (Context a))))
     (SourceInfo a)
     (SourceInfo (EMIInputs a))
     (ModDecl a)
     (ModDecl (EMIInputs a))
forall (f :: * -> *) s t a b.
LensLike f s t a b -> LensLike f s t a b
traverseOf ((Verilog a
 -> ReaderT
      Config (GenT (State (Context a))) (Verilog (EMIInputs a)))
-> SourceInfo a
-> ReaderT
     Config (GenT (State (Context a))) (SourceInfo (EMIInputs a))
forall a1 a2 (f :: * -> *).
Functor f =>
(Verilog a1 -> f (Verilog a2))
-> SourceInfo a1 -> f (SourceInfo a2)
infoSrc ((Verilog a
  -> ReaderT
       Config (GenT (State (Context a))) (Verilog (EMIInputs a)))
 -> SourceInfo a
 -> ReaderT
      Config (GenT (State (Context a))) (SourceInfo (EMIInputs a)))
-> ((ModDecl a
     -> ReaderT
          Config (GenT (State (Context a))) (ModDecl (EMIInputs a)))
    -> Verilog a
    -> ReaderT
         Config (GenT (State (Context a))) (Verilog (EMIInputs a)))
-> LensLike
     (ReaderT Config (GenT (State (Context a))))
     (SourceInfo a)
     (SourceInfo (EMIInputs a))
     (ModDecl a)
     (ModDecl (EMIInputs a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([ModDecl a]
 -> ReaderT
      Config (GenT (State (Context a))) [ModDecl (EMIInputs a)])
-> Verilog a
-> ReaderT
     Config (GenT (State (Context a))) (Verilog (EMIInputs a))
(Unwrapped (Verilog a)
 -> ReaderT
      Config
      (GenT (State (Context a)))
      (Unwrapped (Verilog (EMIInputs a))))
-> Verilog a
-> ReaderT
     Config (GenT (State (Context a))) (Verilog (EMIInputs a))
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
Iso
  (Verilog a)
  (Verilog (EMIInputs a))
  (Unwrapped (Verilog a))
  (Unwrapped (Verilog (EMIInputs a)))
_Wrapped (([ModDecl a]
  -> ReaderT
       Config (GenT (State (Context a))) [ModDecl (EMIInputs a)])
 -> Verilog a
 -> ReaderT
      Config (GenT (State (Context a))) (Verilog (EMIInputs a)))
-> ((ModDecl a
     -> ReaderT
          Config (GenT (State (Context a))) (ModDecl (EMIInputs a)))
    -> [ModDecl a]
    -> ReaderT
         Config (GenT (State (Context a))) [ModDecl (EMIInputs a)])
-> (ModDecl a
    -> ReaderT
         Config (GenT (State (Context a))) (ModDecl (EMIInputs a)))
-> Verilog a
-> ReaderT
     Config (GenT (State (Context a))) (Verilog (EMIInputs a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModDecl a
 -> ReaderT
      Config (GenT (State (Context a))) (ModDecl (EMIInputs a)))
-> [ModDecl a]
-> ReaderT
     Config (GenT (State (Context a))) [ModDecl (EMIInputs a)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse) ModDecl a
-> ReaderT
     Config (GenT (State (Context a))) (ModDecl (EMIInputs a))
forall a. ModDecl a -> StateGen a (ModDecl (EMIInputs a))
moddeclEMI SourceInfo a
s

initNewRegs :: [Port] -> ModDecl a -> ModDecl a
initNewRegs :: forall a. [Port] -> ModDecl a -> ModDecl a
initNewRegs [Port]
ps ModDecl a
m = ModDecl a
m ModDecl a -> (ModDecl a -> ModDecl a) -> ModDecl a
forall a b. a -> (a -> b) -> b
& ([ModItem a] -> Identity [ModItem a])
-> ModDecl a -> Identity (ModDecl a)
forall a (f :: * -> *).
Applicative f =>
([ModItem a] -> f [ModItem a]) -> ModDecl a -> f (ModDecl a)
modItems (([ModItem a] -> Identity [ModItem a])
 -> ModDecl a -> Identity (ModDecl a))
-> ([ModItem a] -> [ModItem a]) -> ModDecl a -> ModDecl a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ([ModItem a] -> [ModItem a] -> [ModItem a]
forall a. [a] -> [a] -> [a]
++ (Maybe PortDir -> Port -> Maybe ConstExpr -> ModItem a
forall a. Maybe PortDir -> Port -> Maybe ConstExpr -> ModItem a
Decl (PortDir -> Maybe PortDir
forall a. a -> Maybe a
Just PortDir
PortIn) (Port -> Maybe ConstExpr -> ModItem a)
-> [Port] -> [Maybe ConstExpr -> ModItem a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Port]
ps [Maybe ConstExpr -> ModItem a] -> [Maybe ConstExpr] -> [ModItem a]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe ConstExpr -> [Maybe ConstExpr]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ConstExpr
forall a. Maybe a
Nothing))

initNewInnerRegs :: [Port] -> ModDecl a -> ModDecl a
initNewInnerRegs :: forall a. [Port] -> ModDecl a -> ModDecl a
initNewInnerRegs [Port]
ps ModDecl a
m = ModDecl a
m ModDecl a -> (ModDecl a -> ModDecl a) -> ModDecl a
forall a b. a -> (a -> b) -> b
& ([ModItem a] -> Identity [ModItem a])
-> ModDecl a -> Identity (ModDecl a)
forall a (f :: * -> *).
Applicative f =>
([ModItem a] -> f [ModItem a]) -> ModDecl a -> f (ModDecl a)
modItems (([ModItem a] -> Identity [ModItem a])
 -> ModDecl a -> Identity (ModDecl a))
-> ([ModItem a] -> [ModItem a]) -> ModDecl a -> ModDecl a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ([ModItem a] -> [ModItem a] -> [ModItem a]
forall a. [a] -> [a] -> [a]
++ (Maybe PortDir -> Port -> Maybe ConstExpr -> ModItem a
forall a. Maybe PortDir -> Port -> Maybe ConstExpr -> ModItem a
Decl Maybe PortDir
forall a. Maybe a
Nothing (Port -> Maybe ConstExpr -> ModItem a)
-> [Port] -> [Maybe ConstExpr -> ModItem a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Port]
ps [Maybe ConstExpr -> ModItem a] -> [Maybe ConstExpr] -> [ModItem a]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe ConstExpr -> [Maybe ConstExpr]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ConstExpr
forall a. Maybe a
Nothing))

-- | Procedural generation method for random Verilog. Uses internal 'Reader' and
-- 'State' to keep track of the current Verilog code structure.
proceduralEMI :: SourceInfo a -> Config -> Gen (SourceInfo (EMIInputs a))
proceduralEMI :: forall a. SourceInfo a -> Config -> Gen (SourceInfo (EMIInputs a))
proceduralEMI SourceInfo a
src Config
config = do
  (SourceInfo (EMIInputs a)
mainMod, Context a
st) <-
    Size
-> GenT Identity (SourceInfo (EMIInputs a), Context a)
-> GenT Identity (SourceInfo (EMIInputs a), Context a)
forall (m :: * -> *) a. MonadGen m => Size -> m a -> m a
Hog.resize Size
num (GenT Identity (SourceInfo (EMIInputs a), Context a)
 -> GenT Identity (SourceInfo (EMIInputs a), Context a))
-> GenT Identity (SourceInfo (EMIInputs a), Context a)
-> GenT Identity (SourceInfo (EMIInputs a), Context a)
forall a b. (a -> b) -> a -> b
$
      StateT (Context a) (GenT Identity) (SourceInfo (EMIInputs a))
-> Context a -> GenT Identity (SourceInfo (EMIInputs a), Context a)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
        (GenT (StateT (Context a) Identity) (SourceInfo (EMIInputs a))
-> StateT (Context a) (GenT Identity) (SourceInfo (EMIInputs a))
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(MonadTransDistributive g, Transformer f g m) =>
g (f m) a -> f (g m) a
forall (f :: (* -> *) -> * -> *) (m :: * -> *) a.
Transformer f GenT m =>
GenT (f m) a -> f (GenT m) a
Hog.distributeT (ReaderT
  Config
  (GenT (StateT (Context a) Identity))
  (SourceInfo (EMIInputs a))
-> Config
-> GenT (StateT (Context a) Identity) (SourceInfo (EMIInputs a))
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (SourceInfo a
-> ReaderT
     Config
     (GenT (StateT (Context a) Identity))
     (SourceInfo (EMIInputs a))
forall a. SourceInfo a -> StateGen a (SourceInfo (EMIInputs a))
sourceEMI SourceInfo a
src) Config
config))
        Context a
forall {a}. Context a
context
  SourceInfo (EMIInputs a) -> Gen (SourceInfo (EMIInputs a))
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SourceInfo (EMIInputs a)
mainMod
  where
    context :: Context a
context =
      [Port]
-> [Port]
-> [Port]
-> [Port]
-> [Parameter]
-> [ModDecl a]
-> Int
-> Int
-> Int
-> Bool
-> Maybe EMIContext
-> Context a
forall a.
[Port]
-> [Port]
-> [Port]
-> [Port]
-> [Parameter]
-> [ModDecl a]
-> Int
-> Int
-> Int
-> Bool
-> Maybe EMIContext
-> Context a
Context
        []
        []
        []
        []
        []
        []
        Int
100000
        (((Int -> Const Int Int) -> ConfProperty -> Const Int ConfProperty)
-> Int
forall {a}.
((a -> Const a a) -> ConfProperty -> Const a ConfProperty) -> a
confProp (Int -> Const Int Int) -> ConfProperty -> Const Int ConfProperty
Lens' ConfProperty Int
propStmntDepth)
        (((Int -> Const Int Int) -> ConfProperty -> Const Int ConfProperty)
-> Int
forall {a}.
((a -> Const a a) -> ConfProperty -> Const a ConfProperty) -> a
confProp (Int -> Const Int Int) -> ConfProperty -> Const Int ConfProperty
Lens' ConfProperty Int
propModDepth)
        Bool
True
        (EMIContext -> Maybe EMIContext
forall a. a -> Maybe a
Just ([Port] -> EMIContext
EMIContext []))
    num :: Size
num = Int -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Size) -> Int -> Size
forall a b. (a -> b) -> a -> b
$ ((Int -> Const Int Int) -> ConfProperty -> Const Int ConfProperty)
-> Int
forall {a}.
((a -> Const a a) -> ConfProperty -> Const a ConfProperty) -> a
confProp (Int -> Const Int Int) -> ConfProperty -> Const Int ConfProperty
Lens' ConfProperty Int
propSize
    confProp :: ((a -> Const a a) -> ConfProperty -> Const a ConfProperty) -> a
confProp (a -> Const a a) -> ConfProperty -> Const a ConfProperty
i = Config
config Config -> Getting a Config a -> a
forall s a. s -> Getting a s a -> a
^. (ConfProperty -> Const a ConfProperty) -> Config -> Const a Config
Lens' Config ConfProperty
configProperty ((ConfProperty -> Const a ConfProperty)
 -> Config -> Const a Config)
-> ((a -> Const a a) -> ConfProperty -> Const a ConfProperty)
-> Getting a Config a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Const a a) -> ConfProperty -> Const a ConfProperty
i

proceduralEMIIO :: SourceInfo a -> Config -> IO (SourceInfo (EMIInputs a))
proceduralEMIIO :: forall a. SourceInfo a -> Config -> IO (SourceInfo (EMIInputs a))
proceduralEMIIO SourceInfo a
t = Gen (SourceInfo (EMIInputs a)) -> IO (SourceInfo (EMIInputs a))
forall (m :: * -> *) a. MonadIO m => Gen a -> m a
Hog.sample (Gen (SourceInfo (EMIInputs a)) -> IO (SourceInfo (EMIInputs a)))
-> (Config -> Gen (SourceInfo (EMIInputs a)))
-> Config
-> IO (SourceInfo (EMIInputs a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceInfo a -> Config -> Gen (SourceInfo (EMIInputs a))
forall a. SourceInfo a -> Config -> Gen (SourceInfo (EMIInputs a))
proceduralEMI SourceInfo a
t

-- | Make top level module for equivalence verification. Also takes in how many
-- modules to instantiate.
makeTopEMI :: Int -> ModDecl (EMIInputs ann) -> (ModDecl (EMIInputs ann), [Identifier])
makeTopEMI :: forall ann.
Int
-> ModDecl (EMIInputs ann)
-> (ModDecl (EMIInputs ann), [Identifier])
makeTopEMI Int
i ModDecl (EMIInputs ann)
m' = (Identifier
-> [Port]
-> [Port]
-> [ModItem (EMIInputs ann)]
-> [Parameter]
-> ModDecl (EMIInputs ann)
forall a.
Identifier
-> [Port] -> [Port] -> [ModItem a] -> [Parameter] -> ModDecl a
ModDecl (ModDecl (EMIInputs ann)
m ModDecl (EMIInputs ann)
-> Getting Identifier (ModDecl (EMIInputs ann)) Identifier
-> Identifier
forall s a. s -> Getting a s a -> a
^. Getting Identifier (ModDecl (EMIInputs ann)) Identifier
forall a (f :: * -> *).
Applicative f =>
(Identifier -> f Identifier) -> ModDecl a -> f (ModDecl a)
modId) [Port]
ys [Port]
nports [ModItem (EMIInputs ann)]
modIt [], [Identifier]
anns)
  where
    ys :: [Port]
ys = Identifier -> Port
yPort (Identifier -> Port) -> (Int -> Identifier) -> Int -> Port
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Identifier -> Identifier)
-> Identifier -> Int -> Identifier
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Identifier -> Identifier
forall a. Show a => a -> Identifier -> Identifier
makeIdFrom Identifier
"y" (Int -> Port) -> [Int] -> [Port]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1 .. Int
i]
    modIt :: [ModItem (EMIInputs ann)]
modIt = Bool -> Text -> ModDecl (EMIInputs ann) -> ModItem (EMIInputs ann)
forall ann. Bool -> Text -> ModDecl ann -> ModItem ann
instantiateModSpec_ Bool
True Text
"_" (ModDecl (EMIInputs ann) -> ModItem (EMIInputs ann))
-> (Int -> ModDecl (EMIInputs ann))
-> Int
-> ModItem (EMIInputs ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ModDecl (EMIInputs ann)
forall {a}. Show a => a -> ModDecl (EMIInputs ann)
modN (Int -> ModItem (EMIInputs ann))
-> [Int] -> [ModItem (EMIInputs ann)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1 .. Int
i]
    modN :: a -> ModDecl (EMIInputs ann)
modN a
n =
      ModDecl (EMIInputs ann)
m ModDecl (EMIInputs ann)
-> (ModDecl (EMIInputs ann) -> ModDecl (EMIInputs ann))
-> ModDecl (EMIInputs ann)
forall a b. a -> (a -> b) -> b
& (Identifier -> Identity Identifier)
-> ModDecl (EMIInputs ann) -> Identity (ModDecl (EMIInputs ann))
forall a (f :: * -> *).
Applicative f =>
(Identifier -> f Identifier) -> ModDecl a -> f (ModDecl a)
modId ((Identifier -> Identity Identifier)
 -> ModDecl (EMIInputs ann) -> Identity (ModDecl (EMIInputs ann)))
-> (Identifier -> Identifier)
-> ModDecl (EMIInputs ann)
-> ModDecl (EMIInputs ann)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ a -> Identifier -> Identifier
forall a. Show a => a -> Identifier -> Identifier
makeIdFrom a
n ModDecl (EMIInputs ann)
-> (ModDecl (EMIInputs ann) -> ModDecl (EMIInputs ann))
-> ModDecl (EMIInputs ann)
forall a b. a -> (a -> b) -> b
& ([Port] -> Identity [Port])
-> ModDecl (EMIInputs ann) -> Identity (ModDecl (EMIInputs ann))
forall a (f :: * -> *).
Applicative f =>
([Port] -> f [Port]) -> ModDecl a -> f (ModDecl a)
modOutPorts (([Port] -> Identity [Port])
 -> ModDecl (EMIInputs ann) -> Identity (ModDecl (EMIInputs ann)))
-> [Port] -> ModDecl (EMIInputs ann) -> ModDecl (EMIInputs ann)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ [Identifier -> Port
yPort (a -> Identifier -> Identifier
forall a. Show a => a -> Identifier -> Identifier
makeIdFrom a
n Identifier
"y")]
    anns :: [Identifier]
anns =
      (EMIInputs ann -> [Identifier]) -> [EMIInputs ann] -> [Identifier]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
        ( \EMIInputs ann
x -> case EMIInputs ann
x of
            EMIInputs [Identifier]
x -> [Identifier]
x
            EMIInputs ann
_ -> []
        )
        (ModDecl (EMIInputs ann) -> [EMIInputs ann]
forall a. ModDecl a -> [a]
forall (m :: * -> *) a. Annotations m => m a -> [a]
collectAnn ModDecl (EMIInputs ann)
m')
    m :: ModDecl (EMIInputs ann)
m = ModDecl (EMIInputs ann) -> ModDecl (EMIInputs ann)
forall a. ModDecl a -> ModDecl a
forall (m :: * -> *) a. Annotations m => m a -> m a
removeAnn ModDecl (EMIInputs ann)
m'
    nports :: [Port]
nports = (Port -> Bool) -> [Port] -> [Port]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Port
x -> (Port
x Port -> Getting Identifier Port Identifier -> Identifier
forall s a. s -> Getting a s a -> a
^. Getting Identifier Port Identifier
Lens' Port Identifier
portName) Identifier -> [Identifier] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Identifier]
anns) (ModDecl (EMIInputs ann)
m ModDecl (EMIInputs ann)
-> Getting [Port] (ModDecl (EMIInputs ann)) [Port] -> [Port]
forall s a. s -> Getting a s a -> a
^. Getting [Port] (ModDecl (EMIInputs ann)) [Port]
forall a (f :: * -> *).
Applicative f =>
([Port] -> f [Port]) -> ModDecl a -> f (ModDecl a)
modInPorts)

createProperty :: Identifier -> ModItem a
createProperty :: forall a. Identifier -> ModItem a
createProperty Identifier
i =
  Identifier -> Event -> Maybe Expr -> Expr -> ModItem a
forall a. Identifier -> Event -> Maybe Expr -> Expr -> ModItem a
Property (Identifier
i Identifier -> Identifier -> Identifier
forall a. Semigroup a => a -> a -> a
<> Identifier
"_emi_prop") (Identifier -> Event
EPosEdge Identifier
"clk") Maybe Expr
forall a. Maybe a
Nothing (Expr -> BinaryOperator -> Expr -> Expr
BinOp (Identifier -> Expr
Id Identifier
i) BinaryOperator
BinEq Expr
0)

createAssignment :: Identifier -> Statement a
createAssignment :: forall a. Identifier -> Statement a
createAssignment Identifier
i = Assign -> Statement a
forall a. Assign -> Statement a
BlockAssign (LVal -> Maybe Delay -> Expr -> Assign
Assign (Identifier -> LVal
RegId Identifier
i) Maybe Delay
forall a. Maybe a
Nothing Expr
0)

addAssumesEMI ::
  (ModDecl a, [Identifier]) ->
  (ModDecl a, [Identifier])
addAssumesEMI :: forall a. (ModDecl a, [Identifier]) -> (ModDecl a, [Identifier])
addAssumesEMI (ModDecl a
m, [Identifier]
i) = (ModDecl a
m ModDecl a -> (ModDecl a -> ModDecl a) -> ModDecl a
forall a b. a -> (a -> b) -> b
& ([ModItem a] -> Identity [ModItem a])
-> ModDecl a -> Identity (ModDecl a)
forall a (f :: * -> *).
Applicative f =>
([ModItem a] -> f [ModItem a]) -> ModDecl a -> f (ModDecl a)
modItems (([ModItem a] -> Identity [ModItem a])
 -> ModDecl a -> Identity (ModDecl a))
-> ([ModItem a] -> [ModItem a]) -> ModDecl a -> ModDecl a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ([ModItem a] -> [ModItem a] -> [ModItem a]
forall a. [a] -> [a] -> [a]
++ [ModItem a]
forall {a}. [ModItem a]
mods), [Identifier]
i)
  where
    mods :: [ModItem a]
mods = (Identifier -> ModItem a) -> [Identifier] -> [ModItem a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Identifier -> ModItem a
forall a. Identifier -> ModItem a
createProperty [Identifier]
i

addAssignmentsEMI ::
  (ModDecl a, [Identifier]) ->
  (ModDecl a, [Identifier])
addAssignmentsEMI :: forall a. (ModDecl a, [Identifier]) -> (ModDecl a, [Identifier])
addAssignmentsEMI (ModDecl a
m, [Identifier]
i) = (ModDecl a
m ModDecl a -> (ModDecl a -> ModDecl a) -> ModDecl a
forall a b. a -> (a -> b) -> b
& ([ModItem a] -> Identity [ModItem a])
-> ModDecl a -> Identity (ModDecl a)
forall a (f :: * -> *).
Applicative f =>
([ModItem a] -> f [ModItem a]) -> ModDecl a -> f (ModDecl a)
modItems (([ModItem a] -> Identity [ModItem a])
 -> ModDecl a -> Identity (ModDecl a))
-> ([ModItem a] -> [ModItem a]) -> ModDecl a -> ModDecl a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (ModItem a
forall {a}. ModItem a
mods ModItem a -> [ModItem a] -> [ModItem a]
forall a. a -> [a] -> [a]
:), [Identifier]
i)
  where
    mods :: ModItem a
mods = Statement a -> ModItem a
forall a. Statement a -> ModItem a
Initial ([Statement a] -> Statement a
forall a. [Statement a] -> Statement a
SeqBlock (Identifier -> Statement a
forall a. Identifier -> Statement a
createAssignment (Identifier -> Statement a) -> [Identifier] -> [Statement a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Identifier]
i))

-- | Make a top module with an assert that requires @y_1@ to always be equal to
-- @y_2@, which can then be proven using a formal verification tool.
makeTopAssertEMI :: Bool -> ModDecl (EMIInputs ann) -> (ModDecl (EMIInputs ann), [Identifier])
makeTopAssertEMI :: forall ann.
Bool
-> ModDecl (EMIInputs ann)
-> (ModDecl (EMIInputs ann), [Identifier])
makeTopAssertEMI Bool
b =
  (ModDecl (EMIInputs ann) -> ModDecl (EMIInputs ann))
-> ([Identifier] -> [Identifier])
-> (ModDecl (EMIInputs ann), [Identifier])
-> (ModDecl (EMIInputs ann), [Identifier])
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (([ModItem (EMIInputs ann)] -> Identity [ModItem (EMIInputs ann)])
-> ModDecl (EMIInputs ann) -> Identity (ModDecl (EMIInputs ann))
forall a (f :: * -> *).
Applicative f =>
([ModItem a] -> f [ModItem a]) -> ModDecl a -> f (ModDecl a)
modItems (([ModItem (EMIInputs ann)] -> Identity [ModItem (EMIInputs ann)])
 -> ModDecl (EMIInputs ann) -> Identity (ModDecl (EMIInputs ann)))
-> ([ModItem (EMIInputs ann)] -> [ModItem (EMIInputs ann)])
-> ModDecl (EMIInputs ann)
-> ModDecl (EMIInputs ann)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (ModItem (EMIInputs ann)
forall {a}. ModItem a
assert ModItem (EMIInputs ann)
-> [ModItem (EMIInputs ann)] -> [ModItem (EMIInputs ann)]
forall a. a -> [a] -> [a]
:)) [Identifier] -> [Identifier]
forall a. a -> a
id
    ((ModDecl (EMIInputs ann), [Identifier])
 -> (ModDecl (EMIInputs ann), [Identifier]))
-> (ModDecl (EMIInputs ann)
    -> (ModDecl (EMIInputs ann), [Identifier]))
-> ModDecl (EMIInputs ann)
-> (ModDecl (EMIInputs ann), [Identifier])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if Bool
b then (ModDecl (EMIInputs ann), [Identifier])
-> (ModDecl (EMIInputs ann), [Identifier])
forall a. (ModDecl a, [Identifier]) -> (ModDecl a, [Identifier])
addAssumesEMI else (ModDecl (EMIInputs ann), [Identifier])
-> (ModDecl (EMIInputs ann), [Identifier])
forall a. (ModDecl a, [Identifier]) -> (ModDecl a, [Identifier])
addAssignmentsEMI)
    ((ModDecl (EMIInputs ann), [Identifier])
 -> (ModDecl (EMIInputs ann), [Identifier]))
-> (ModDecl (EMIInputs ann)
    -> (ModDecl (EMIInputs ann), [Identifier]))
-> ModDecl (EMIInputs ann)
-> (ModDecl (EMIInputs ann), [Identifier])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int
-> ModDecl (EMIInputs ann)
-> (ModDecl (EMIInputs ann), [Identifier])
forall ann.
Int
-> ModDecl (EMIInputs ann)
-> (ModDecl (EMIInputs ann), [Identifier])
makeTopEMI Int
2
  where
    assert :: ModItem a
assert =
      Statement a -> ModItem a
forall a. Statement a -> ModItem a
Always (Statement a -> ModItem a)
-> (Statement a -> Statement a) -> Statement a -> ModItem a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Event -> Maybe (Statement a) -> Statement a
forall a. Event -> Maybe (Statement a) -> Statement a
EventCtrl Event
e (Maybe (Statement a) -> Statement a)
-> (Statement a -> Maybe (Statement a))
-> Statement a
-> Statement a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Statement a -> Maybe (Statement a)
forall a. a -> Maybe a
Just (Statement a -> ModItem a) -> Statement a -> ModItem a
forall a b. (a -> b) -> a -> b
$
        [Statement a] -> Statement a
forall a. [Statement a] -> Statement a
SeqBlock
          [Task -> Statement a
forall a. Task -> Statement a
TaskEnable (Task -> Statement a) -> Task -> Statement a
forall a b. (a -> b) -> a -> b
$ Identifier -> [Expr] -> Task
Task Identifier
"assert" [Expr -> BinaryOperator -> Expr -> Expr
BinOp (Identifier -> Expr
Id Identifier
"y_1") BinaryOperator
BinEq (Identifier -> Expr
Id Identifier
"y_2")]]
    e :: Event
e = Identifier -> Event
EPosEdge Identifier
"clk"

initModEMI :: (ModDecl ann, [Identifier]) -> (ModDecl ann)
initModEMI :: forall ann. (ModDecl ann, [Identifier]) -> ModDecl ann
initModEMI (ModDecl ann
m, [Identifier]
i) = ModDecl ann
m ModDecl ann -> (ModDecl ann -> ModDecl ann) -> ModDecl ann
forall a b. a -> (a -> b) -> b
& ([ModItem ann] -> Identity [ModItem ann])
-> ModDecl ann -> Identity (ModDecl ann)
forall a (f :: * -> *).
Applicative f =>
([ModItem a] -> f [ModItem a]) -> ModDecl a -> f (ModDecl a)
modItems (([ModItem ann] -> Identity [ModItem ann])
 -> ModDecl ann -> Identity (ModDecl ann))
-> ([ModItem ann] -> [ModItem ann]) -> ModDecl ann -> ModDecl ann
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (([ModItem ann]
forall {a}. [ModItem a]
out [ModItem ann] -> [ModItem ann] -> [ModItem ann]
forall a. [a] -> [a] -> [a]
++ [ModItem ann]
forall {a}. [ModItem a]
inp [ModItem ann] -> [ModItem ann] -> [ModItem ann]
forall a. [a] -> [a] -> [a]
++ [ModItem ann]
forall {a}. [ModItem a]
other) [ModItem ann] -> [ModItem ann] -> [ModItem ann]
forall a. [a] -> [a] -> [a]
++)
  where
    out :: [ModItem a]
out = Maybe PortDir -> Port -> Maybe ConstExpr -> ModItem a
forall a. Maybe PortDir -> Port -> Maybe ConstExpr -> ModItem a
Decl (PortDir -> Maybe PortDir
forall a. a -> Maybe a
Just PortDir
PortOut) (Port -> Maybe ConstExpr -> ModItem a)
-> [Port] -> [Maybe ConstExpr -> ModItem a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ModDecl ann
m ModDecl ann -> Getting [Port] (ModDecl ann) [Port] -> [Port]
forall s a. s -> Getting a s a -> a
^. Getting [Port] (ModDecl ann) [Port]
forall a (f :: * -> *).
Applicative f =>
([Port] -> f [Port]) -> ModDecl a -> f (ModDecl a)
modOutPorts) [Maybe ConstExpr -> ModItem a] -> [Maybe ConstExpr] -> [ModItem a]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe ConstExpr -> [Maybe ConstExpr]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ConstExpr
forall a. Maybe a
Nothing
    inp :: [ModItem a]
inp = Maybe PortDir -> Port -> Maybe ConstExpr -> ModItem a
forall a. Maybe PortDir -> Port -> Maybe ConstExpr -> ModItem a
Decl (PortDir -> Maybe PortDir
forall a. a -> Maybe a
Just PortDir
PortIn) (Port -> Maybe ConstExpr -> ModItem a)
-> [Port] -> [Maybe ConstExpr -> ModItem a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ModDecl ann
m ModDecl ann -> Getting [Port] (ModDecl ann) [Port] -> [Port]
forall s a. s -> Getting a s a -> a
^. Getting [Port] (ModDecl ann) [Port]
forall a (f :: * -> *).
Applicative f =>
([Port] -> f [Port]) -> ModDecl a -> f (ModDecl a)
modInPorts) [Maybe ConstExpr -> ModItem a] -> [Maybe ConstExpr] -> [ModItem a]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe ConstExpr -> [Maybe ConstExpr]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ConstExpr
forall a. Maybe a
Nothing
    other :: [ModItem a]
other = Maybe PortDir -> Port -> Maybe ConstExpr -> ModItem a
forall a. Maybe PortDir -> Port -> Maybe ConstExpr -> ModItem a
Decl Maybe PortDir
forall a. Maybe a
Nothing (Port -> Maybe ConstExpr -> ModItem a)
-> [Port] -> [Maybe ConstExpr -> ModItem a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Identifier -> Port) -> [Identifier] -> [Port]
forall a b. (a -> b) -> [a] -> [b]
map (\Identifier
i' -> PortType -> Bool -> Range -> Identifier -> Port
Port PortType
Reg Bool
False (ConstExpr -> ConstExpr -> Range
Range ConstExpr
0 ConstExpr
0) Identifier
i') [Identifier]
i [Maybe ConstExpr -> ModItem a] -> [Maybe ConstExpr] -> [ModItem a]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe ConstExpr -> [Maybe ConstExpr]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ConstExpr
forall a. Maybe a
Nothing

getTopEMIIdent :: SourceInfo (EMIInputs a) -> [Identifier]
getTopEMIIdent :: forall a. SourceInfo (EMIInputs a) -> [Identifier]
getTopEMIIdent SourceInfo (EMIInputs a)
s =
  (EMIInputs a -> [Identifier]) -> [EMIInputs a] -> [Identifier]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
    ( \EMIInputs a
x -> case EMIInputs a
x of
        EMIInputs [Identifier]
x -> [Identifier]
x
        EMIInputs a
_ -> []
    )
    (ModDecl (EMIInputs a) -> [EMIInputs a]
forall a. ModDecl a -> [a]
forall (m :: * -> *) a. Annotations m => m a -> [a]
collectAnn (SourceInfo (EMIInputs a)
s SourceInfo (EMIInputs a)
-> Getting
     (ModDecl (EMIInputs a))
     (SourceInfo (EMIInputs a))
     (ModDecl (EMIInputs a))
-> ModDecl (EMIInputs a)
forall s a. s -> Getting a s a -> a
^. Getting
  (ModDecl (EMIInputs a))
  (SourceInfo (EMIInputs a))
  (ModDecl (EMIInputs a))
forall a (f :: * -> *).
Functor f =>
(ModDecl a -> f (ModDecl a)) -> SourceInfo a -> f (SourceInfo a)
mainModule))

-- Test code

m :: SourceInfo ()
m :: SourceInfo ()
m =
  Text -> Verilog () -> SourceInfo ()
forall a. Text -> Verilog a -> SourceInfo a
SourceInfo
    Text
"m"
    [verilog|
module m;
  always @(posedge clk) begin
    if (z == 2) begin
      ry = 2;
    end
    x <= y;
    y <= z;
  end
endmodule

module m2;
  always @(posedge clk) begin
    if (z == 2) begin
      ry = 2;
    end
    x <= y;
    y <= z;
  end
endmodule
|]

p :: (Show a) => ModDecl a -> IO ()
p :: forall a. Show a => ModDecl a -> IO ()
p = Text -> IO ()
T.putStrLn (Text -> IO ()) -> (ModDecl a -> Text) -> ModDecl a -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModDecl a -> Text
forall a. Source a => a -> Text
genSource

p2 :: (Show a) => SourceInfo a -> IO ()
p2 :: forall a. Show a => SourceInfo a -> IO ()
p2 = Text -> IO ()
T.putStrLn (Text -> IO ()) -> (SourceInfo a -> Text) -> SourceInfo a -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceInfo a -> Text
forall a. Source a => a -> Text
genSource

customConfig :: Config
customConfig =
  Config
defaultConfig
    Config -> (Config -> Config) -> Config
forall a b. a -> (a -> b) -> b
& ((ConfEMI -> Identity ConfEMI) -> Config -> Identity Config
Lens' Config ConfEMI
configEMI ((ConfEMI -> Identity ConfEMI) -> Config -> Identity Config)
-> ((Int -> Identity Int) -> ConfEMI -> Identity ConfEMI)
-> (Int -> Identity Int)
-> Config
-> Identity Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Identity Int) -> ConfEMI -> Identity ConfEMI
Lens' ConfEMI Int
confEMIGenerateProb ((Int -> Identity Int) -> Config -> Identity Config)
-> Int -> Config -> Config
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Int
1)
      (Config -> Config) -> (Config -> Config) -> Config -> Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ConfEMI -> Identity ConfEMI) -> Config -> Identity Config
Lens' Config ConfEMI
configEMI ((ConfEMI -> Identity ConfEMI) -> Config -> Identity Config)
-> ((Int -> Identity Int) -> ConfEMI -> Identity ConfEMI)
-> (Int -> Identity Int)
-> Config
-> Identity Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Identity Int) -> ConfEMI -> Identity ConfEMI
Lens' ConfEMI Int
confEMINoGenerateProb ((Int -> Identity Int) -> Config -> Identity Config)
-> Int -> Config -> Config
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Int
0)

top :: IO ()
top = (((ModDecl (EMIInputs ()), [Identifier]) -> ModDecl (EMIInputs ())
forall ann. (ModDecl ann, [Identifier]) -> ModDecl ann
initModEMI ((ModDecl (EMIInputs ()), [Identifier]) -> ModDecl (EMIInputs ()))
-> (SourceInfo (EMIInputs ())
    -> (ModDecl (EMIInputs ()), [Identifier]))
-> SourceInfo (EMIInputs ())
-> ModDecl (EMIInputs ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> ModDecl (EMIInputs ()) -> (ModDecl (EMIInputs ()), [Identifier])
forall ann.
Bool
-> ModDecl (EMIInputs ann)
-> (ModDecl (EMIInputs ann), [Identifier])
makeTopAssertEMI Bool
True (ModDecl (EMIInputs ()) -> (ModDecl (EMIInputs ()), [Identifier]))
-> (SourceInfo (EMIInputs ()) -> ModDecl (EMIInputs ()))
-> SourceInfo (EMIInputs ())
-> (ModDecl (EMIInputs ()), [Identifier])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\SourceInfo (EMIInputs ())
s -> SourceInfo (EMIInputs ())
s SourceInfo (EMIInputs ())
-> Getting
     (ModDecl (EMIInputs ()))
     (SourceInfo (EMIInputs ()))
     (ModDecl (EMIInputs ()))
-> ModDecl (EMIInputs ())
forall s a. s -> Getting a s a -> a
^. Getting
  (ModDecl (EMIInputs ()))
  (SourceInfo (EMIInputs ()))
  (ModDecl (EMIInputs ()))
forall a (f :: * -> *).
Functor f =>
(ModDecl a -> f (ModDecl a)) -> SourceInfo a -> f (SourceInfo a)
mainModule)) (SourceInfo (EMIInputs ()) -> ModDecl (EMIInputs ()))
-> IO (SourceInfo (EMIInputs ())) -> IO (ModDecl (EMIInputs ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceInfo () -> Config -> IO (SourceInfo (EMIInputs ()))
forall a. SourceInfo a -> Config -> IO (SourceInfo (EMIInputs a))
proceduralEMIIO SourceInfo ()
m Config
customConfig) IO (ModDecl (EMIInputs ()))
-> (ModDecl (EMIInputs ()) -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ModDecl (EMIInputs ()) -> IO ()
forall a. Show a => ModDecl a -> IO ()
p

top2 :: IO ()
top2 = SourceInfo () -> Config -> IO (SourceInfo (EMIInputs ()))
forall a. SourceInfo a -> Config -> IO (SourceInfo (EMIInputs a))
proceduralEMIIO SourceInfo ()
m Config
customConfig IO (SourceInfo (EMIInputs ()))
-> (SourceInfo (EMIInputs ()) -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SourceInfo (EMIInputs ()) -> IO ()
forall a. Show a => SourceInfo a -> IO ()
p2