Payload Checker

Author: Tomas Kratochvila

This verification of Payload Checker were motivated by request from the hardware designer Jiri Tobola.

In the Cadence SMV sources the lbconn_mem_983040_12_notri module were abstracted. This means that every possible output from this module is taken into acount.

VHDL source list from CVS: liberouter/vhdl_design (date: 2005-02-18 18:45)

units/lb/lbconn_mem.vhd (vhdl)
units/lb/local_bus.vhd (vhdl)
units/common/pkg/math_pack.vhd (vhdl)
projects/scampi_ph2/pkg/commands.vhd (vhdl)
units/common/cmd_dec/cmd_dec_cmp.vhd (vhdl)
units/common/cmd_dec/cmd_dec.vhd (vhdl)
projects/scampi_ph2/comp/pck/addr_dec.vhd (vhdl)
projects/scampi_ph2/comp/pck/cam_op.vhd (vhdl)
projects/scampi_ph2/comp/pck/data_buf.vhd (vhdl)
projects/scampi_ph2/comp/pck/op_ctrl.vhd (vhdl)
projects/scampi_ph2/comp/pck/res_ctrl.vhd (vhdl)
projects/scampi_ph2/comp/pck/pck_ent.vhd (vhdl)
projects/scampi_ph2/comp/pck/pck.vhd (vhdl)

Preconditions

fair_CLK: G ( (F CLK) & (F !CLK) ) Precondition that clock CLK is ticking.

fair_LBCLK: G ( (F LBCLK) & (F !LBCLK) ) Precondition that clock LBCLK is ticking.

fair_CMCLK: G ( (F CMCLK) & (F !CMCLK) ) Precondition that clock CMCLK is ticking.

fair_CLK_DV: G ( (F CLK_DV) & (F !CLK_DV) ) Precondition that clock CLK_DV is ticking.

fair_CLK_DV_PH180: G ( (F CLK_DV_PH180) & (F !CLK_DV_PH180) ) Precondition that clock CLK_DV_PH180 is ticking.

Formulas

pck_never_stops

     G (
         RESET
         ->
         F (
             !RESET & READY & INP_DATA_VLD & INP_EOP
             ->
	     F VALID
           )
       );

When the valid data comes to Payload Checker than Payload Checker signals VALID in future.

Preconditions:
fair_CLK, fair_LBCLK, fair_CMCLK, fair_CLK_DV, fair_CLK_DV_PH180

Verification takes 2315 MB of RAM and 75571501 BDD nodes were allocated.

Verified in 2903.38 s.

Payload Checker

Author: Tomas Kratochvila

This verification of Payload Checker were motivated by request from the hardware designer Jiri Tobola.

In the Cadence SMV sources the lbconn_mem_983040_12_notri module were abstracted. This means that every possible output from this module is taken into acount.

VHDL source list from CVS: liberouter/vhdl_design (date: 2005-02-24 21:21)

Preconditions

Formulas

pck_never_stops

     G (
         RESET
         ->
         F (
             !RESET & READY & INP_DATA_VLD & INP_EOP
             ->
	     F VALID
           )
       );

When the valid data comes to Payload Checker than Payload Checker signals VALID in future.

Preconditions:
fair_CLK, fair_LBCLK, fair_CMCLK, fair_CLK_DV, fair_CLK_DV_PH180

Verification takes 2315 MB of RAM and 75571501 BDD nodes were allocated.

Verified in 2900.31 s.

pck_never_stops_stronger

     G (
         RESET
         ->
         F (
             READY & INP_DATA_VLD
             ->
	     F VALID
           )
       );

When the Payload Checker is ready and valid data comes than Payload Checker signals VALID in future.

Preconditions:
fair_CLK, fair_LBCLK, fair_CMCLK, fair_CLK_DV, fair_CLK_DV_PH180

This strongest formulae do not have to be satisfied and moreover, takes more than 3 GB of memory.

pck_never_stops_strongest

     G (
         RESET
         ->
         F (
             READY
             ->
	     F VALID
           )
       );

When the Payload Checker is ready than Payload Checker signals VALID in future.

Preconditions:
fair_CLK, fair_LBCLK, fair_CMCLK, fair_CLK_DV, fair_CLK_DV_PH180

This stronger formulae do not have to be satisfied and moreover, takes more than 3 GB of memory.