-
Notifications
You must be signed in to change notification settings - Fork 3
/
gen-btor.ys
85 lines (77 loc) · 2.89 KB
/
gen-btor.ys
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
read_verilog -formal ./ridecore-src-buggy/define.v \
./ridecore-src-buggy/topsim.v \
./ridecore-src-buggy/alloc_issue_ino.v \
./ridecore-src-buggy/search_be.v \
./ridecore-src-buggy/srcsel.v \
./ridecore-src-buggy/alu_ops.vh \
./ridecore-src-buggy/arf.v \
./ridecore-src-buggy/ram_sync.v \
./ridecore-src-buggy/ram_sync_nolatch.v \
./ridecore-src-buggy/brimm_gen.v \
./ridecore-src-buggy/constants.vh \
./ridecore-src-buggy/decoder.v \
./ridecore-src-buggy/dmem.v \
./ridecore-src-buggy/exunit_alu.v \
./ridecore-src-buggy/exunit_branch.v \
./ridecore-src-buggy/exunit_ldst.v \
./ridecore-src-buggy/exunit_mul.v \
./ridecore-src-buggy/imem.v \
./ridecore-src-buggy/imm_gen.v \
./ridecore-src-buggy/pipeline_if.v \
./ridecore-src-buggy/gshare.v \
./ridecore-src-buggy/pipeline.v \
./ridecore-src-buggy/oldest_finder.v \
./ridecore-src-buggy/btb.v \
./ridecore-src-buggy/prioenc.v \
./ridecore-src-buggy/mpft.v \
./ridecore-src-buggy/reorderbuf.v \
./ridecore-src-buggy/rrf_freelistmanager.v \
./ridecore-src-buggy/rrf.v \
./ridecore-src-buggy/rs_alu.v \
./ridecore-src-buggy/rs_branch.v \
./ridecore-src-buggy/rs_ldst.v \
./ridecore-src-buggy/rs_mul.v \
./ridecore-src-buggy/rs_reqgen.v \
./ridecore-src-buggy/rv32_opcodes.vh \
./ridecore-src-buggy/src_manager.v \
./ridecore-src-buggy/srcopr_manager.v \
./ridecore-src-buggy/storebuf.v \
./ridecore-src-buggy/tag_generator.v \
./ridecore-src-buggy/dualport_ram.v \
./ridecore-src-buggy/alu.v \
./ridecore-src-buggy/multiplier.v \
./sqed-generator/SQED-Generator/QEDFiles/inst_constraints.v \
./sqed-generator/SQED-Generator/QEDFiles/modify_instruction.v \
./sqed-generator/SQED-Generator/QEDFiles/qed_decoder.v \
./sqed-generator/SQED-Generator/QEDFiles/qed_i_cache.v \
./sqed-generator/SQED-Generator/QEDFiles/qed_instruction_mux.v \
./sqed-generator/SQED-Generator/QEDFiles/qed.v;
# prep does a conservative elaboration
# of the top module provided
prep -top top;
# this command just does a sanity check
# of the hierarchy
hierarchy -check;
# If an assumption is flopped, you might
# see strange behavior at the last state
# (because the clock hasn't toggled)
# this command ensures that assumptions
# hold at every state
chformal -assume -early;
# this processes memories
# nomap means it will keep them as arrays
memory;
# flatten the design hierarchy
flatten;
# (optional) uncomment and set values to simulate reset signal
# use -resetn for an active low pin
# -n configures the number of cycles to simulate
# -rstlen configures how long the reset is active (recommended to keep it active for the whole simulation)
# -w tells it to write back the final state of the simulation as the initial state in the btor2 file
# another useful option is -zinit which zero initializes any uninitialized state
sim -clock clk -resetn reset_x -n 5 -rstlen 5 -zinit -w top
# This turns all undriven signals into
# inputs
setundef -undriven -expose;
# This writes to a file in BTOR2 format
write_btor ridecore.btor2