{-# LANGUAGE QuasiQuotes #-}

-- |
-- Module      : Verismith.Tool.Yosys
-- Description : Yosys simulator implementation.
-- Copyright   : (c) 2018-2022, Yann Herklotz
-- License     : GPL-3
-- Maintainer  : yann [at] yannherklotz [dot] com
-- Stability   : experimental
-- Portability : POSIX
--
-- Yosys simulator implementation.
module Verismith.Tool.Yosys
  ( Yosys (..),
    defaultYosys,
    runEquiv,
    runEquivYosys,
  )
where

import Control.DeepSeq (NFData, rnf, rwhnf)
import Control.Lens
import Control.Monad (void)
import Data.Either (fromRight)
import Data.Text (Text, unpack)
import Shelly (FilePath, (</>))
import qualified Shelly as S
import Shelly.Lifted (liftSh, readfile)
import Verismith.CounterEg (parseCounterEg)
import Verismith.Result
import Verismith.Tool.Internal
import Verismith.Tool.Template
import Verismith.Verilog.AST
import Verismith.Verilog.CodeGen
import Verismith.Verilog.Mutate
import Prelude hiding (FilePath)

data Yosys = Yosys
  { Yosys -> Maybe FilePath
yosysBin :: !(Maybe FilePath),
    Yosys -> Text
yosysDesc :: !Text,
    Yosys -> FilePath
yosysOutput :: !FilePath
  }
  deriving (Yosys -> Yosys -> Bool
(Yosys -> Yosys -> Bool) -> (Yosys -> Yosys -> Bool) -> Eq Yosys
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Yosys -> Yosys -> Bool
== :: Yosys -> Yosys -> Bool
$c/= :: Yosys -> Yosys -> Bool
/= :: Yosys -> Yosys -> Bool
Eq)

instance Tool Yosys where
  toText :: Yosys -> Text
toText (Yosys Maybe FilePath
_ Text
t FilePath
_) = Text
t

instance Show Yosys where
  show :: Yosys -> FilePath
show Yosys
t = Text -> FilePath
unpack (Text -> FilePath) -> Text -> FilePath
forall a b. (a -> b) -> a -> b
$ Yosys -> Text
forall a. Tool a => a -> Text
toText Yosys
t

instance Synthesiser Yosys where
  runSynth :: forall ann. Show ann => Yosys -> SourceInfo ann -> ResultSh ()
runSynth = Yosys -> SourceInfo ann -> ResultSh ()
forall ann. Show ann => Yosys -> SourceInfo ann -> ResultSh ()
runSynthYosys
  synthOutput :: Yosys -> FilePath
synthOutput = Yosys -> FilePath
yosysOutput
  setSynthOutput :: Yosys -> FilePath -> Yosys
setSynthOutput (Yosys Maybe FilePath
a Text
b FilePath
_) = Maybe FilePath -> Text -> FilePath -> Yosys
Yosys Maybe FilePath
a Text
b

instance NFData Yosys where
  rnf :: Yosys -> ()
rnf = Yosys -> ()
forall a. a -> ()
rwhnf

defaultYosys :: Yosys
defaultYosys :: Yosys
defaultYosys = Maybe FilePath -> Text -> FilePath -> Yosys
Yosys Maybe FilePath
forall a. Maybe a
Nothing Text
"yosys" FilePath
"syn_yosys.v"

yosysPath :: Yosys -> FilePath
yosysPath :: Yosys -> FilePath
yosysPath Yosys
sim = FilePath -> ShowS -> Maybe FilePath -> FilePath
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Text -> FilePath
S.fromText Text
"yosys") (FilePath -> ShowS
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> Text -> FilePath
S.fromText Text
"yosys") (Maybe FilePath -> FilePath) -> Maybe FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ Yosys -> Maybe FilePath
yosysBin Yosys
sim

runSynthYosys :: (Show ann) => Yosys -> (SourceInfo ann) -> ResultSh ()
runSynthYosys :: forall ann. Show ann => Yosys -> SourceInfo ann -> ResultSh ()
runSynthYosys Yosys
sim (SourceInfo Text
_ Verilog ann
src) = do
  FilePath
dir <- Sh FilePath -> ResultT Failed Sh FilePath
forall a. Sh a -> ResultT Failed Sh a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh FilePath -> ResultT Failed Sh FilePath)
-> Sh FilePath -> ResultT Failed Sh FilePath
forall a b. (a -> b) -> a -> b
$ do
    FilePath
dir' <- Sh FilePath
S.pwd
    FilePath -> Text -> Sh ()
S.writefile FilePath
inpf (Text -> Sh ()) -> Text -> Sh ()
forall a b. (a -> b) -> a -> b
$ Verilog ann -> Text
forall a. Source a => a -> Text
genSource Verilog ann
src
    FilePath -> Sh FilePath
