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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
|
{-|
Module : Verismith.Tool.Template
Description : Template file for different configuration files
Copyright : (c) 2019, Yann Herklotz
License : GPL-3
Maintainer : yann [at] yannherklotz [dot] com
Stability : experimental
Portability : POSIX
Template file for different configuration files.
-}
{-# LANGUAGE QuasiQuotes #-}
module Verismith.Tool.Template
( yosysSynthConfigStd
, yosysSatConfig
, yosysSimConfig
, quartusLightSynthConfig
, quartusSynthConfig
, xstSynthConfig
, vivadoSynthConfig
, sbyConfig
, icarusTestbench
)
where
import Control.Lens ((^..))
import Data.Maybe (fromMaybe)
import Data.Text (Text)
import qualified Data.Text as T
import Prelude hiding (FilePath)
import Shelly
import Verismith.Tool.Internal
import Verismith.Verilog.AST
import Verismith.Verilog.CodeGen
rename :: Text -> [Text] -> Text
rename end entries =
T.intercalate "\n"
$ flip mappend end
. mappend "rename "
. doubleName
<$> entries
{-# INLINE rename #-}
doubleName :: Text -> Text
doubleName n = n <> " " <> n
{-# INLINE doubleName #-}
outputText :: Synthesiser a => a -> Text
outputText = toTextIgnore . synthOutput
yosysSynthConfig :: Synthesiser a => Text -> a -> FilePath -> Text
yosysSynthConfig t a fp = T.unlines
[ "read_verilog " <> toTextIgnore fp
, t
, "write_verilog " <> outputText a
]
yosysSynthConfigStd :: Synthesiser a => a -> FilePath -> Text
yosysSynthConfigStd = yosysSynthConfig "synth"
yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> b -> (SourceInfo ann) -> Text
yosysSatConfig sim1 sim2 (SourceInfo top src) = T.unlines
[ "read_verilog " <> outputText sim1
, rename "_1" mis
, "read_verilog syn_" <> outputText sim2 <> ".v"
, rename "_2" mis
, "read_verilog " <> top <> ".v"
, "proc; opt_clean"
, "flatten " <> top
, "sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 " <> top
]
where
mis = src ^.. getSourceId
yosysSimConfig :: Text
yosysSimConfig = "read_verilog rtl.v; proc;;\nrename mod mod_rtl"
quartusLightSynthConfig :: Synthesiser a => a -> FilePath -> Text -> FilePath -> Text
quartusLightSynthConfig q sdc top fp = T.unlines
[ "load_package flow"
, ""
, "project_new -overwrite " <> top
, ""
, "set_global_assignment -name FAMILY \"Cyclone V\""
, "set_global_assignment -name SYSTEMVERILOG_FILE " <> toTextIgnore fp
, "set_global_assignment -name TOP_LEVEL_ENTITY " <> top
, "set_global_assignment -name SDC_FILE " <> toTextIgnore sdc
, "set_global_assignment -name INI_VARS \"qatm_force_vqm=on;\""
, "set_global_assignment -name NUM_PARALLEL_PROCESSORS 2"
, "set_instance_assignment -name VIRTUAL_PIN ON -to *"
, ""
, "execute_module -tool map"
, "execute_module -tool fit"
, "execute_module -tool sta -args \"--mode=implement\""
, "execute_module -tool eda -args \"--simulation --tool=vcs\""
, ""
, "project_close"
]
quartusSynthConfig :: Synthesiser a => a -> FilePath -> Text -> FilePath -> Text
quartusSynthConfig q sdc top fp = T.unlines
[ "load_package flow"
, ""
, "project_new -overwrite " <> top
, ""
, "set_global_assignment -name FAMILY \"Cyclone 10 GX\""
, "set_global_assignment -name SYSTEMVERILOG_FILE " <> toTextIgnore fp
, "set_global_assignment -name TOP_LEVEL_ENTITY " <> top
, "set_global_assignment -name SDC_FILE " <> toTextIgnore sdc
, "set_global_assignment -name INI_VARS \"qatm_force_vqm=on;\""
, "set_global_assignment -name NUM_PARALLEL_PROCESSORS 2"
, "set_instance_assignment -name VIRTUAL_PIN ON -to *"
, ""
, "execute_module -tool syn"
, "execute_module -tool eda -args \"--simulation --tool=vcs\""
, ""
, "project_close"
]
xstSynthConfig :: Text -> Text
xstSynthConfig top = T.unlines
[ "run"
, "-ifn " <> top <> ".prj -ofn " <> top <> " -p artix7 -top " <> top
, "-iobuf NO -ram_extract NO -rom_extract NO -use_dsp48 NO"
, "-fsm_extract YES -fsm_encoding Auto"
, "-change_error_to_warning \"HDLCompiler:226 HDLCompiler:1832\""
]
vivadoSynthConfig :: Text -> Text -> Text
vivadoSynthConfig top outf = T.unlines
[ "# CRITICAL WARNING: [Synth 8-5821] Potential divide by zero"
, "set_msg_config -id {Synth 8-5821} -new_severity {WARNING}"
, ""
, "read_verilog rtl.v"
, "synth_design -part xc7k70t -top " <> top
, "write_verilog -force " <> outf
]
sbyConfig :: (Synthesiser a, Synthesiser b) => Maybe Text -> FilePath -> a -> b -> (SourceInfo ann) -> Text
sbyConfig mt datadir sim1 sim2 (SourceInfo top _) = T.unlines
[ "[options]"
, "multiclock on"
, "mode prove"
, "aigsmt " <> fromMaybe "none" mt
, ""
, "[engines]"
, "abc pdr"
, ""
, "[script]"
, readL
, "read -formal " <> outputText sim1
, "read -formal " <> outputText sim2
, "read -formal top.v"
, "prep -top " <> top
, ""
, "[files]"
, depList
, outputText sim2
, outputText sim1
, "top.v"
]
where
deps = ["cells_cmos.v", "cells_cyclone_v.v", "cells_verific.v", "cells_xilinx_7.v", "cells_yosys.v"]
depList =
T.intercalate "\n"
$ toTextIgnore
. (datadir </> fromText "data" </>)
. fromText
<$> deps
readL = T.intercalate "\n" $ mappend "read -formal " <$> deps
icarusTestbench :: (Synthesiser a, Show ann) => FilePath -> (Verilog ann) -> a -> Text
icarusTestbench datadir t synth1 = T.unlines
[ "`include \"" <> ddir <> "/data/cells_cmos.v\""
, "`include \"" <> ddir <> "/data/cells_cyclone_v.v\""
, "`include \"" <> ddir <> "/data/cells_verific.v\""
, "`include \"" <> ddir <> "/data/cells_xilinx_7.v\""
, "`include \"" <> ddir <> "/data/cells_yosys.v\""
, "`include \"" <> toTextIgnore (synthOutput synth1) <> "\""
, ""
, genSource t
]
where
ddir = toTextIgnore datadir
|
