-
Notifications
You must be signed in to change notification settings - Fork 0
/
fetch.sby
36 lines (31 loc) · 819 Bytes
/
fetch.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
[tasks]
cover
prove
[options]
cover: mode cover
cover: depth 10
cover: append 3
prove: mode prove
prove: depth 10
[engines]
smtbmc
[script]
ghdl --std=08 fetch.vhd fetch.psl \
one_stage_buffer.vhd one_stage_buffer.psl \
two_stage_buffer.vhd two_stage_buffer.psl \
two_stage_fifo.vhd two_stage_fifo.psl \
pipe_concat.vhd pipe_concat.psl \
-e fetch
prep -top fetch
chformal -assume2assert fetch/* %M
[files]
fetch.vhd
fetch.psl
../pipe_concat/pipe_concat.vhd
../pipe_concat/pipe_concat.psl
../one_stage_buffer/one_stage_buffer.vhd
../one_stage_buffer/one_stage_buffer.psl
../two_stage_buffer/two_stage_buffer.vhd
../two_stage_buffer/two_stage_buffer.psl
../two_stage_fifo/two_stage_fifo.vhd
../two_stage_fifo/two_stage_fifo.psl