forall a. a -> Sh a
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
dir'
  Failed -> FilePath -> Text -> FilePath -> [Text] -> ResultSh ()
forall (m :: * -> *).
(MonadSh m, Monad m) =>
Failed
-> FilePath -> Text -> FilePath -> [Text] -> ResultT Failed m ()
execute_
    Failed
SynthFail
    FilePath
dir
    Text
"yosys"
    (Yosys -> FilePath
yosysPath Yosys
sim)
    [ Text
"-p",
      Text
"read_verilog " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
inp Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"; synth; write_verilog -noattr " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
out
    ]
  where
    inpf :: FilePath
inpf = FilePath
"rtl.v"
    inp :: Text
inp = FilePath -> Text
S.toTextIgnore FilePath
inpf
    out :: Text
out = FilePath -> Text
S.toTextIgnore (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ Yosys -> FilePath
forall a. Synthesiser a => a -> FilePath
synthOutput Yosys
sim

runEquivYosys ::
  (Synthesiser a, Synthesiser b, Show ann) =>
  Yosys ->
  a ->
  b ->
  (SourceInfo ann) ->
  ResultSh ()
runEquivYosys :: forall a b ann.
(Synthesiser a, Synthesiser b, Show ann) =>
Yosys -> a -> b -> SourceInfo ann -> ResultSh ()
runEquivYosys Yosys
yosys a
sim1 b
sim2 SourceInfo ann
srcInfo = do
  Sh () -> ResultSh ()
forall a. Sh a -> ResultT Failed Sh a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> ResultSh ()) -> Sh () -> ResultSh ()
forall a b. (a -> b) -> a -> b
$ do
    FilePath -> Text -> Sh ()
S.writefile FilePath
"top.v"
      (Text -> Sh ()) -> (ModDecl ann -> Text) -> ModDecl ann -> Sh ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModDecl ann -> Text
forall a. Source a => a -> Text
genSource
      (ModDecl ann -> Text)
-> (ModDecl ann -> ModDecl ann) -> ModDecl ann -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModDecl ann -> ModDecl ann
forall ann. ModDecl ann -> ModDecl ann
initMod
      (ModDecl ann -> ModDecl ann)
-> (ModDecl ann -> ModDecl ann) -> ModDecl ann -> ModDecl ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Int -> ModDecl ann -> ModDecl ann
forall ann. Bool -> Int -> ModDecl ann -> ModDecl ann
makeTop Bool
False Int
2
      (ModDecl ann -> Sh ()) -> ModDecl ann -> Sh ()
forall a b. (a -> b) -> a -> b
$ SourceInfo ann
srcInfo
        SourceInfo ann
-> Getting (ModDecl ann) (SourceInfo ann) (ModDecl ann)
-> ModDecl ann
forall s a. s -> Getting a s a -> a
^. Getting (ModDecl ann) (SourceInfo ann) (ModDecl ann)
forall a (f :: * -> *).
Functor f =>
(ModDecl a -> f (ModDecl a)) -> SourceInfo a -> f (SourceInfo a)
mainModule
    FilePath -> Text -> Sh ()
S.writefile FilePath
checkFile (Text -> Sh ()) -> Text -> Sh ()
forall a b. (a -> b) -> a -> b
$ a -> b -> SourceInfo ann -> Text
forall a b ann.
(Synthesiser a, Synthesiser b) =>
a -> b -> SourceInfo ann -> Text
yosysSatConfig a
sim1 b
sim2 SourceInfo ann
srcInfo
  a -> SourceInfo ann -> ResultSh ()
forall ann. Show ann => a -> SourceInfo ann -> ResultSh ()
forall a ann.
(Synthesiser a, Show ann) =>
a -> SourceInfo ann -> ResultSh ()
runSynth a
sim1 SourceInfo ann
srcInfo
  b -> SourceInfo ann -> ResultSh ()
forall ann. Show ann => b -> SourceInfo ann -> ResultSh ()
forall a ann.
(Synthesiser a, Show ann) =>
a -> SourceInfo ann -> ResultSh ()
runSynth b
sim2 SourceInfo ann
srcInfo
  Sh () -> ResultSh ()
forall a. Sh a -> ResultT Failed Sh a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> ResultSh ()) -> Sh () -> ResultSh ()
forall a b. (a -> b) -> a -> b
$ FilePath -> [Text] -> Sh ()
S.run_ (Yosys -> FilePath
yosysPath Yosys
yosys) [FilePath -> Text
S.toTextIgnore FilePath
checkFile]
  where
    checkFile :: FilePath
