-
Notifications
You must be signed in to change notification settings - Fork 24
/
Copy pathqflexpress.sby
87 lines (82 loc) · 2.56 KB
/
qflexpress.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
[tasks]
bare prf
barep prf optpipe
barecfg prf optpipe optcfg
bareswap prf optswap
barepswap prf optpipe optswap
barecfgswp prf optpipe optcfg optswap
cfgonly prf optcfg
cfgonlyswp prf optcfg optswap
divthree prf optpipe optcfg
divthrswp prf optpipe optcfg optswap
divfive prf optpipe optcfg
divfives cvr optpipe optcfg optstartup
ice40 prf optpipe optcfg optstartup
ice40c cvr optpipe optcfg
ice40s cvr optpipe optcfg optstartup
ice40div prf optpipe optcfg optstartup divone
ice40divc cvr optpipe optcfg divone
ice40divs cvr optpipe optcfg optstartup divone
xilinx prf xilinx optpipe optcfg optstartup
xilinxswap prf xilinx optpipe optcfg optstartup optswap
xilinxc cvr xilinx optpipe optcfg
xilinxs cvr xilinx optpipe optcfg optstartup
xilinxdiv prf xilinx optpipe optcfg divone
xilinxdvsw prf xilinx optpipe optcfg divone optswap
xilinxdivc cvr xilinx optpipe optcfg divone
xilinxdivs cvr xilinx optpipe optcfg optstartup divone
x32 prf xilinx optpipe optcfg optstartup optaddr32
x32c cvr xilinx optpipe optcfg optaddr32
x32swap prf xilinx optpipe optcfg optaddr32 optswap
#
# Special proofs, defined for bench mark testing only
divfivebmc bmc optpipe optcfg divfive
[options]
prf: mode prove
prf: depth 34
bmc: mode bmc
bmc: depth 34
cvr: mode cover
cvr: depth 40
divone: depth 60
divthree: depth 102
divfive: depth 155
ice40s: depth 150
xilinxs: depth 160
ice40divc: depth 72
ice40divs: depth 250
xilinxdivc: depth 80
xilinxdivs: depth 250
divfives: depth 610
x32: depth 26
x32c: depth 44
divfivebmc: depth 155
[engines]
smtbmc boolector
smtbmc yices
[script]
read -formal -DQFLEXPRESS fwb_slave.v
read -formal -DQFLEXPRESS qflexpress.v
--pycode-begin--
cmd = "hierarchy -top qflexpress"
cmd += " -chparam RDDELAY %d" % (3 if "xilinx" in tags else 0)
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 ("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 qflexpress
dump
[files]
fwb_slave.v
../../rtl/qflexpress.v