diff --git a/formal/ddr3_multiconfig.sby b/formal/ddr3_multiconfig.sby deleted file mode 100644 index 2e6f2b1..0000000 --- a/formal/ddr3_multiconfig.sby +++ /dev/null @@ -1,92 +0,0 @@ -[tasks] -prf2lanes_83MHz prf opt_2lanes opt_83MHz opt_with_ODELAY -prf4lanes_83MHz prf opt_4lanes opt_83MHz opt_with_ODELAY -prf8lanes_83MHz prf opt_8lanes opt_83MHz opt_with_ODELAY opt_WB_ERR -prf2lanes_100MHz prf opt_2lanes opt_100MHz opt_with_ODELAY opt_WB_ERR -prf4lanes_100MHz prf opt_4lanes opt_100MHz opt_with_ODELAY -prf8lanes_100MHz prf opt_8lanes opt_100MHz opt_with_ODELAY -prf_no_ODELAY prf opt_8lanes opt_100MHz -prf2lanes_83MHz_ECC_2 prf opt_2lanes opt_83MHz opt_with_ODELAY opt_ECC_2 -prf8lanes_100MHz_ECC_2 prf opt_8lanes opt_100MHz opt_ECC_2 -prf8lanes_100MHz_ECC_2_err prf opt_8lanes opt_100MHz opt_with_ODELAY opt_ECC_2 opt_WB_ERR -prf2lanes_83MHz_ECC_1 prf opt_2lanes opt_83MHz opt_with_ODELAY opt_ECC_1 -prf8lanes_100MHz_ECC_1 prf opt_8lanes opt_100MHz opt_ECC_1 -prf8lanes_100MHz_ECC_1_err prf opt_8lanes opt_100MHz opt_with_ODELAY opt_ECC_1 opt_WB_ERR -prf8lanes_100MHz_rbc_0 prf opt_8lanes opt_100MHz opt_with_ODELAY opt_rbc_0 -prf8lanes_ECC_1_rbc_2 prf opt_8lanes opt_100MHz opt_with_ODELAY opt_ECC_1 opt_rbc_2 - -[options] -prf: mode prove -prf: depth 7 - -[engines] -prf: smtbmc - -[script] -read -formal ddr3_controller.v -read -formal fwb_slave.v -read -formal ecc_dec.sv -read -formal ecc_enc.sv - ---pycode-begin-- - -# Number of Lanes -if "opt_2lanes" in tags: - cmd = "chparam -set LANES 2 ddr3_controller\n" -elif "opt_4lanes" in tags: - cmd = "chparam -set LANES 4 ddr3_controller\n" -elif "opt_8lanes" in tags: - cmd = "chparam -set LANES 8 ddr3_controller\n" -else: - cmd = "chparam -set LANES 8 ddr3_controller\n" - -# Clock period -if "opt_83MHz" in tags: - cmd += "chparam -set CONTROLLER_CLK_PERIOD 12000 ddr3_controller\n" - cmd += "chparam -set DDR3_CLK_PERIOD 3000 ddr3_controller\n" -elif "opt_100MHz" in tags: - cmd += "chparam -set CONTROLLER_CLK_PERIOD 10000 ddr3_controller\n" - cmd += "chparam -set DDR3_CLK_PERIOD 2500 ddr3_controller\n" -else: - cmd += "chparam -set CONTROLLER_CLK_PERIOD 10000 ddr3_controller\n" - cmd += "chparam -set DDR3_CLK_PERIOD 2500 ddr3_controller\n" - -# ODELAY support -if "opt_with_ODELAY" in tags: - cmd += "chparam -set ODELAY_SUPPORTED 1 ddr3_controller\n" -else: - cmd += "chparam -set ODELAY_SUPPORTED 0 ddr3_controller\n" - -# ECC -if "opt_ECC_2" in tags: - cmd += "chparam -set ECC_ENABLE 2 ddr3_controller\n" -elif "opt_ECC_1" in tags: - cmd += "chparam -set ECC_ENABLE 1 ddr3_controller\n" -else: - cmd += "chparam -set ECC_ENABLE 0 ddr3_controller\n" - -# Row_Bank_Col Memory Mapping -if "opt_rbc_0" in tags: - cmd += "chparam -set row_bank_col 0 ddr3_controller\n" -elif "opt_rbc_2" in tags: - cmd += "chparam -set row_bank_col 2 ddr3_controller\n" -else: - cmd += "chparam -set row_bank_col 1 ddr3_controller\n" - -# Wishbone Error -if "opt_WB_ERR" in tags: - cmd += "chparam -set WB_ERROR 1 ddr3_controller\n" -else: - cmd += "chparam -set WB_ERROR 0 ddr3_controller\n" - -output(cmd) ---pycode-end-- - -prep -top ddr3_controller - -[files] -./rtl/ddr3_controller.v -./formal/fwb_slave.v -./rtl/ecc/ecc_dec.sv -./rtl/ecc/ecc_enc.sv - diff --git a/formal/ddr3_singleconfig.sby b/formal/ddr3_singleconfig.sby index de2d0ad..6128254 100644 --- a/formal/ddr3_singleconfig.sby +++ b/formal/ddr3_singleconfig.sby @@ -10,8 +10,13 @@ smtbmc [script] read -formal ddr3_controller.v read -formal fwb_slave.v +read -formal ecc_dec.sv +read -formal ecc_enc.sv prep -top ddr3_controller + [files] ./rtl/ddr3_controller.v ./formal/fwb_slave.v +./rtl/ecc/ecc_dec.sv +./rtl/ecc/ecc_enc.sv diff --git a/formal/ecc.sby b/formal/ecc.sby new file mode 100644 index 0000000..9edc845 --- /dev/null +++ b/formal/ecc.sby @@ -0,0 +1,20 @@ +[options] +mode prove +depth 1 +#mode cover +#depth 50 + +[engines] +smtbmc + +[script] +read -formal ecc_formal.v +read -formal ecc_dec.sv +read -formal ecc_enc.sv +prep -top ecc_formal + + +[files] +./formal/ecc_formal.v +./rtl/ecc/ecc_dec.sv +./rtl/ecc/ecc_enc.sv