#ifndef _BCM_GPIO_H_
#define _BCM_GPIO_H_


/*------------------------------------------------------------------------------------------*\
 * AVM:
 * Function specifications for GPIO access functions
 * using the simplified macros in 63138_map_part.h
 * via switch CONFIG_AVM_GPIO_ACCESS in
 * ACSL Version 1.9
\*------------------------------------------------------------------------------------------*/


/*------------------------------------------------------------------------------------------*\
\*------------------------------------------------------------------------------------------*/
/*@ requires \valid(GPIO);
    requires 0 <= (unsigned int)(gpio_num >> 5) < 5;

    ensures \result == ( (GPIO->GPIODir[((gpio_num >> 5) & 0x07)]) &
                                         (1 << (gpio_num & 0x1f)) ) >> (gpio_num & 0x1f);

    assigns \nothing;
 */
unsigned int bcm_gpio_get_dir(unsigned int gpio_num);


/*------------------------------------------------------------------------------------------*\
\*------------------------------------------------------------------------------------------*/
/*@ requires \valid(GPIO);
    requires 0 <= (unsigned int)(gpio_num >> 5) < 5;

    behavior GpioNumValidDirInput:
      assumes dir == 0;
      ensures ( (GPIO->GPIODir[((gpio_num >> 5) & 0x07)]) &
                                (1 << (gpio_num & 0x1f)) ) == 0;

    behavior GpioNumValidDirOutput:
      assumes (dir > 0);
      ensures ( (GPIO->GPIODir[((gpio_num >> 5) & 0x07)]) &
                                (1 << (gpio_num & 0x1f)) ) == (1 << (gpio_num & 0x1f));

    assigns GPIO->GPIODir[((gpio_num >> 5) & 0x07)];

    complete behaviors;
    disjoint behaviors;
 */
void bcm_gpio_set_dir(unsigned int gpio_num, unsigned int dir);


/*------------------------------------------------------------------------------------------*\
\*------------------------------------------------------------------------------------------*/
/*@ requires \valid(GPIO);
    requires 0 <= (unsigned int)(gpio_num >> 5) < 5;

    ensures \result == ( (GPIO->GPIOio[((gpio_num >> 5) & 0x07)]) &
                                        (1 << (gpio_num & 0x1f)) ) >> (gpio_num & 0x1f);

    assigns \nothing;
 */
unsigned int bcm_gpio_get_data(unsigned int gpio_num);


/*------------------------------------------------------------------------------------------*\
\*------------------------------------------------------------------------------------------*/
/*@ requires \valid(GPIO);
    requires 0 <= (unsigned int)(gpio_num >> 5) < 5;

    behavior GpioNumValidDataClear:
      assumes data == 0;
      ensures ( (GPIO->GPIOio[((gpio_num >> 5) & 0x07)]) &
                               (1 << (gpio_num & 0x1f)) ) == 0;

    behavior GpioNumValidDataSet:
      assumes (data > 0);
      ensures ( (GPIO->GPIOio[((gpio_num >> 5) & 0x07)]) &
                               (1 << (gpio_num & 0x1f)) ) == (1 << (gpio_num & 0x1f));

    assigns GPIO->GPIOio[((gpio_num >> 5) & 0x07)];

    complete behaviors;
    disjoint behaviors;
 */
void bcm_gpio_set_data(unsigned int gpio_num, unsigned int data);


/*------------------------------------------------------------------------------------------*\
 * AVM: Added for altering the first 64 GPIO pins in the 32 bit wide HW-registers
 * GPIO->GPIOio[0] and GPIO->GPIOio[1] simultaneously via an uint64 mask and value.
\*------------------------------------------------------------------------------------------*/
/*@ requires \valid(GPIO);

    ensures ( \let regs_orig = ((unsigned long long)(\old(GPIO->GPIOio[1])) << 31) ^ (\old(GPIO->GPIOio[0]));
                 \let regs_upd = (regs_orig & (~mask)) | (value & mask);
                    ((GPIO->GPIOio[1]) == (0xFFFFFFFFU & (regs_upd >> 31))) &&
                    ((GPIO->GPIOio[0]) == (0xFFFFFFFFU & regs_upd)) );

    assigns GPIO->GPIOio[0], GPIO->GPIOio[1];
 */
void bcm_gpio_set_bitmask(unsigned long long mask, unsigned long long value);


#if defined(CONFIG_BCM960333) || defined(_BCM960333_)
unsigned int bcm_gpio_get_funcmode(unsigned int gpio_num);
void bcm_gpio_set_funcmode(unsigned int gpio_num, unsigned int mode);
#endif


#endif // _BCM_GPIO_H_