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
|
{-|
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
( yosysSatConfig
, yosysSimConfig
, xstSynthConfig
, vivadoSynthConfig
, sbyConfig
, icarusTestbench
)
where
import Control.Lens ((^..))
import Data.Text (Text)
import qualified Data.Text as T
import Prelude hiding (FilePath)
import Shelly
import Text.Shakespeare.Text (st)
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
-- brittany-disable-next-binding
yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> Text
yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|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
-- brittany-disable-next-binding
yosysSimConfig :: Text
yosysSimConfig = [st|read_verilog rtl.v; proc;;
rename mod mod_rtl
|]
-- brittany-disable-next-binding
xstSynthConfig :: Text -> Text
xstSynthConfig top = [st|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"
|]
-- brittany-disable-next-binding
vivadoSynthConfig :: Text -> Text -> Text
vivadoSynthConfig top outf = [st|
# 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}
|]
-- brittany-disable-next-binding
sbyConfig :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo -> Text
sbyConfig datadir sim1 sim2 (SourceInfo top _) = [st|[options]
multiclock on
mode prove
[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) => FilePath -> Verilog -> a -> Text
icarusTestbench datadir t synth1 = [st|
`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
|
