1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
{-# LANGUAGE QuasiQuotes #-}
-- |
-- Module : Verismith.Tool.Yosys
-- Description : Yosys simulator implementation.
-- Copyright : (c) 2018-2019, 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
{ yosysBin :: !(Maybe FilePath),
yosysDesc :: !Text,
yosysOutput :: !FilePath
}
deriving (Eq)
instance Tool Yosys where
toText (Yosys _ t _) = t
instance Show Yosys where
show t = unpack $ toText t
instance Synthesiser Yosys where
runSynth = runSynthYosys
synthOutput = yosysOutput
setSynthOutput (Yosys a b _) = Yosys a b
instance NFData Yosys where
rnf = rwhnf
defaultYosys :: Yosys
defaultYosys = Yosys Nothing "yosys" "syn_yosys.v"
yosysPath :: Yosys -> FilePath
yosysPath sim = maybe (S.fromText "yosys") (</> S.fromText "yosys") $ yosysBin sim
runSynthYosys :: Show ann => Yosys -> (SourceInfo ann) -> ResultSh ()
runSynthYosys sim (SourceInfo _ src) = do
dir <- liftSh $ do
dir' <- S.pwd
S.writefile inpf $ genSource src
return dir'
execute_
SynthFail
dir
"yosys"
(yosysPath sim)
[ "-p",
"read_verilog " <> inp <> "; synth; write_verilog -noattr " <> out
]
where
inpf = "rtl.v"
inp = S.toTextIgnore inpf
out = S.toTextIgnore $ synthOutput sim
runEquivYosys ::
(Synthesiser a, Synthesiser b, Show ann) =>
Yosys ->
a ->
b ->
(SourceInfo ann) ->
ResultSh ()
runEquivYosys yosys sim1 sim2 srcInfo = do
liftSh $ do
S.writefile "top.v"
. genSource
. initMod
. makeTop 2
$ srcInfo
^. mainModule
S.writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo
runSynth sim1 srcInfo
runSynth sim2 srcInfo
liftSh $ S.run_ (yosysPath yosys) [S.toTextIgnore checkFile]
where
checkFile = S.fromText $ "test." <> toText sim1 <> "." <> toText sim2 <> ".ys"
runEquiv ::
(Synthesiser a, Synthesiser b, Show ann) =>
Maybe Text ->
FilePath ->
a ->
b ->
(SourceInfo ann) ->
ResultSh ()
runEquiv mt datadir sim1 sim2 srcInfo = do
dir <- liftSh S.pwd
liftSh $ do
S.writefile "top.v"
. genSource
. initMod
. makeTopAssert
$ srcInfo
^. mainModule
replaceMods (synthOutput sim1) "_1" srcInfo
replaceMods (synthOutput sim2) "_2" srcInfo
S.writefile "proof.sby" $ sbyConfig mt datadir sim1 sim2 srcInfo
e <- liftSh $ do
exe dir "symbiyosys" "sby" ["-f", "proof.sby"]
S.lastExitCode
case e of
0 -> ResultT . return $ Pass ()
2 -> case mt of
Nothing -> ResultT . return . Fail $ EquivFail Nothing
Just _ ->
ResultT $
Fail . EquivFail . Just . fromRight mempty
. parseCounterEg
<$> readfile "proof/engine_0/trace.smtc"
124 -> ResultT . return $ Fail TimeoutError
_ -> ResultT . return $ Fail EquivError
where
exe dir name e = void . S.errExit False . logCommand dir name . timeout e
|
