blob: 536c64a1596b27aa7bb882474b2fdd65f78d009c (
plain)
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
|
# Verify xilinx cell models
read_verilog xl_cells.v
read_verilog xl_cells_tb.v
rename GND MY_GND
rename INV MY_INV
rename LUT1 MY_LUT1
rename LUT2 MY_LUT2
rename LUT3 MY_LUT3
rename LUT4 MY_LUT4
rename LUT5 MY_LUT5
rename LUT6 MY_LUT6
rename MUXCY MY_MUXCY
rename MUXF7 MY_MUXF7
rename VCC MY_VCC
rename XORCY MY_XORCY
read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/GND.v
read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/INV.v
read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/LUT1.v
read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/LUT2.v
read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/LUT3.v
read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/LUT4.v
read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/LUT5.v
read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/LUT6.v
read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/MUXCY.v
read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/MUXF7.v
read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/VCC.v
read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/XORCY.v
rename GND XL_GND
rename INV XL_INV
rename LUT1 XL_LUT1
rename LUT2 XL_LUT2
rename LUT3 XL_LUT3
rename LUT4 XL_LUT4
rename LUT5 XL_LUT5
rename LUT6 XL_LUT6
rename MUXCY XL_MUXCY
rename MUXF7 XL_MUXF7
rename VCC XL_VCC
rename XORCY XL_XORCY
hierarchy
proc
flatten TB_*
opt_clean
sat -verify -prove ok 1'b1 TB_GND
sat -verify -prove ok 1'b1 TB_INV
sat -verify -prove ok 1'b1 TB_LUT1
sat -verify -prove ok 1'b1 TB_LUT2
sat -verify -prove ok 1'b1 TB_LUT3
sat -verify -prove ok 1'b1 TB_LUT4
sat -verify -prove ok 1'b1 TB_LUT5
sat -verify -prove ok 1'b1 TB_LUT6
sat -verify -prove ok 1'b1 TB_MUXCY
sat -verify -prove ok 1'b1 TB_MUXF7
sat -verify -prove ok 1'b1 TB_VCC
sat -verify -prove ok 1'b1 TB_XORCY
|