checkFile = Text -> FilePath
S.fromText (Text -> FilePath) -> Text -> FilePath
forall a b. (a -> b) -> a -> b
$ Text
"test." Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. Tool a => a -> Text
toText a
sim1 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"." Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> b -> Text
forall a. Tool a => a -> Text
toText b
sim2 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
".ys"

runEquiv ::
  (Synthesiser a, Synthesiser b, Show ann) =>
  Maybe Text ->
  FilePath ->
  a ->
  b ->
  (SourceInfo ann) ->
  ResultSh ()
runEquiv :: forall a b ann.
(Synthesiser a, Synthesiser b, Show ann) =>
Maybe Text -> FilePath -> a -> b -> SourceInfo ann -> ResultSh ()
runEquiv Maybe Text
mt FilePath
datadir a
sim1 b
sim2 SourceInfo ann
srcInfo = do
  FilePath
dir <- Sh FilePath -> ResultT Failed Sh FilePath
forall a. Sh a -> ResultT Failed Sh a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh Sh FilePath
S.pwd
  Sh () -> ResultSh ()
forall a. Sh a -> ResultT Failed Sh a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> ResultSh ()) -> Sh () -> ResultSh ()
forall a b. (a -> b) -> a -> b
$ do
    FilePath -> Text -> Sh ()
S.writefile FilePath
"top.v"
      (Text -> Sh ()) -> (ModDecl ann -> Text) -> ModDecl ann -> Sh ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModDecl ann -> Text
forall a. Source a => a -> Text
genSource
      (ModDecl ann -> Text)
-> (ModDecl ann -> ModDecl ann) -> ModDecl ann -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModDecl ann -> ModDecl ann
forall ann. ModDecl ann -> ModDecl ann
initMod
      (ModDecl ann -> ModDecl ann)
-> (ModDecl ann -> ModDecl ann) -> ModDecl ann -> ModDecl ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModDecl ann -> ModDecl ann
forall ann. ModDecl ann -> ModDecl ann
makeTopAssert
      (ModDecl ann -> Sh ()) -> ModDecl ann -> Sh ()
forall a b. (a -> b) -> a -> b
$ SourceInfo ann
srcInfo
        SourceInfo ann
-> Getting (ModDecl ann) (SourceInfo ann) (ModDecl ann)
-> ModDecl ann
forall s a. s -> Getting a s a -> a
^. Getting (ModDecl ann) (SourceInfo ann) (ModDecl ann)
forall a (f :: * -> *).
Functor f =>
(ModDecl a -> f (ModDecl a)) -> SourceInfo a -> f (SourceInfo a)
mainModule
    FilePath -> Text -> SourceInfo ann -> Sh ()
forall ann. FilePath -> Text -> SourceInfo ann -> Sh ()
replaceMods (a -> FilePath
forall a. Synthesiser a => a -> FilePath
synthOutput a
sim1) Text
"_1" SourceInfo ann
srcInfo
    FilePath -> Text -> SourceInfo ann -> Sh ()
forall ann. FilePath -> Text -> SourceInfo ann -> Sh ()
replaceMods (b -> FilePath
forall a. Synthesiser a => a -> FilePath
synthOutput b
sim2) Text
"_2" SourceInfo ann
srcInfo
    FilePath -> Text -> Sh ()
S.writefile FilePath
"proof.sby" (Text -> Sh ()) -> Text -> Sh ()
forall a b. (a -> b) -> a -> b
$ Maybe Text -> FilePath -> a -> b -> SourceInfo ann -> Text
forall a b ann.
(Synthesiser a, Synthesiser b) =>
Maybe Text -> FilePath -> a -> b -> SourceInfo ann -> Text
sbyConfig Maybe Text
mt FilePath
datadir a
sim1 b
sim2 SourceInfo ann
srcInfo
  Int
e <- Sh Int -> ResultT Failed Sh Int
forall a. Sh a -> ResultT Failed Sh a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh Int -> ResultT Failed Sh Int)
-> Sh Int -> ResultT Failed Sh Int
forall a b. (a -> b) -> a -> b
$ do
    FilePath -> Text -> FilePath -> [Text] -> Sh ()
exe FilePath
dir Text
"symbiyosys" FilePath
"sby" [Text
"-f", Text
"proof.sby"]
    Sh Int
S.lastExitCode
  case Int
e of
    Int
0 -> Sh (Result Failed ()) -> ResultSh ()
forall a (m :: * -> *) b. m (Result a b) -> ResultT a m b
ResultT (Sh (Result Failed ()) -> ResultSh ())
-> (Result Failed () -> Sh (Result Failed ()))
-> Result Failed ()
-> ResultSh ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result Failed () -> Sh (Result Failed ())
forall a. a -> Sh a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result Failed () -> ResultSh ())
-> Result Failed () -> ResultSh ()
forall a b. (a -> b) -> a -> b
$ () -> Result Failed ()
forall a b. b -> Result a b
Pass ()
    Int
