{-# OPTIONS_GHC -Wno-unused-top-binds #-}

-- |
-- Module      : Verismith
-- Description : Verismith
-- Copyright   : (c) 2018-2022, Yann Herklotz
-- License     : GPL-3
-- Maintainer  : yann [at] yannherklotz [dot] com
-- Stability   : experimental
-- Portability : POSIX
module Verismith
  ( defaultMain,

    -- * Types
    Opts (..),
    SourceInfo (..),

    -- * Run functions
    runEquivalence,
    runSimulation,
    runReduce,
    draw,

    -- * Verilog generation functions
    procedural,
    proceduralIO,
    proceduralSrc,
    proceduralSrcIO,
    randomMod,

    -- * Extra modules
    module Verismith.Verilog,
    module Verismith.Config,
    module Verismith.Circuit,
    module Verismith.Tool,
    module Verismith.Fuzz,
    module Verismith.Report,
  )
where

import Control.Concurrent
import Control.Lens hiding ((<.>))
import Control.Monad.IO.Class (liftIO)
import Control.Monad.Trans.Reader (runReaderT)
import Data.ByteString (ByteString)
import Data.ByteString.Builder (byteStringHex, toLazyByteString)
import Data.ByteString.Internal (unpackChars)
import qualified Data.ByteString.Lazy as L
import qualified Data.Graph.Inductive as G
import qualified Data.Graph.Inductive.Dot as G
import Data.Maybe (isNothing)
import Data.Text (Text)
import qualified Data.Text as T
import Data.Text.Encoding (decodeUtf8)
import qualified Data.Text.IO as T
import qualified Data.Text.Lazy as LT
import qualified Data.Text.Lazy.IO as LT
import Data.Time
import Hedgehog (Gen)
import qualified Hedgehog.Gen as Hog
import Hedgehog.Internal.Seed (Seed)
import Options.Applicative
import Paths_verismith (getDataDir)
import Shelly hiding (command)
import Shelly.Lifted (liftSh)
import System.Exit (exitFailure, exitSuccess)
import System.IO
import System.Random (randomIO)
import Verismith.Circuit
import Verismith.Config
import Verismith.EMI
import Verismith.Fuzz
import Verismith.Generate
import Verismith.OptParser
import Verismith.Reduce
import Verismith.Report
import Verismith.Result
import Verismith.Shuffle
import Verismith.Tool
import Verismith.Tool.Internal
import Verismith.Utils (generateByteString)
import Verismith.Verilog
import Verismith.Verilog.Distance
import Verismith.Verilog.Parser (parseSourceInfoFile)
import qualified Verismith.Verilog2005 as V2
import Prelude hiding (FilePath)

toFP :: String -> FilePath
toFP :: FilePath -> FilePath
toFP = Text -> FilePath
fromText (Text -> FilePath) -> (FilePath -> Text) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text
T.pack

myForkIO :: IO () -> IO (MVar ())
myForkIO :: IO () -> IO (MVar ())
myForkIO IO ()
io = do
  MVar ()
mvar <- IO (MVar ())
forall a. IO (MVar a)
newEmptyMVar
  ThreadId
_ <- IO () -> (Either SomeException () -> IO ()) -> IO ThreadId
forall a. IO a -> (Either SomeException a -> IO ()) -> IO ThreadId
forkFinally IO ()
io (\Either SomeException ()
_ -> MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ()
mvar ())
  MVar () -> IO (MVar ())
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MVar ()
mvar

logMsg :: Text -> Text -> IO ()
logMsg :: Text -> Text -> IO ()
logMsg Text
level Text
msg = do
  ZonedTime
currentTime <- IO ZonedTime
getZonedTime
  Text -> IO ()
T.putStrLn (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$
    Text
"["
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
level
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"] "
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (TimeLocale -> FilePath -> ZonedTime -> FilePath
forall t. FormatTime t => TimeLocale -> FilePath -> t -> FilePath
formatTime TimeLocale
defaultTimeLocale FilePath
"%H:%M:%S " ZonedTime
currentTime)
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
msg

logInfo :: Text -> IO ()
logInfo :: Text -> IO ()
logInfo = Text -> Text -> IO ()
logMsg Text
"INFO"

logWarn :: Text -> IO ()
logWarn :: Text -> IO ()
logWarn = Text -> Text -> IO ()
logMsg Text
"WARN"

logFatal :: Text -> IO ()
logFatal :: Text -> IO ()
logFatal = Text -> Text -> IO ()
logMsg Text
"FATAL"

getConfig' :: Bool -> Maybe FilePath -> IO Config
getConfig' :: Bool -> Maybe FilePath -> IO Config
getConfig' Bool
strict Maybe FilePath
s = do
  Either Text Config
config <- IO (Either Text Config)
-> (FilePath -> IO (Either Text Config))
-> Maybe FilePath
-> IO (Either Text Config)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO (Either Text Config)
forall {a}. IO (Either a Config)
def (FilePath -> IO (Either Text Config)
parseConfigFile (FilePath -> IO (Either Text Config))
-> (FilePath -> FilePath) -> FilePath -> IO (Either Text Config)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
T.unpack (Text -> FilePath) -> (FilePath -> Text) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text
toTextIgnore) Maybe FilePath
s
  case Either Text Config
config of
    Left Text
errFst -> do
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
strict (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ (Text -> IO ()) -> [Text] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Text -> IO ()
logFatal (Text -> [Text]
T.lines Text
errFst) IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO ()
forall a. IO a
exitFailure
      Either Text Config
relaxedConfig <- IO (Either Text Config)
-> (FilePath -> IO (Either Text Config))
-> Maybe FilePath
-> IO (Either Text Config)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO (Either Text Config)
forall {a}. IO (Either a Config)
def (FilePath -> IO (Either Text Config)
parseConfigFileRelaxed (FilePath -> IO (Either Text Config))
-> (FilePath -> FilePath) -> FilePath -> IO (Either Text Config)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
T.unpack (Text -> FilePath) -> (FilePath -> Text) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text
toTextIgnore) Maybe FilePath
s
      case Either Text Config
relaxedConfig of
        Left Text
errSnd -> do
          (Text -> IO ()) -> [Text] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Text -> IO ()
logFatal ([Text] -> IO ()) -> [Text] -> IO ()
forall a b. (a -> b) -> a -> b
$ Text -> [Text]
T.lines Text
errSnd
          IO Config
forall a. IO a
exitFailure
        Right Config
x -> do
          (Text -> IO ()) -> [Text] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Text -> IO ()
logWarn (Text -> [Text]
T.lines Text
errFst)
          Text -> IO ()
logWarn Text
"Ignoring additional fields"
          Config -> IO Config
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Config
x
    Right Config
x -> Config -> IO Config
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Config
x
  where
    def :: IO (Either a Config)
def = Either a Config -> IO (Either a Config)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Config -> Either a Config
forall a b. b -> Either a b
Right Config
defaultConfig)

getConfig :: Maybe FilePath -> IO Config
getConfig = Bool -> Maybe FilePath -> IO Config
getConfig' Bool
True

getGenerator :: Config -> Text -> Maybe FilePath -> IO (Gen (SourceInfo ()))
getGenerator :: Config -> Text -> Maybe FilePath -> IO (Gen (SourceInfo ()))
getGenerator Config
config Text
top Maybe FilePath
s =
  IO (Gen (SourceInfo ()))
-> (Text -> IO (Gen (SourceInfo ())))
-> Maybe Text
-> IO (Gen (SourceInfo ()))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Gen (SourceInfo ()) -> IO (Gen (SourceInfo ()))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Gen (SourceInfo ()) -> IO (Gen (SourceInfo ())))
-> Gen (SourceInfo ()) -> IO (Gen (SourceInfo ()))
forall a b. (a -> b) -> a -> b
$ Text -> Config -> Gen (SourceInfo ())
forall ann. Text -> Config -> Gen (SourceInfo ann)
proceduralSrc Text
top Config
config) ((SourceInfo () -> Gen (SourceInfo ()))
-> IO (SourceInfo ()) -> IO (Gen (SourceInfo ()))
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SourceInfo () -> Gen (SourceInfo ())
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (IO (SourceInfo ()) -> IO (Gen (SourceInfo ())))
-> (Text -> IO (SourceInfo ())) -> Text -> IO (Gen (SourceInfo ()))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> IO (SourceInfo ())
forall ann. Text -> Text -> IO (SourceInfo ann)
parseSourceInfoFile Text
top) (Maybe Text -> IO (Gen (SourceInfo ())))
-> Maybe Text -> IO (Gen (SourceInfo ()))
forall a b. (a -> b) -> a -> b
$
    FilePath -> Text
