fix sby for ecc

formal/ddr3_multiconfig.sby

@@ -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
-

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

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