EXTENDS Naturals
\* LOGIC <- 0..1
CONSTANT LOGIC
VARIABLES vcc_1v8_aon, pcie_vph, aon_vdd, pcie_vp, vddq_nand, core_vdd, fphy_vdd, hsstp_vph, hsstp_vp, pmic_reset
vars == <<vcc_1v8_aon, pcie_vph, aon_vdd, pcie_vp, vddq_nand, core_vdd, fphy_vdd, hsstp_vph, hsstp_vp, pmic_reset>>
Init ==
/\ vcc_1v8_aon = 0
/\ pcie_vph = 0
/\ aon_vdd = 0
/\ pcie_vp = 0
/\ vddq_nand = 0
/\ core_vdd = 0
/\ fphy_vdd = 0
/\ hsstp_vph = 0
/\ hsstp_vp = 0
/\ pmic_reset = 0
FullPowerUp ==
/\ vcc_1v8_aon = 0
/\ pcie_vph = 0
/\ aon_vdd = 0
/\ pcie_vp = 0
/\ vddq_nand = 0
/\ core_vdd = 0
/\ fphy_vdd = 0
/\ hsstp_vph \in LOGIC \*HSSTP is described as independent but wrong in diagram
/\ hsstp_vp \in LOGIC \*HSSTP is described as independent but wrong in diagram
/\ pmic_reset = 0
/\ vcc_1v8_aon' = 1
/\ pcie_vph' = 1
/\ aon_vdd' = 1
/\ pcie_vp' = 1
/\ vddq_nand' = 1
/\ core_vdd' = 1
/\ fphy_vdd' = 1
/\ hsstp_vph' = 1
/\ hsstp_vp' = 1
/\ pmic_reset' = 1
DPS2Entry ==
/\ pmic_reset = 1
/\ pcie_vph = 1
/\ aon_vdd = 1
/\ vcc_1v8_aon = 1
/\ pcie_vp = 1
/\ vddq_nand = 1
/\ core_vdd = 1
/\ fphy_vdd = 1
/\ pcie_vp' = 0
/\ vddq_nand' = 0
/\ core_vdd' = 0
/\ fphy_vdd' = 0
/\ \E logic \in LOGIC: /\ hsstp_vph = 1 /\ hsstp_vp = 1
/\ hsstp_vph' = logic /\ hsstp_vp' = logic
/\ UNCHANGED <<pmic_reset, vcc_1v8_aon, pcie_vph, aon_vdd>>
DPS2Exit ==
/\ vcc_1v8_aon = 1
/\ pcie_vph = 1
/\ pmic_reset = 1
/\ pcie_vp = 0
/\ pcie_vp' = 1
/\ vddq_nand = 0
/\ vddq_nand' = 1
/\ core_vdd = 0
/\ core_vdd' = 1
/\ fphy_vdd = 0
/\ fphy_vdd' = 1
/\ hsstp_vph \in LOGIC
/\ hsstp_vph' \in LOGIC
/\ hsstp_vp \in LOGIC
/\ hsstp_vp' \in LOGIC
/\ UNCHANGED <<vcc_1v8_aon, pcie_vph, aon_vdd, pmic_reset>>
FullPowerDown ==
/\ vcc_1v8_aon = 1
/\ vcc_1v8_aon' = 0
/\ pcie_vph = 1
/\ pcie_vph' = 0
/\ aon_vdd = 1
/\ aon_vdd' = 0
/\ pcie_vp = 1
/\ pcie_vp' = 0
/\ vddq_nand = 1
/\ vddq_nand' = 0
/\ core_vdd = 1
/\ core_vdd' = 0
/\ fphy_vdd = 1
/\ fphy_vdd' = 0
/\ pmic_reset = 1
/\ pmic_reset' = 0
/\ UNCHANGED <<hsstp_vph, hsstp_vp>>
Next ==
\/ FullPowerUp
\/ DPS2Entry
\/ DPS2Exit
\/ FullPowerDown
CannotDPS2ExitWithoutEntry == [][DPS2Entry => DPS2Exit]_vars
Spec == Init /\ [][Next]_vars
THEOREM Spec => CannotDPS2ExitWithoutEntry