toTextIgnore (FilePath -> Text) -> Maybe FilePath -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe FilePath
s

-- | Randomly remove an option by setting it to 0.
randDelete :: Int -> IO Int
randDelete :: Int -> IO Int
randDelete Int
i = do
  Bool
r <- IO Bool
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
  Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ if Bool
r then Int
i else Int
0

randomise :: Config -> IO Config
randomise :: Config -> IO Config
randomise config :: Config
config@(Config ConfEMI
emi Info
a Probability
_ ConfProperty
c GarbageOpts
d [SimDescription]
e [SynthDescription]
f) = do
  Int
mia <- Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbModItem
cm ProbModItem -> Getting Int ProbModItem Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbModItem Int
Lens' ProbModItem Int
probModItemAssign
  Int
misa <- Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbModItem
cm ProbModItem -> Getting Int ProbModItem Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbModItem Int
Lens' ProbModItem Int
probModItemSeqAlways
  Int
mica <- Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbModItem
cm ProbModItem -> Getting Int ProbModItem Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbModItem Int
Lens' ProbModItem Int
probModItemCombAlways
  Int
mii <- Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbModItem
cm ProbModItem -> Getting Int ProbModItem Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbModItem Int
Lens' ProbModItem Int
probModItemInst
  Int
ssb <- Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbStatement
cs ProbStatement -> Getting Int ProbStatement Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbStatement Int
Lens' ProbStatement Int
probStmntBlock
  Int
ssnb <- Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbStatement
cs ProbStatement -> Getting Int ProbStatement Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbStatement Int
Lens' ProbStatement Int
probStmntNonBlock
  Int
ssc <- Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbStatement
cs ProbStatement -> Getting Int ProbStatement Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbStatement Int
Lens' ProbStatement Int
probStmntCond
  Int
ssf <- Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbStatement
cs ProbStatement -> Getting Int ProbStatement Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbStatement Int
Lens' ProbStatement Int
probStmntFor
  Int
en <- Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbExpr
ce ProbExpr -> Getting Int ProbExpr Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbExpr Int
Lens' ProbExpr Int
probExprNum
  Int
keep_out <- Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbMod
cmo ProbMod -> Getting Int ProbMod Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbMod Int
Lens' ProbMod Int
probModDropOutput
  Int
