OpenCores
URL https://opencores.org/ocsvn/zipcpu/zipcpu/trunk

Subversion Repositories zipcpu

[/] [zipcpu/] [trunk/] [bench/] [formal/] [zipcpu.sby] - Rev 209

Compare with Previous | Blame | View Log

[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
#

Compare with Previous | Blame | View Log

powered by: WebSVN 2.1.0

© copyright 1999-2021 OpenCores.org, equivalent to Oliscience, all rights reserved. OpenCores®, registered trademark.