Subversion Repositories zipcpu

[tasks]

dcache          full_proof      dcache

piped           full_proof      no_dcache

nopipe          nopipe          no_dcache

lowlogic        nopipe          no_dcache

ice40           nopipe          no_dcache       nobkram

[options]

mode prove

depth 18

dcache:   depth 16 # Was 10

piped:    depth 16 # Was 14 for yosys only, trying 18 w/ Verific

nopipe:   depth 16 # Was 11

lowlogic: depth 16 # Was 10

ice40:    depth 16 # Was 11

[engines]

smtbmc boolector

[script]

nobkram: read -define -DNO_DISTRIBUTED_RAM

read -define -DZIPCPU

#

read -formal -D ZIPCPU cpuops.v

read -formal -D ZIPCPU memops.v

read -formal -D ZIPCPU pipemem.v

read -formal -D ZIPCPU dcache.v

read -formal -D ZIPCPU iscachable.v

read -formal -D ZIPCPU idecode.v

read -formal -D ZIPCPU wbdblpriarb.v

#

read -formal -D ZIPCPU fwb_counter.v

read -formal -D ZIPCPU fwb_master.v

read -formal -D ZIPCPU fwb_slave.v

read -formal -D ZIPCPU f_idecode.v

read -formal -D ZIPCPU abs_prefetch.v

read -formal -D ZIPCPU abs_div.v

read -formal -D ZIPCPU abs_mpy.v

#

read -formal zipcpu.v

chparam -set IMPLEMENT_FPU    0 zipcpu

dcache:

chparam -set OPT_LGDCACHE    10 zipcpu

no_dcache:

chparam -set OPT_LGDCACHE     0 zipcpu

full_proof:

chparam -set IMPLEMENT_MPY    1 zipcpu

chparam -set IMPLEMENT_DIVIDE 1 zipcpu

chparam -set EARLY_BRANCHING  1 zipcpu

chparam -set OPT_CIS          1 zipcpu

chparam -set OPT_PIPELINED    1 zipcpu

nopipe:

chparam -set IMPLEMENT_MPY    0 zipcpu

chparam -set IMPLEMENT_DIVIDE 0 zipcpu

chparam -set EARLY_BRANCHING  0 zipcpu

chparam -set OPT_CIS          1 zipcpu

chparam -set OPT_PIPELINED    0 zipcpu

lowlogic:

chparam -set OPT_CIS 0 zipcpu

--

prep -top zipcpu

[files]

../../rtl/core/zipcpu.v

../../rtl/core/cpuops.v

../../rtl/core/memops.v

../../rtl/core/pipemem.v

../../rtl/core/dcache.v

../../rtl/core/iscachable.v

../../rtl/core/idecode.v

../../rtl/ex/wbdblpriarb.v

#

../../rtl/ex/fwb_counter.v

../../rtl/ex/fwb_master.v

../../rtl/ex/fwb_slave.v

#

../../rtl/cpudefs.v

f_idecode.v

abs_prefetch.v

abs_div.v

abs_mpy.v

#