2 -> case Maybe Text
mt of
      Maybe Text
Nothing -> Sh (Result Failed ()) -> ResultSh ()
forall a (m :: * -> *) b. m (Result a b) -> ResultT a m b
ResultT (Sh (Result Failed ()) -> ResultSh ())
-> (Failed -> Sh (Result Failed ())) -> Failed -> ResultSh ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result Failed () -> Sh (Result Failed ())
forall a. a -> Sh a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result Failed () -> Sh (Result Failed ()))
-> (Failed -> Result Failed ()) -> Failed -> Sh (Result Failed ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Failed -> Result Failed ()
forall a b. a -> Result a b
Fail (Failed -> ResultSh ()) -> Failed -> ResultSh ()
forall a b. (a -> b) -> a -> b
$ Maybe CounterEg -> Failed
EquivFail Maybe CounterEg
forall a. Maybe a
Nothing
      Just Text
_ ->
        Sh (Result Failed ()) -> ResultSh ()
forall a (m :: * -> *) b. m (Result a b) -> ResultT a m b
ResultT (Sh (Result Failed ()) -> ResultSh ())
-> Sh (Result Failed ()) -> ResultSh ()
forall a b. (a -> b) -> a -> b
$
          Failed -> Result Failed ()
forall a b. a -> Result a b
Fail
            (Failed -> Result Failed ())
-> (Text -> Failed) -> Text -> Result Failed ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe CounterEg -> Failed
EquivFail
            (Maybe CounterEg -> Failed)
-> (Text -> Maybe CounterEg) -> Text -> Failed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CounterEg -> Maybe CounterEg
forall a. a -> Maybe a
Just
            (CounterEg -> Maybe CounterEg)
-> (Text -> CounterEg) -> Text -> Maybe CounterEg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CounterEg -> Either FilePath CounterEg -> CounterEg
forall b a. b -> Either a b -> b
fromRight CounterEg
forall a. Monoid a => a
mempty
            (Either FilePath CounterEg -> CounterEg)
-> (Text -> Either FilePath CounterEg) -> Text -> CounterEg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either FilePath CounterEg
parseCounterEg
            (Text -> Result Failed ()) -> Sh Text -> Sh (Result Failed ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> Sh Text
forall (m :: * -> *). MonadSh m => FilePath -> m Text
readfile FilePath
"proof/engine_0/trace.smtc"
    Int
124 -> Sh (Result Failed ()) -> ResultSh ()
forall a (m :: * -> *) b. m (Result a b) -> ResultT a m b
ResultT (Sh (Result Failed ()) -> ResultSh ())
-> (Result Failed () -> Sh (Result Failed ()))
-> Result Failed ()
-> ResultSh ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result Failed () -> Sh (Result Failed ())
forall a. a -> Sh a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result Failed () -> ResultSh ())
-> Result Failed () -> ResultSh ()
forall a b. (a -> b) -> a -> b
$ Failed -> Result Failed ()
forall a b. a -> Result a b
Fail Failed
TimeoutError
    Int
_ -> Sh (Result Failed ()) -> ResultSh ()
forall a (m :: * -> *) b. m (Result a b) -> ResultT a m b
ResultT (Sh (Result Failed ()) -> ResultSh ())
-> (Result Failed () -> Sh (Result Failed ()))
-> Result Failed ()
-> ResultSh ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result Failed () -> Sh (Result Failed ())
forall a. a -> Sh a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result Failed () -> ResultSh ())
-> Result Failed () -> ResultSh ()
forall a b. (a -> b) -> a -> b
$ Failed -> Result Failed ()
forall a b. a -> Result a b
Fail Failed
EquivError
  where
    exe :: FilePath -> Text -> FilePath -> [Text] -> Sh ()
exe FilePath
dir Text
name FilePath
e = Sh Text -> Sh ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Sh Text -> Sh ()) -> ([Text] -> Sh Text) -> [Text] -> Sh ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Sh Text -> Sh Text
forall a. Bool -> Sh a -> Sh a
S.errExit Bool
False (Sh Text -> Sh Text) -> ([Text] -> Sh Text) -> [Text] -> Sh Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text -> Sh Text -> Sh Text
forall a. FilePath -> Text -> Sh a -> Sh a
logCommand FilePath
dir Text
name (Sh Text -> Sh Text) -> ([Text] -> Sh Text) -> [Text] -> Sh Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [Text] -> Sh Text
timeout FilePath
e