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
|
{-|
Module : VeriFuzz.Sim.Yosys
Description : Yosys simulator implementation.
Copyright : (c) 2018-2019, Yann Herklotz
License : BSD-3
Maintainer : yann [at] yannherklotz [dot] com
Stability : experimental
Portability : POSIX
Yosys simulator implementation.
-}
{-# LANGUAGE QuasiQuotes #-}
module VeriFuzz.Sim.Yosys
( Yosys(..)
, defaultYosys
, runEquiv
, runEquivYosys
)
where
import Control.DeepSeq (NFData, rnf, rwhnf)
import Control.Lens
import Control.Monad (void)
import Data.Text (Text, unpack)
import Prelude hiding (FilePath)
import Shelly
import Shelly.Lifted (liftSh)
import Text.Shakespeare.Text (st)
import VeriFuzz.Result
import VeriFuzz.Sim.Internal
import VeriFuzz.Sim.Template
import VeriFuzz.Verilog.AST
import VeriFuzz.Verilog.CodeGen
import VeriFuzz.Verilog.Mutate
data Yosys = Yosys { yosysBin :: !(Maybe FilePath)
, yosysDesc :: {-# UNPACK #-} !Text
, yosysOutput :: {-# UNPACK #-} !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 (fromText "yosys") (</> fromText "yosys") $ yosysBin sim
runSynthYosys :: Yosys -> SourceInfo -> ResultSh ()
runSynthYosys sim (SourceInfo _ src) = do
dir <- liftSh $ do
dir' <- pwd
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 = toTextIgnore inpf
out = toTextIgnore $ synthOutput sim
runEquivYosys
:: (Synthesiser a, Synthesiser b)
=> Yosys
-> a
-> b
-> SourceInfo
-> ResultSh ()
runEquivYosys yosys sim1 sim2 srcInfo = do
liftSh $ do
writefile "top.v"
. genSource
. initMod
. makeTop 2
$ srcInfo
^. mainModule
writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo
runSynth sim1 srcInfo
runSynth sim2 srcInfo
liftSh $ run_ (yosysPath yosys) [toTextIgnore checkFile]
where checkFile = fromText [st|test.#{toText sim1}.#{toText sim2}.ys|]
runEquiv
:: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> ResultSh ()
runEquiv sim1 sim2 srcInfo = do
dir <- liftSh pwd
liftSh $ do
writefile "top.v"
. genSource
. initMod
. makeTopAssert
$ srcInfo
^. mainModule
replaceMods (synthOutput sim1) "_1" srcInfo
replaceMods (synthOutput sim2) "_2" srcInfo
writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo
e <- liftSh $ do
exe dir "symbiyosys" "sby" ["-f", "proof.sby"]
lastExitCode
case e of
0 -> ResultT . return $ Pass ()
2 -> ResultT . return $ Fail EquivFail
124 -> ResultT . return $ Fail TimeoutError
_ -> ResultT . return $ Fail EquivError
where
exe dir name e = void . errExit False . logCommand dir name . timeout e
|