drop_out <- Int -> IO Int
randDelete (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbMod
cmo ProbMod -> Getting Int ProbMod Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbMod Int
Lens' ProbMod Int
probModDropOutput
  Int
ei <- Int -> IO Int
randDelete (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbExpr
ce ProbExpr -> Getting Int ProbExpr Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbExpr Int
Lens' ProbExpr Int
probExprId
  Int
ers <- Int -> IO Int
randDelete (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbExpr
ce ProbExpr -> Getting Int ProbExpr Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbExpr Int
Lens' ProbExpr Int
probExprRangeSelect
  Int
euo <- Int -> IO Int
randDelete (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbExpr
ce ProbExpr -> Getting Int ProbExpr Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbExpr Int
Lens' ProbExpr Int
probExprUnOp
  Int
ebo <- Int -> IO Int
randDelete (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbExpr
ce ProbExpr -> Getting Int ProbExpr Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbExpr Int
Lens' ProbExpr Int
probExprBinOp
  Int
ec <- Int -> IO Int
randDelete (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbExpr
ce ProbExpr -> Getting Int ProbExpr Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbExpr Int
Lens' ProbExpr Int
probExprCond
  Int
eco <- Int -> IO Int
randDelete (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbExpr
ce ProbExpr -> Getting Int ProbExpr Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbExpr Int
Lens' ProbExpr Int
probExprConcat
  Int
estr <- Int -> IO Int
randDelete (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbExpr
ce ProbExpr -> Getting Int ProbExpr Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbExpr Int
Lens' ProbExpr Int
probExprStr
  Int
esgn <- Int -> IO Int
randDelete (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbExpr
ce ProbExpr -> Getting Int ProbExpr Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbExpr Int
Lens' ProbExpr Int
probExprSigned
  Int
eus <- Int -> IO Int
randDelete (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ ProbExpr
ce ProbExpr -> Getting Int ProbExpr Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int ProbExpr Int
Lens' ProbExpr Int
probExprUnsigned
  Config -> IO Config
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Config -> IO Config) -> Config -> IO Config
forall a b. (a -> b) -> a -> b
$
    ConfEMI
-> Info
-> Probability
-> ConfProperty
-> GarbageOpts
-> [SimDescription]
-> [SynthDescription]
-> Config
Config
      ConfEMI
emi
      Info
a
      ( ProbModItem -> ProbStatement -> ProbExpr -> ProbMod -> Probability
Probability
          (Int -> Int -> Int -> Int -> ProbModItem
ProbModItem Int
mia Int
misa Int
mica Int
mii)
          (Int -> Int -> Int -> Int -> ProbStatement
ProbStatement Int
ssb Int
ssnb Int
ssc Int
ssf)
          (Int
-> Int
-> Int
-> Int
-> Int
-> Int
-> Int
-> Int
-> Int
-> Int
-> ProbExpr
ProbExpr Int
en Int
ei Int
ers Int
euo Int
ebo Int
ec Int
eco Int
estr Int
esgn Int
eus)
          (Int -> Int -> ProbMod
ProbMod Int
drop_out Int
keep_out)
      )
      ConfProperty
c
      GarbageOpts
d
      [SimDescription]
e
      [SynthDescription]
f
  where
    cm :: ProbModItem
cm = Config
config Config -> Getting ProbModItem Config ProbModItem -> ProbModItem
forall s a. s -> Getting a s a -> a
^. (Probability -> Const ProbModItem Probability)
-> Config -> Const ProbModItem Config
Lens' Config Probability
configProbability ((Probability -> Const ProbModItem Probability)
 -> Config -> Const ProbModItem Config)
-> ((ProbModItem -> Const ProbModItem ProbModItem)
    -> Probability -> Const ProbModItem Probability)
-> Getting ProbModItem Config ProbModItem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProbModItem -> Const ProbModItem ProbModItem)
-> Probability -> Const ProbModItem Probability
Lens' Probability ProbModItem
probModItem
    cs :: ProbStatement
cs = Config
config Config
-> Getting ProbStatement Config ProbStatement -> ProbStatement
forall s a. s -> Getting a s a -> a
^. (Probability -> Const ProbStatement Probability)
-> Config -> Const ProbStatement Config
Lens' Config Probability
configProbability ((Probability -> Const ProbStatement Probability)
 -> Config -> Const ProbStatement Config)
-> ((ProbStatement -> Const ProbStatement ProbStatement)
    -> Probability -> Const ProbStatement Probability)
-> Getting ProbStatement Config ProbStatement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProbStatement -> Const ProbStatement ProbStatement)
-> Probability -> Const ProbStatement Probability
Lens' Probability ProbStatement
probStmnt
    ce :: ProbExpr
ce = Config
config Config -> Getting ProbExpr Config ProbExpr -> ProbExpr
forall s a. s -> Getting a s a -> a
^. (Probability -> Const ProbExpr Probability)
-> Config -> Const ProbExpr Config
Lens' Config Probability
configProbability ((Probability -> Const ProbExpr Probability)
 -> Config -> Const ProbExpr Config)
-> ((ProbExpr -> Const ProbExpr ProbExpr)
    -> Probability -> Const ProbExpr Probability)
-> Getting ProbExpr Config ProbExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProbExpr -> Const ProbExpr ProbExpr)
-> Probability -> Const ProbExpr Probability
Lens' Probability ProbExpr
probExpr
    cmo :: ProbMod
cmo = Config
config Config -> Getting ProbMod Config ProbMod -> ProbMod
forall s a. s -> Getting a s a -> a
^. (Probability -> Const ProbMod Probability)
-> Config -> Const ProbMod Config
Lens' Config Probability
configProbability ((Probability -> Const ProbMod Probability)
 -> Config -> Const ProbMod Config)
-> ((ProbMod -> Const ProbMod ProbMod)
    -> Probability -> Const ProbMod Probability)
-> Getting ProbMod Config ProbMod
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProbMod -> Const ProbMod ProbMod)
-> Probability -> Const ProbMod Probability
Lens' Probability ProbMod
probMod

handleOpts :: Opts -> IO ()
handleOpts :: Opts -> IO ()
handleOpts (Fuzz Text
o Maybe FilePath
configF Bool
f Bool
k Int
n Bool
nosim Bool
noequiv Bool
noreduction Maybe FilePath
file Text
top Bool
cc Maybe Text
checker) = do
  Config
config <- Maybe FilePath -> IO Config
getConfig Maybe FilePath
configF
  Gen (SourceInfo ())
gen <- Config -> Text -> Maybe FilePath -> IO (Gen (SourceInfo ()))
getGenerator Config
config Text
top Maybe FilePath
file
  FilePath
datadir <- IO FilePath
getDataDir
  [FuzzReport]
_ <-
    FuzzOpts -> Yosys -> Fuzz Sh [FuzzReport] -> IO [FuzzReport]
forall (m :: * -> *) a.
MonadIO m =>
FuzzOpts -> Yosys -> Fuzz Sh a -> m a
runFuzz
      ( Maybe FilePath
-> Bool
-> Bool
-> Int
-> Bool
-> Bool
-> Bool
-> Config
-> FilePath
-> Bool
-> Maybe Text
-> FuzzOpts
FuzzOpts
          (FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just (FilePath -> Maybe FilePath) -> FilePath -> Maybe FilePath
forall a b. (a -> b) -> a -> b
$ Text -> FilePath
fromText Text
o)
          Bool
f
          Bool
k
          Int
n
          Bool
nosim
          Bool
noequiv
          Bool
noreduction
          Config
config
          (FilePath -> FilePath
toFP FilePath
datadir)
          Bool
cc
          Maybe Text
checker
      )
      Yosys
defaultYosys
      (Gen (SourceInfo ()) -> Fuzz Sh [FuzzReport]
forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
Gen (SourceInfo ann) -> Fuzz m [FuzzReport]
fuzzMultiple Gen (SourceInfo ())
gen)
  () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
handleOpts (EMIOpts Text
o Maybe FilePath
configF Bool
f Bool
k Int
n Bool
nosim Bool
noequiv Bool
noreduction Text
top FilePath
file) = do
  Config
config <- Maybe FilePath -> IO Config
getConfig Maybe FilePath
configF
  FilePath
datadir <- IO FilePath
getDataDir
  SourceInfo ()
src <- Text -> Text -> IO (SourceInfo ())
forall ann. Text -> Text -> IO (SourceInfo ann)
parseSourceInfoFile Text
top (FilePath -> Text
T.pack FilePath
file) :: IO (SourceInfo ())
  let gen :: Gen (SourceInfo (EMIInputs ()))
gen = SourceInfo () -> Config -> Gen (SourceInfo (EMIInputs ()))
forall a. SourceInfo a -> Config -> Gen (SourceInfo (EMIInputs a))
proceduralEMI SourceInfo ()
src Config
config
  [FuzzReport]
_ <-
    FuzzOpts -> Yosys -> Fuzz Sh [FuzzReport] -> IO [FuzzReport]
forall (m :: * -> *) a.
MonadIO m =>
FuzzOpts -> Yosys -> Fuzz Sh a -> m a
runFuzz
      ( Maybe FilePath
-> Bool
-> Bool
-> Int
-> Bool
-> Bool
-> Bool
-> Config
-> FilePath
-> Bool
-> Maybe Text
-> FuzzOpts
FuzzOpts
          (FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just (FilePath -> Maybe FilePath) -> FilePath -> Maybe FilePath
forall a b. (a -> b) -> a -> b
$ Text -> FilePath
fromText Text
o)
          Bool
f
          Bool
k
          Int
n
          Bool
nosim
          Bool
noequiv
          Bool
noreduction
          Config
config
          (FilePath -> FilePath
toFP FilePath
datadir)
          Bool
False
          Maybe Text
forall a. Maybe a
Nothing
      )
      Yosys
defaultYosys
      (Gen (SourceInfo (EMIInputs ())) -> Fuzz Sh [FuzzReport]
forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
Gen (SourceInfo (EMIInputs ann)) -> Fuzz m [FuzzReport]
fuzzMultipleEMI Gen (SourceInfo (EMIInputs ()))
gen)
  () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
handleOpts (Generate Maybe FilePath
f Maybe FilePath
c Bool
sf PrintingOpts
popts) = do
  Config
config <- Maybe FilePath -> IO Config
getConfig Maybe FilePath
c
  if Bool
sf
    then do
      Verilog2005
source <- Config -> IO Verilog2005
V2.runGarbageGeneration Config
config
      (ByteString -> IO ())
-> (FilePath -> ByteString -> IO ())
-> Maybe FilePath
-> ByteString
-> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ByteString -> IO ()
L.putStr FilePath -> ByteString -> IO ()
L.writeFile Maybe FilePath
f (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Maybe Word -> PrintingOpts -> Verilog2005 -> ByteString
V2.genSource (Word -> Maybe Word
forall a. a -> Maybe a
Just Word
80) PrintingOpts
popts Verilog2005
source
    else do
      Verilog ()
source <- Text -> Config -> IO (Verilog ())
forall a. Text -> Config -> IO (Verilog a)
proceduralIO Text
"top" Config
config :: IO (Verilog ())
      (Text -> IO ())
-> (FilePath -> Text -> IO ()) -> Maybe FilePath -> Text -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Text -> IO ()
T.putStrLn FilePath -> Text -> IO ()
T.writeFile (Text -> FilePath
T.unpack (Text -> FilePath) -> (FilePath -> Text) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text
toTextIgnore (FilePath -> FilePath) -> Maybe FilePath -> Maybe FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe FilePath
f) (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Verilog () -> Text
forall a. Source a => a -> Text
genSource Verilog ()
source
handleOpts (Parse FilePath
f Maybe FilePath
o Bool
s PrintingOpts
popts) = do
  (Verilog2005
ast, [FilePath]
warns) <- FilePath -> IO (Verilog2005, [FilePath])
V2.parseVerilog2005 (Text -> FilePath
T.unpack (FilePath -> Text
toTextIgnore FilePath
f))
  (FilePath -> IO ()) -> [FilePath] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Handle -> FilePath -> IO ()
hPutStrLn Handle
stderr) [FilePath]
warns
  if [FilePath] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
warns Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
s
    then () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    else FilePath -> IO ()
forall a. HasCallStack => FilePath -> a
error FilePath
"Input file does not comply strictly with the Verilog 2005 standard"
  (ByteString -> IO ())
-> (FilePath -> ByteString -> IO ())
-> Maybe FilePath
-> ByteString
-> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ByteString -> IO ()
L.putStr FilePath -> ByteString -> IO ()
L.writeFile Maybe FilePath
o (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Maybe Word -> PrintingOpts -> Verilog2005 -> ByteString
V2.genSource (Word -> Maybe Word
forall a. a -> Maybe a
Just Word
80) PrintingOpts
popts Verilog2005
ast
handleOpts (ShuffleOpt FilePath
f Text
t Maybe FilePath
o Bool
nshuffle Bool
nrename Bool
noequiv FilePath
equivdir Maybe Text
checker) = do
  FilePath
datadir <- IO FilePath
getDataDir
  Text
verilogSrc <- FilePath -> IO Text
T.readFile FilePath
file
  case Text -> Text -> Either Text (Verilog ())
forall ann. Text -> Text -> Either Text (Verilog ann)
parseVerilog (FilePath -> Text
T.pack FilePath
file) Text
verilogSrc of
    Left Text
l -> Text -> IO ()
forall a. Show a => a -> IO ()
print Text
l
    Right Verilog ()
v -> do
      let sv :: SourceInfo ()
sv = Text -> Verilog () -> SourceInfo ()
forall a. Text -> Verilog a -> SourceInfo a
SourceInfo Text
t Verilog ()
v
      SourceInfo ()
sv' <- Bool -> Bool -> SourceInfo () -> IO (SourceInfo ())
forall a. Bool -> Bool -> SourceInfo a -> IO (SourceInfo a)
runShuffle Bool
nshuffle Bool
nrename SourceInfo ()
sv
      let gv :: GenVerilog (SourceInfo ())
gv = SourceInfo () -> GenVerilog (SourceInfo ())
forall a. a -> GenVerilog a
GenVerilog SourceInfo ()
sv' :: GenVerilog (SourceInfo ())
      if Bool
noequiv
        then () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else do
          Sh () -> IO ()
forall (m :: * -> *) a. MonadIO m => Sh a -> m a
shelly (Sh () -> IO ()) -> Sh () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
            FilePath -> Sh ()
mkdir FilePath
equivdir
            FilePath -> FilePath -> Sh ()
cp FilePath
file (FilePath
equivdir FilePath -> Text -> FilePath
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> Text
fn1)
          FilePath -> FilePath -> IO ()
writeFile (FilePath
equivdir FilePath -> Text -> FilePath
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> Text
fn2) (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ GenVerilog (SourceInfo ()) -> FilePath
forall a. Show a => a -> FilePath
show GenVerilog (SourceInfo ())
gv
          Result Failed ()
res <- Sh (Result Failed ()) -> IO (Result Failed ())
forall (m :: * -> *) a. MonadIO m => Sh a -> m a
shelly (Sh (Result Failed ()) -> IO (Result Failed ()))
-> (ResultT Failed Sh () -> Sh (Result Failed ()))
-> ResultT Failed Sh ()
-> IO (Result Failed ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ResultT Failed Sh () -> Sh (Result Failed ())
forall a (m :: * -> *) b. ResultT a m b -> m (Result a b)
runResultT (ResultT Failed Sh () -> IO (Result Failed ()))
-> ResultT Failed Sh () -> IO (Result Failed ())
forall a b. (a -> b) -> a -> b
$
            FilePath -> ResultT Failed Sh () -> ResultT Failed Sh ()
forall (m :: * -> *) a.
(MonadBaseControl IO m, MonadSh m) =>
FilePath -> m a -> m a
pop FilePath
equivdir (ResultT Failed Sh () -> ResultT Failed Sh ())
-> ResultT Failed Sh () -> ResultT Failed Sh ()
forall a b. (a -> b) -> a -> b
$ do
              Maybe Text
-> FilePath
-> Identity
-> Identity
-> SourceInfo ()
-> ResultT Failed Sh ()
forall a b ann.
(Synthesiser a, Synthesiser b, Show ann) =>
Maybe Text
-> FilePath -> a -> b -> SourceInfo ann -> ResultT Failed Sh ()
runEquiv Maybe Text
checker (FilePath -> FilePath
toFP FilePath
datadir) (Text -> Identity
mkid Text
fn1) (Text -> Identity
mkid Text
fn2) SourceInfo ()
sv'
          case Result Failed ()
res of
            Pass ()
_ -> FilePath -> IO ()
putStrLn FilePath
"Equivalence check passed"
            Fail (EquivFail Maybe CounterEg
_) -> FilePath -> IO ()
putStrLn FilePath
"Equivalence check failed"
            Fail Failed
TimeoutError -> FilePath -> IO ()
putStrLn FilePath
"Equivalence check timed out"
            Fail Failed
_ -> FilePath -> IO ()
putStrLn FilePath
"Equivalence check error"
      case Maybe FilePath
o of
        Maybe FilePath
Nothing -> GenVerilog (SourceInfo ()) -> IO ()
forall a. Show a => a -> IO ()
print GenVerilog (SourceInfo ())
gv
        Just FilePath
o' -> FilePath -> FilePath -> IO ()
writeFile (Text -> FilePath
T.unpack (Text -> FilePath) -> Text -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> Text
toTextIgnore FilePath
o') (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ GenVerilog (SourceInfo ()) -> FilePath
forall a. Show a => a -> FilePath
show GenVerilog (SourceInfo ())
gv
  where
    file :: FilePath
file = Text -> FilePath
T.unpack (Text -> FilePath) -> (FilePath -> Text) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text
toTextIgnore (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
f
    fn1 :: Text
fn1 = Text
"rtl1.v"
    fn2 :: Text
fn2 = Text
"rtl2.v"
    mkid :: Text -> Identity
mkid Text
f = Text -> FilePath -> Identity
Verismith.Tool.Identity Text
"" (Text -> FilePath
fromText Text
f)
handleOpts (Reduce FilePath
f Text
t Maybe FilePath
_ [SynthDescription]
ls' Bool
False) = do
  SourceInfo ()
src <- Text -> Text -> IO (SourceInfo ())
forall ann. Text -> Text -> IO (SourceInfo ann)
parseSourceInfoFile Text
t (FilePath -> Text
toTextIgnore FilePath
f)
  FilePath
datadir <- IO FilePath
getDataDir
  case SynthDescription -> SynthTool
descriptionToSynth (SynthDescription -> SynthTool)
-> [SynthDescription] -> [SynthTool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SynthDescription]
ls' of
    SynthTool
a : SynthTool
b : [SynthTool]
_ -> do
      FilePath -> IO ()
putStrLn FilePath
"Reduce with equivalence check"
      Sh () -> IO ()
forall (m :: * -> *) a. MonadIO m => Sh a -> m a
shelly (Sh () -> IO ()) -> Sh () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        FilePath -> Sh ()
forall (m :: * -> *). MonadSh m => FilePath -> m ()
make FilePath
dir
        FilePath -> Sh () -> Sh ()
forall (m :: * -> *) a.
(MonadBaseControl IO m, MonadSh m) =>
FilePath -> m a -> m a
pop FilePath
dir (Sh () -> Sh ()) -> Sh () -> Sh ()
forall a b. (a -> b) -> a -> b
$ do
          SourceInfo ()
src' <- Maybe Text
-> FilePath
-> SynthTool
-> SynthTool
-> SourceInfo ()
-> Sh (SourceInfo ())
forall a b (m :: * -> *).
(Synthesiser a, Synthesiser b, MonadSh m) =>
Maybe Text
-> FilePath -> a -> b -> SourceInfo () -> m (SourceInfo ())
reduceSynth Maybe Text
forall a. Maybe a
Nothing (FilePath -> FilePath
toFP FilePath
datadir) SynthTool
a SynthTool
b SourceInfo ()
src :: Sh (SourceInfo ())
          FilePath -> Text -> Sh ()
writefile (Text -> FilePath
fromText Text
".." FilePath -> FilePath -> FilePath
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> FilePath
dir FilePath -> Text -> FilePath
forall filepath.
ToFilePath filepath =>
filepath -> Text -> FilePath
<.> Text
"v") (Text -> Sh ()) -> Text -> Sh ()
forall a b. (a -> b) -> a -> b
$ SourceInfo () -> Text
forall a. Source a => a -> Text
genSource SourceInfo ()
src'
    SynthTool
a : [SynthTool]
_ -> do
      FilePath -> IO ()
putStrLn FilePath
"Reduce with synthesis failure"
      Sh () -> IO ()
forall (m :: * -> *) a. MonadIO m => Sh a -> m a
shelly (Sh () -> IO ()) -> Sh () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        FilePath -> Sh ()
forall (m :: * -> *). MonadSh m => FilePath -> m ()
make FilePath
dir
        FilePath -> Sh () -> Sh ()
forall (m :: * -> *) a.
(MonadBaseControl IO m, MonadSh m) =>
FilePath -> m a -> m a
pop FilePath
dir (Sh () -> Sh ()) -> Sh () -> Sh ()
forall a b. (a -> b) -> a -> b
$ do
          SourceInfo ()
src' <- SynthTool -> SourceInfo () -> Sh (SourceInfo ())
forall a (m :: * -> *).
(Synthesiser a, MonadSh m) =>
a -> SourceInfo () -> m (SourceInfo ())
reduceSynthesis SynthTool
a SourceInfo ()
src
          FilePath -> Text -> Sh ()
writefile (Text -> FilePath
fromText Text
".." FilePath -> FilePath -> FilePath
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> FilePath
dir FilePath -> Text -> FilePath
forall filepath.
ToFilePath filepath =>
filepath -> Text -> FilePath
<.> Text
"v") (Text -> Sh ()) -> Text -> Sh ()
forall a b. (a -> b) -> a -> b
$ SourceInfo () -> Text
forall a. Source a => a -> Text
genSource SourceInfo ()
src'
    [SynthTool]
_ -> do
      FilePath -> IO ()
putStrLn FilePath
"Not reducing because no synthesiser was specified"
      () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    dir :: FilePath
dir = Text -> FilePath
fromText Text
"reduce"
handleOpts (Reduce FilePath
f Text
t Maybe FilePath
_ [SynthDescription]
ls' Bool
True) = do
  SourceInfo ()
src <- Text -> Text -> IO (SourceInfo ())
forall ann. Text -> Text -> IO (SourceInfo ann)
parseSourceInfoFile Text
t (FilePath -> Text
toTextIgnore FilePath
f) :: IO (SourceInfo ())
  FilePath
datadir <- IO FilePath
getDataDir
  case SynthDescription -> SynthTool
descriptionToSynth (SynthDescription -> SynthTool)
-> [SynthDescription] -> [SynthTool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SynthDescription]
ls' of
    SynthTool
a : SynthTool
b : [SynthTool]
_ -> do
      FilePath -> IO ()
putStrLn FilePath
"Starting equivalence check"
      Result Failed ()
res <- Sh (Result Failed ()) -> IO (Result Failed ())
forall (m :: * -> *) a. MonadIO m => Sh a -> m a
shelly (Sh (Result Failed ()) -> IO (Result Failed ()))
-> (ResultT Failed Sh () -> Sh (Result Failed ()))
-> ResultT Failed Sh ()
-> IO (Result Failed ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ResultT Failed Sh () -> Sh (Result Failed ())
forall a (m :: * -> *) b. ResultT a m b -> m (Result a b)
runResultT (ResultT Failed Sh () -> IO (Result Failed ()))
-> ResultT Failed Sh () -> IO (Result Failed ())
forall a b. (a -> b) -> a -> b
$ do
        FilePath -> ResultT Failed Sh ()
forall (m :: * -> *). MonadSh m => FilePath -> m ()
make FilePath
dir
        FilePath -> ResultT Failed Sh () -> ResultT Failed Sh ()
forall (m :: * -> *) a.
(MonadBaseControl IO m, MonadSh m) =>
FilePath -> m a -> m a
pop FilePath
dir (ResultT Failed Sh () -> ResultT Failed Sh ())
-> ResultT Failed Sh () -> ResultT Failed Sh ()
forall a b. (a -> b) -> a -> b
$ do
          SynthTool -> SourceInfo () -> ResultT Failed Sh ()
forall ann.
Show ann =>
SynthTool -> SourceInfo ann -> ResultT Failed Sh ()
forall a ann.
(Synthesiser a, Show ann) =>
a -> SourceInfo ann -> ResultT Failed Sh ()
runSynth SynthTool
a SourceInfo ()
src
          SynthTool -> SourceInfo () -> ResultT Failed Sh ()
forall ann.
Show ann =>
SynthTool -> SourceInfo ann -> ResultT Failed Sh ()
forall a ann.
(Synthesiser a, Show ann) =>
a -> SourceInfo ann -> ResultT Failed Sh ()
runSynth SynthTool
b SourceInfo ()
src
          Maybe Text
-> FilePath
-> SynthTool
-> SynthTool
-> SourceInfo ()
-> ResultT Failed Sh ()
forall a b ann.
(Synthesiser a, Synthesiser b, Show ann) =>
Maybe Text
-> FilePath -> a -> b -> SourceInfo ann -> ResultT Failed Sh ()
runEquiv Maybe Text
forall a. Maybe a
Nothing (FilePath -> FilePath
toFP FilePath
datadir) SynthTool
a SynthTool
b SourceInfo ()
src
      case Result Failed ()
res of
        Pass ()
_ -> FilePath -> IO ()
putStrLn FilePath
"Equivalence check passed"
        Fail (EquivFail Maybe CounterEg
_) -> FilePath -> IO ()
putStrLn FilePath
"Equivalence check failed"
        Fail Failed
TimeoutError -> FilePath -> IO ()
putStrLn FilePath
"Equivalence check timed out"
        Fail Failed
_ -> FilePath -> IO ()
putStrLn FilePath
"Equivalence check error"
      () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    [SynthTool]
as -> do
      FilePath -> IO ()
putStrLn FilePath
"Synthesis check"
      Result Failed [()]
_ <- Sh (Result Failed [()]) -> IO (Result Failed [()])
forall (m :: * -> *) a. MonadIO m => Sh a -> m a
shelly (Sh (Result Failed [()]) -> IO (Result Failed [()]))
-> (ResultT Failed Sh [()] -> Sh (Result Failed [()]))
-> ResultT Failed Sh [()]
-> IO (Result Failed [()])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ResultT Failed Sh [()] -> Sh (Result Failed [()])
forall a (m :: * -> *) b. ResultT a m b -> m (Result a b)
runResultT (ResultT Failed Sh [()] -> IO (Result Failed [()]))
-> ResultT Failed Sh [()] -> IO (Result Failed [()])
forall a b. (a -> b) -> a -> b
$ (SynthTool -> ResultT Failed Sh ())
-> [SynthTool] -> ResultT Failed Sh [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((SynthTool -> SourceInfo () -> ResultT Failed Sh ())
-> SourceInfo () -> SynthTool -> ResultT Failed Sh ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip SynthTool -> SourceInfo () -> ResultT Failed Sh ()
forall ann.
Show ann =>
SynthTool -> SourceInfo ann -> ResultT Failed Sh ()
forall a ann.
(Synthesiser a, Show ann) =>
a -> SourceInfo ann -> ResultT Failed Sh ()
runSynth SourceInfo ()
src) [SynthTool]
as
      () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    dir :: FilePath
dir = Text -> FilePath
fromText Text
"equiv"
handleOpts (ConfigOpt Maybe FilePath
c Maybe FilePath
conf Bool
r) = do
  Config
config <- if Bool
r then Maybe FilePath -> IO Config
getConfig Maybe FilePath
conf IO Config -> (Config -> IO Config) -> IO Config
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Config -> IO Config
randomise else Maybe FilePath -> IO Config
getConfig Maybe FilePath
conf
  IO () -> (FilePath -> IO ()) -> Maybe FilePath -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Text -> IO ()
T.putStrLn (Text -> IO ()) -> (Config -> Text) -> Config -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Text
encodeConfig (Config -> IO ()) -> Config -> IO ()
forall a b. (a -> b) -> a -> b
$ Config
config) (FilePath -> Config -> IO ()
`encodeConfigFile` Config
config) (Maybe FilePath -> IO ()) -> Maybe FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$
    Text -> FilePath
T.unpack
      (Text -> FilePath) -> (FilePath -> Text) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text
toTextIgnore
      (FilePath -> FilePath) -> Maybe FilePath -> Maybe FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe FilePath
c
handleOpts (DistanceOpt FilePath
v1 FilePath
v2) = do
  SourceInfo Any
src1 <- Text -> Text -> IO (SourceInfo Any)
forall ann. Text -> Text -> IO (SourceInfo ann)
parseSourceInfoFile (FilePath -> Text
T.pack FilePath
v1) (FilePath -> Text
toTextIgnore FilePath
v1)
  SourceInfo Any
src2 <- Text -> Text -> IO (SourceInfo Any)
forall ann. Text -> Text -> IO (SourceInfo ann)
parseSourceInfoFile (FilePath -> Text
T.pack FilePath
v2) (FilePath -> Text
toTextIgnore FilePath
v2)
  let d :: Int
d = SourceInfo Any -> SourceInfo Any -> Int
forall a. Distance a => a -> a -> Int
distance SourceInfo Any
src1 SourceInfo Any
src2
  FilePath -> IO ()
putStrLn (FilePath
"Distance: " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Int -> FilePath
forall a. Show a => a -> FilePath
show Int
d)
handleOpts (Equiv FilePath
o FilePath
v1 FilePath
v2 Text
top Maybe Text
checker) = do
  FilePath
datadir <- IO FilePath
getDataDir
  SourceInfo ()
src <- Text -> Text -> IO (SourceInfo ())
forall ann. Text -> Text -> IO (SourceInfo ann)
parseSourceInfoFile Text
top (FilePath -> Text
toTextIgnore FilePath
v1) :: IO (SourceInfo ())
  Sh () -> IO ()
forall (m :: * -> *) a. MonadIO m => Sh a -> m a
shelly (Sh () -> IO ()) -> Sh () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    FilePath -> Sh ()
mkdir FilePath
o
    FilePath -> FilePath -> Sh ()
cp FilePath
v1 (FilePath
o FilePath -> Text -> FilePath
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> Text
fn1)
    FilePath -> FilePath -> Sh ()
cp FilePath
v2 (FilePath
o FilePath -> Text -> FilePath
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> Text
fn2)
  Result Failed ()
res <- Sh (Result Failed ()) -> IO (Result Failed ())
forall (m :: * -> *) a. MonadIO m => Sh a -> m a
shelly (Sh (Result Failed ()) -> IO (Result Failed ()))
-> (ResultT Failed Sh () -> Sh (Result Failed ()))
-> ResultT Failed Sh ()
-> IO (Result Failed ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ResultT Failed Sh () -> Sh (Result Failed ())
forall a (m :: * -> *) b. ResultT a m b -> m (Result a b)
runResultT (ResultT Failed Sh () -> IO (Result Failed ()))
-> ResultT Failed Sh () -> IO (Result Failed ())
forall a b. (a -> b) -> a -> b
$
    FilePath -> ResultT Failed Sh () -> ResultT Failed Sh ()
forall (m :: * -> *) a.
(MonadBaseControl IO m, MonadSh m) =>
FilePath -> m a -> m a
pop FilePath
o (ResultT Failed Sh () -> ResultT Failed Sh ())
-> ResultT Failed Sh () -> ResultT Failed Sh ()
forall a b. (a -> b) -> a -> b
$ do
      Maybe Text
-> FilePath
-> Identity
-> Identity
-> SourceInfo ()
-> ResultT Failed Sh ()
forall a b ann.
(Synthesiser a, Synthesiser b, Show ann) =>
Maybe Text
-> FilePath -> a -> b -> SourceInfo ann -> ResultT Failed Sh ()
runEquiv Maybe Text
checker (FilePath -> FilePath
toFP FilePath
datadir) (Text -> Identity
mkid Text
fn1) (Text -> Identity
mkid Text
fn2) SourceInfo ()
src
  case Result Failed ()
res of
    Pass ()
_ -> FilePath -> IO ()
putStrLn FilePath
"Equivalence check passed"
    Fail (EquivFail Maybe CounterEg
_) -> FilePath -> IO ()
putStrLn FilePath
"Equivalence check failed"
    Fail Failed
TimeoutError -> FilePath -> IO ()
putStrLn FilePath
"Equivalence check timed out"
    Fail Failed
_ -> FilePath -> IO ()
putStrLn FilePath
"Equivalence check error"
  where
    fn1 :: Text
fn1 = Text
"rtl1.v"
    fn2 :: Text
fn2 = Text
"rtl2.v"
    mkid :: Text -> Identity
mkid Text
f = Text -> FilePath -> Identity
Verismith.Tool.Identity Text
"" (Text -> FilePath
fromText Text
f)

defaultMain :: IO ()
defaultMain :: IO ()
defaultMain = do
  Opts
optsparsed <- ParserInfo Opts -> IO Opts
forall a. ParserInfo a -> IO a
execParser ParserInfo Opts
opts
  Opts -> IO ()
handleOpts Opts
optsparsed

makeSrcInfo :: (ModDecl ann) -> (SourceInfo ann)
makeSrcInfo :: forall ann. ModDecl ann -> SourceInfo ann
makeSrcInfo ModDecl ann
m = Text -> Verilog ann -> SourceInfo ann
forall a. Text -> Verilog a -> SourceInfo a
SourceInfo (Identifier -> Text
getIdentifier (Identifier -> Text) -> Identifier -> Text
forall a b. (a -> b) -> a -> b
$ ModDecl ann
m ModDecl ann
-> Getting Identifier (ModDecl ann) Identifier -> Identifier
forall s a. s -> Getting a s a -> a
^. Getting Identifier (ModDecl ann) Identifier
forall a (f :: * -> *).
Applicative f =>
(Identifier -> f Identifier) -> ModDecl a -> f (ModDecl a)
modId) ([ModDecl ann] -> Verilog ann
forall a. [ModDecl a] -> Verilog a
Verilog [ModDecl ann
m])

-- | Draw a randomly generated DAG to a dot file and compile it to a png so it
-- can be seen.
draw :: IO ()
draw :: IO ()
draw = do
  Gr Gate ()
gr <- Gen (Gr Gate ()) -> IO (Gr Gate ())
forall (m :: * -> *) a. MonadIO m => Gen a -> m a
Hog.sample (Gen (Gr Gate ()) -> IO (Gr Gate ()))
-> Gen (Gr Gate ()) -> IO (Gr Gate ())
forall a b. (a -> b) -> a -> b
$ Gr Gate () -> Gr Gate ()
forall a b. (Eq a, Eq b) => Gr a b -> Gr a b
rDups (Gr Gate () -> Gr Gate ())
-> (Circuit -> Gr Gate ()) -> Circuit -> Gr Gate ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Circuit -> Gr Gate ()
getCircuit (Circuit -> Gr Gate ())
-> GenT Identity Circuit -> Gen (Gr Gate ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Size -> GenT Identity Circuit -> GenT Identity Circuit
forall (m :: * -> *) a. MonadGen m => Size -> m a -> m a
Hog.resize Size
10 GenT Identity Circuit
randomDAG
  let dot :: FilePath
dot = Dot () -> FilePath
forall a. Dot a -> FilePath
G.showDot (Dot () -> FilePath)
-> (Gr FilePath FilePath -> Dot ())
-> Gr FilePath FilePath
-> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gr FilePath FilePath -> Dot ()
forall (gr :: * -> * -> *).
Graph gr =>
gr FilePath FilePath -> Dot ()
G.fglToDotString (Gr FilePath FilePath -> FilePath)
-> Gr FilePath FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ (Gate -> FilePath)
-> (() -> FilePath) -> Gr Gate () -> Gr FilePath FilePath
forall (gr :: * -> * -> *) a c b d.
DynGraph gr =>
(a -> c) -> (b -> d) -> gr a b -> gr c d
G.nemap Gate -> FilePath
forall a. Show a => a -> FilePath
show (FilePath -> () -> FilePath
forall a b. a -> b -> a
const FilePath
"") Gr Gate ()
gr
  FilePath -> FilePath -> IO ()
writeFile FilePath
"file.dot" FilePath
dot
  Sh () -> IO ()
forall (m :: * -> *) a. MonadIO m => Sh a -> m a
shelly (Sh () -> IO ()) -> Sh () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> [Text] -> Sh ()
run_ FilePath
"dot" [Text
"-Tpng", Text
"-o", Text
"file.png", Text
"file.dot"]

-- | Function to show a bytestring in a hex format.
showBS :: ByteString -> Text
showBS :: ByteString -> Text
showBS = ByteString -> Text
decodeUtf8 (ByteString -> Text)
-> (ByteString -> ByteString) -> ByteString -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
L.toStrict (ByteString -> ByteString)
-> (ByteString -> ByteString) -> ByteString -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Builder -> ByteString
toLazyByteString (Builder -> ByteString)
-> (ByteString -> Builder) -> ByteString -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Builder
byteStringHex

-- | Run a simulation on a random DAG or a random module.
runSimulation :: IO ()
runSimulation :: IO ()
runSimulation = do
  -- gr <- Hog.generate $ rDups <$> Hog.resize 100 (randomDAG :: Gen (G.Gr Gate ()))
  -- let dot = G.showDot . G.fglToDotString $ G.nemap show (const "") gr
  -- writeFile "file.dot" dot
  -- shelly $ run_ "dot" ["-Tpng", "-o", "file.png", "file.dot"]
  -- let circ =
  --       head $ (nestUpTo 30 . generateAST $ Circuit gr) ^.. getVerilog . traverse . getDescription
  [ByteString]
rand <- Maybe Int -> Int -> Int -> IO [ByteString]
generateByteString Maybe Int
forall a. Maybe a
Nothing Int
32 Int
20
  ModDecl ()
rand2 <- Gen (ModDecl ()) -> IO (ModDecl ())
forall (m :: * -> *) a. MonadIO m => Gen a -> m a
Hog.sample (Int -> Int -> Gen (ModDecl ())
forall (m :: * -> *) ann.
MonadGen m =>
Int -> Int -> m (ModDecl ann)
randomMod Int
10 Int
100) :: IO (ModDecl ())
  Result Failed ByteString
val <- Sh (Result Failed ByteString) -> IO (Result Failed ByteString)
forall (m :: * -> *) a. MonadIO m => Sh a -> m a
shelly (Sh (Result Failed ByteString) -> IO (Result Failed ByteString))
-> (ResultSh ByteString -> Sh (Result Failed ByteString))
-> ResultSh ByteString
-> IO (Result Failed ByteString)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ResultSh ByteString -> Sh (Result Failed ByteString)
forall a (m :: * -> *) b. ResultT a m b -> m (Result a b)
runResultT (ResultSh ByteString -> IO (Result Failed ByteString))
-> ResultSh ByteString -> IO (Result Failed ByteString)
forall a b. (a -> b) -> a -> b
$ Icarus -> SourceInfo () -> [ByteString] -> ResultSh ByteString
forall ann.
Show ann =>
Icarus -> SourceInfo ann -> [ByteString] -> ResultSh ByteString
forall a ann.
(Simulator a, Show ann) =>
a -> SourceInfo ann -> [ByteString] -> ResultSh ByteString
runSim Icarus
defaultIcarus (ModDecl () -> SourceInfo ()
forall ann. ModDecl ann -> SourceInfo ann
makeSrcInfo ModDecl ()
rand2) [ByteString]
rand
  case Result Failed ByteString
val of
    Pass ByteString
a -> Text -> IO ()
T.putStrLn (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ ByteString -> Text
showBS ByteString
a
    Result Failed ByteString
_ -> Text -> IO ()
T.putStrLn Text
"Test failed"

-- | Code to be executed on a failure. Also checks if the failure was a timeout,
-- as the timeout command will return the 124 error code if that was the
-- case. In that case, the error will be moved to a different directory.
onFailure :: Text -> RunFailed -> Sh (Result Failed ())
onFailure :: Text -> RunFailed -> Sh (Result Failed ())
onFailure Text
t RunFailed
_ = do
  Int
ex <- Sh Int
lastExitCode
  case Int
ex of
    Int
124 -> do
      Text -> Sh ()
logger Text
"Test TIMEOUT"
      FilePath -> Sh () -> Sh ()
forall a. FilePath -> Sh a -> Sh a
chdir FilePath
".." (Sh () -> Sh ()) -> Sh () -> Sh ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> Sh ()
cp_r (Text -> FilePath
fromText Text
t) (FilePath -> Sh ()) -> FilePath -> Sh ()
forall a b. (a -> b) -> a -> b
$ Text -> FilePath
fromText (Text
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_timeout")
      Result Failed () -> Sh (Result Failed ())
forall a. a -> Sh a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result Failed () -> Sh (Result Failed ()))
-> Result Failed () -> Sh (Result Failed ())
forall a b. (a -> b) -> a -> b
$ Failed -> Result Failed ()
forall a b. a -> Result a b
Fail Failed
EmptyFail
    Int
_ -> do
      Text -> Sh ()
logger Text
"Test FAIL"
      FilePath -> Sh () -> Sh ()
forall a. FilePath -> Sh a -> Sh a
chdir FilePath
".." (Sh () -> Sh ()) -> Sh () -> Sh ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> Sh ()
cp_r (Text -> FilePath
fromText Text
t) (FilePath -> Sh ()) -> FilePath -> Sh ()
forall a b. (a -> b) -> a -> b
$ Text -> FilePath
fromText (Text
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_failed")
      Result Failed () -> Sh (Result Failed ())
forall a. a -> Sh a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result Failed () -> Sh (Result Failed ()))
-> Result Failed () -> Sh (Result Failed ())
forall a b. (a -> b) -> a -> b
$ Failed -> Result Failed ()
forall a b. a -> Result a b
Fail Failed
EmptyFail

checkEquivalence :: (Show ann) => SourceInfo ann -> Text -> IO Bool
checkEquivalence :: forall ann. Show ann => SourceInfo ann -> Text -> IO Bool
checkEquivalence SourceInfo ann
src Text
dir = Sh Bool -> IO Bool
forall (m :: * -> *) a. MonadIO m => Sh a -> m a
shellyFailDir (Sh Bool -> IO Bool) -> Sh Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ do
  FilePath -> Sh ()
mkdir_p (Text -> FilePath
fromText Text
dir)
  Text
curr <- FilePath -> Text
toTextIgnore (FilePath -> Text) -> Sh FilePath -> Sh Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sh FilePath
pwd
  FilePath
datadir <- IO FilePath -> Sh FilePath
forall a. IO a -> Sh a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO FilePath
getDataDir
  Text -> Text -> Sh ()
setenv Text
"VERISMITH_ROOT" Text
curr
  FilePath -> Sh ()
cd (Text -> FilePath
fromText Text
dir)
  Sh Bool -> (RunFailed -> Sh Bool) -> Sh Bool
forall e a. Exception e => Sh a -> (e -> Sh a) -> Sh a
catch_sh
    ((ResultT Failed Sh () -> Sh (Result Failed ())
forall a (m :: * -> *) b. ResultT a m b -> m (Result a b)
runResultT (ResultT Failed Sh () -> Sh (Result Failed ()))
-> ResultT Failed Sh () -> Sh (Result Failed ())
forall a b. (a -> b) -> a -> b
$ Maybe Text
-> FilePath
-> Yosys
-> Vivado
-> SourceInfo ann
-> ResultT Failed Sh ()
forall a b ann.
(Synthesiser a, Synthesiser b, Show ann) =>
Maybe Text
-> FilePath -> a -> b -> SourceInfo ann -> ResultT Failed Sh ()
runEquiv Maybe Text
forall a. Maybe a
Nothing (FilePath -> FilePath
toFP FilePath
datadir) Yosys
defaultYosys Vivado
defaultVivado SourceInfo ann
src) Sh (Result Failed ()) -> Sh Bool -> Sh Bool
forall a b. Sh a -> Sh b -> Sh b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Sh Bool
forall a. a -> Sh a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
    ((\RunFailed
_ -> Bool -> Sh Bool
forall a. a -> Sh a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) :: RunFailed -> Sh Bool)

-- | Run a fuzz run and check if all of the simulators passed by checking if the
-- generated Verilog files are equivalent.
runEquivalence ::
  Maybe Seed ->
  -- | Generator for the Verilog file.
  Gen (Verilog ()) ->
  -- | Name of the folder on each thread.
  Text ->
  -- | Name of the general folder being used.
  Text ->
  -- | Keep flag.
  Bool ->
  -- | Used to track the recursion.
  Int ->
  IO ()
runEquivalence :: Maybe Seed
-> Gen (Verilog ()) -> Text -> Text -> Bool -> Int -> IO ()
runEquivalence Maybe Seed
seed Gen (Verilog ())
gm Text
t Text
d Bool
k Int
i = do
  (Seed
_, Verilog ()
m) <- Sh (Seed, Verilog ()) -> IO (Seed, Verilog ())
forall (m :: * -> *) a. MonadIO m => Sh a -> m a
shelly (Sh (Seed, Verilog ()) -> IO (Seed, Verilog ()))
-> Sh (Seed, Verilog ()) -> IO (Seed, Verilog ())
forall a b. (a -> b) -> a -> b
$ Maybe Seed -> Gen (Verilog ()) -> Sh (Seed, Verilog ())
forall (m :: * -> *) a.
MonadSh m =>
Maybe Seed -> Gen a -> m (Seed, a)
sampleSeed Maybe Seed
seed Gen (Verilog ())
gm
  let srcInfo :: SourceInfo ()
srcInfo = Text -> Verilog () -> SourceInfo ()
forall a. Text -> Verilog a -> SourceInfo a
SourceInfo Text
"top" Verilog ()
m
  [ByteString]
rand <- Maybe Int -> Int -> Int -> IO [ByteString]
generateByteString Maybe Int
forall a. Maybe a
Nothing Int
32 Int
20
  FilePath
datadir <- IO FilePath
getDataDir
  Sh () -> IO ()
forall (m :: * -> *) a. MonadIO m => Sh a -> m a
shellyFailDir (Sh () -> IO ()) -> Sh () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    FilePath -> Sh ()
mkdir_p (Text -> FilePath
fromText Text
d FilePath -> FilePath -> FilePath
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> Text -> FilePath
fromText Text
n)
    Text
curr <- FilePath -> Text
toTextIgnore (FilePath -> Text) -> Sh FilePath -> Sh Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sh FilePath
pwd
    Text -> Text -> Sh ()
setenv Text
"VERISMITH_ROOT" Text
curr
    FilePath -> Sh ()
cd (Text -> FilePath
fromText Text
"output" FilePath -> FilePath -> FilePath
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> Text -> FilePath
fromText Text
n)
    Result Failed ()
_ <-
      Sh (Result Failed ())
-> (RunFailed -> Sh (Result Failed ())) -> Sh (Result Failed ())
forall e a. Exception e => Sh a -> (e -> Sh a) -> Sh a
catch_sh
        ( ResultT Failed Sh () -> Sh (Result Failed ())
forall a (m :: * -> *) b. ResultT a m b -> m (Result a b)
runResultT (ResultT Failed Sh () -> Sh (Result Failed ()))
-> ResultT Failed Sh () -> Sh (Result Failed ())
forall a b. (a -> b) -> a -> b
$
            Maybe Text
-> FilePath
-> Yosys
-> Vivado
-> SourceInfo ()
-> ResultT Failed Sh ()
forall a b ann.
(Synthesiser a, Synthesiser b, Show ann) =>
Maybe Text
-> FilePath -> a -> b -> SourceInfo ann -> ResultT Failed Sh ()
runEquiv Maybe Text
forall a. Maybe a
Nothing (FilePath -> FilePath
toFP FilePath
datadir) Yosys
defaultYosys Vivado
defaultVivado SourceInfo ()
srcInfo
              ResultT Failed Sh ()
-> ResultT Failed Sh () -> ResultT Failed Sh ()
forall a b.
ResultT Failed Sh a -> ResultT Failed Sh b -> ResultT Failed Sh b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sh () -> ResultT Failed Sh ()
forall a. Sh a -> ResultT Failed Sh a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Text -> Sh ()
logger Text
"Test OK")
        )
        ((RunFailed -> Sh (Result Failed ())) -> Sh (Result Failed ()))
-> (RunFailed -> Sh (Result Failed ())) -> Sh (Result Failed ())
forall a b. (a -> b) -> a -> b
$ Text -> RunFailed -> Sh (Result Failed ())
onFailure Text
n
    Result Failed ()
_ <-
      Sh (Result Failed ())
-> (RunFailed -> Sh (Result Failed ())) -> Sh (Result Failed ())
forall e a. Exception e => Sh a -> (e -> Sh a) -> Sh a
catch_sh
        ( ResultT Failed Sh () -> Sh (Result Failed ())
forall a (m :: * -> *) b. ResultT a m b -> m (Result a b)
runResultT (ResultT Failed Sh () -> Sh (Result Failed ()))
-> ResultT Failed Sh () -> Sh (Result Failed ())
forall a b. (a -> b) -> a -> b
$
            Icarus -> SourceInfo () -> [ByteString] -> ResultSh ByteString
forall ann.
Show ann =>
Icarus -> SourceInfo ann -> [ByteString] -> ResultSh ByteString
forall a ann.
(Simulator a, Show ann) =>
a -> SourceInfo ann -> [ByteString] -> ResultSh ByteString
runSim (FilePath -> FilePath -> Icarus
Icarus FilePath
"iverilog" FilePath
"vvp") SourceInfo ()
srcInfo [ByteString]
rand
              ResultSh ByteString
-> (ByteString -> ResultT Failed Sh ()) -> ResultT Failed Sh ()
forall a b.
ResultT Failed Sh a
-> (a -> ResultT Failed Sh b) -> ResultT Failed Sh b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\ByteString
b -> Sh () -> ResultT Failed Sh ()
forall a. Sh a -> ResultT Failed Sh a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> ResultT Failed Sh ()) -> Sh () -> ResultT Failed Sh ()
forall a b. (a -> b) -> a -> b
$ Text -> Sh ()
logger (Text
"RTL Sim: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> ByteString -> Text
showBS ByteString
b))
        )
        ((RunFailed -> Sh (Result Failed ())) -> Sh (Result Failed ()))
-> (RunFailed -> Sh (Result Failed ())) -> Sh (Result Failed ())
forall a b. (a -> b) -> a -> b
$ Text -> RunFailed -> Sh (Result Failed ())
onFailure Text
n
    FilePath -> Sh ()
cd FilePath
".."
    Bool -> Sh () -> Sh ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
k (Sh () -> Sh ()) -> (FilePath -> Sh ()) -> FilePath -> Sh ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Sh ()
rm_rf (FilePath -> Sh ()) -> FilePath -> Sh ()
forall a b. (a -> b) -> a -> b
$ Text -> FilePath
fromText Text
n
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
5 Bool -> Bool -> Bool
&& Maybe Seed -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Seed
seed) (Maybe Seed
-> Gen (Verilog ()) -> Text -> Text -> Bool -> Int -> IO ()
runEquivalence Maybe Seed
seed Gen (Verilog ())
gm Text
t Text
d Bool
k (Int -> IO ()) -> Int -> IO ()
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
  where
    n :: Text
n = Text
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (Int -> FilePath
forall a. Show a => a -> FilePath
show Int
i)

runReduce :: (SourceInfo ()) -> IO (SourceInfo ())
runReduce :: SourceInfo () -> IO (SourceInfo ())
runReduce SourceInfo ()
s =
  Sh (SourceInfo ()) -> IO (SourceInfo ())
forall (m :: * -> *) a. MonadIO m => Sh a -> m a
shelly (Sh (SourceInfo ()) -> IO (SourceInfo ()))
-> Sh (SourceInfo ()) -> IO (SourceInfo ())
forall a b. (a -> b) -> a -> b
$ FilePath
-> (SourceInfo ReduceAnn -> Sh Bool)
-> SourceInfo ()
-> Sh (SourceInfo ())
forall (m :: * -> *).
MonadSh m =>
FilePath
-> (SourceInfo ReduceAnn -> m Bool)
-> SourceInfo ()
-> m (SourceInfo ())
reduce FilePath
"reduce.v" (\SourceInfo ReduceAnn
s' -> Bool -> Bool
not (Bool -> Bool) -> Sh Bool -> Sh Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Bool -> Sh Bool
forall a. IO a -> Sh a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (SourceInfo ReduceAnn -> Text -> IO Bool
forall ann. Show ann => SourceInfo ann -> Text -> IO Bool
checkEquivalence SourceInfo ReduceAnn
s' Text
"reduce")) SourceInfo ()
s