|
|
@ -17,7 +17,13 @@ prove: abc pdr |
|
|
[script] |
|
|
[script] |
|
|
ghdl --std=08 -gFormal=true -gDepth=16 -gWidth=16 fifo.vhd vai_fifo.vhd -e vai_fifo |
|
|
ghdl --std=08 -gFormal=true -gDepth=16 -gWidth=16 fifo.vhd vai_fifo.vhd -e vai_fifo |
|
|
prep -top vai_fifo |
|
|
prep -top vai_fifo |
|
|
|
|
|
# Convert all assumes to asserts in sub-unit i_fifo |
|
|
chformal -assume2assert vai_fifo/i_fifo %M |
|
|
chformal -assume2assert vai_fifo/i_fifo %M |
|
|
|
|
|
# Remove selected covers in i_fifo sub-unit as they cannot be reached |
|
|
|
|
|
chformal -cover -remove */formalg.read_pnt_stable_when_empty.cover |
|
|
|
|
|
chformal -cover -remove */formalg.rerror.cover |
|
|
|
|
|
chformal -cover -remove */formalg.werror.cover |
|
|
|
|
|
chformal -cover -remove */formalg.write_pnt_stable_when_full.cover |
|
|
|
|
|
|
|
|
[files] |
|
|
[files] |
|
|
../fifo/fifo.vhd |
|
|
../fifo/fifo.vhd |
|
|
|
