BINARY_SWITCH.smv

MODULE BINARY_SWITCH(BSWITCH_CONTROL_S, BSWITCH_CONTROL_S_FAULT, BSWITCH_CONTROL_S_CONNECTED, BSWITCH_INP_SIGN_1, BSWITCH_INP_SIGN_1_FAULT, BSWITCH_INP_SIGN_1_CONNECTED, BSWITCH_INP_SIGN_2, BSWITCH_INP_SIGN_2_FAULT, BSWITCH_INP_SIGN_2_CONNECTED, BSWITCH_CONTROL)
    DEFINE
        switch := BSWITCH_CONTROL_S_CONNECTED ? BSWITCH_CONTROL_S : BSWITCH_CONTROL;
        BSWITCH_OUTP_SIGN := switch ? BSWITCH_INP_SIGN_2 : BSWITCH_INP_SIGN_1;
        BSWITCH_OUTP_SIGN_FAULT := FALSE;