-
Notifications
You must be signed in to change notification settings - Fork 24
/
Copy pathdualflexpress.sby
93 lines (89 loc) · 2.75 KB
/
dualflexpress.sby
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
[tasks]
xilinx prf optpipe optcfg optstartup
xilinxswap prf optpipe optcfg optstartup optswap
xilinxc cvr optpipe optcfg
xilinxs cvr optpipe optcfg optstartup
bare prf
barep prf optpipe
barecfg prf optpipe optcfg
cfgonly prf optcfg
bareswap prf optswap
barepswap prf optpipe optswap
barecfgswp prf optpipe optcfg optswap
cfgonlyswp prf optcfg optswap
ice40 prf optpipe optcfg optstartup
ice40c cvr optpipe optcfg
ice40s cvr optpipe optcfg optstartup
ice40div prf optpipe optcfg divone optstartup
ice40divc cvr optpipe optcfg divone
# ice40divs cvr optpipe optcfg divone optstartup
xilinxdiv xilinx prf optpipe optcfg divone
xilinxdivc xilinx cvr optpipe optcfg divone
# xilinxdivs xilinx cvr optpipe optcfg divone optstartup
divthree prf optpipe optcfg
divfive prf optpipe optcfg
# divfives cvr optpipe optcfg optstartup
arrow prf arrow optpipe optcfg optstartup
arrowc cvr arrow optpipe optcfg
arrows cvr arrow optpipe optcfg optstartup
x32 prf xilinx optpipe optcfg optstartup optaddr32
x32c cvr xilinx optpipe optcfg optaddr32
x32swap prf xilinx optpipe optcfg optstartup optaddr32 optswap
#
# Special proofs, defined for bench mark testing only
xilinxdivbmc bmc xilinxdiv xilinx optpipe optcfg divone
divfivebmc bmc optpipe optcfg divfive
divthreebmc bmc optpipe optcfg divthree
[options]
prf: mode prove
prf: depth 40
bmc: mode bmc
bmc: depth 40
cvr: mode cover
cvr: depth 145
divone: depth 120
divthree: depth 150
divfive: depth 222
xilinxdiv: depth 80
ice40div: depth 80
ice40s: depth 120
xilinxs: depth 120
arrows: depth 250
optaddr32: depth 43
x32c: depth 150
# ice40divs: depth 250
# xilinxdivs: depth 250
# divfives: depth 610
[engines]
smtbmc boolector
smtbmc yices
[script]
read -formal -DDUALFLEXPRESS fwb_slave.v
read -formal -DDUALFLEXPRESS dualflexpress.v
--pycode-begin--
cmd = "hierarchy -top dualflexpress"
cmd += " -chparam OPT_PIPE %d" % (1 if "optpipe" in tags else 0)
cmd += " -chparam OPT_CFG %d" % (1 if "optcfg" in tags else 0)
cmd += " -chparam OPT_ENDIANSWAP %d" % (1 if "optswap" in tags else 0)
if ("xilinx" in tags):
cmd += " -chparam RDDELAY 3 -chparam NDUMMY 6"
elif ("arrow" in tags):
cmd += " -chparam RDDELAY 2 -chparam NDUMMY 4"
else:
cmd += " -chparam RDDELAY 0 -chparam NDUMMY 8"
if ("divone" in tags):
cmd += " -chparam OPT_CLKDIV 1"
elif ("divthree" in tags):
cmd += " -chparam OPT_CLKDIV 3"
elif ("divfive" in tags):
cmd += " -chparam OPT_CLKDIV 5"
elif ("divfives" in tags):
cmd += " -chparam OPT_CLKDIV 5"
cmd += " -chparam OPT_STARTUP %d" % (1 if "optstartup" in tags else 0)
cmd += " -chparam LGFLASHSZ %d" % (32 if "optaddr32" in tags else 24)
output(cmd)
--pycode-end--
prep -top dualflexpress
[files]
fwb_slave.v
../../rtl/dualflexpress.v