package Crazyflie_Hardware

-- This package models the hardware architecture of the Crazyflie
-- See https://wiki.bitcraze.io/projects:crazyflie2:architecture:index
-- for details

public
  with Buses::I2C, Buses::SPI, Buses::UART;
  with Processors::ARM, Processor_Properties;

  with Crazyflie_Types;
  with Crazyflie_Errors;
  with EMV2;

  ---------------
  -- STM32F405 --
  ---------------

  -- STM32F405, Cortex-M4@160MHz, that handles the heavy work of
  -- flight control and everything else:
  --
  -- * Sensor reading and motor control
  -- * Flight control
  -- * Telemetry (including the battery voltage)
  -- * Additional user development

  processor STM32F405 extends Processors::ARM::Generic_ARM
  features
    i2c_bus  : requires bus access Buses::I2C::I2C.IMPL;
    spi_bus  : requires bus access Buses::SPI::SPI.IMPL;
    uart_bus : requires bus access Buses::UART::UART.IMPL;
    pwm_bus  : requires bus access PWM;

  properties
    Processor_Properties::Processor_Frequency => 168Mhz;
    --  XXX memory components ?

    Scheduling_Protocol => (POSIX_1003_HIGHEST_PRIORITY_FIRST_PROTOCOL);
    
   annex EMV2 {**
     use types Crazyflie_Errors;
     use behavior Crazyflie_Errors::simple;
         
     error propagations
        bindings : out propagation {Lost, ValueErroneous};
     flows
        f2 : error source bindings{ValueErroneous};
     end propagations;

     component error behavior
     transitions
       t1 : Operational -[binding{ValueErroneous}]-> Failed;
     propagations
       Failed -[]-> bindings{ValueErroneous}; -- XXX
     end component;

  **};
  end STM32F405;

  --------------
  -- nRF51822 --
  --------------

  -- A NRF51, Cortex-M0, that handles radio communication and power
  -- management:
  --
  -- * ON/OFF logic
  -- * Enabling power to the rest of the system (STM32, sensors and
  --   expansion board)
  -- * Battery charging management and voltage measurement
  -- * Master radio bootloader
  -- * Radio and BLE communication
  -- * Detect and check installed expansion boards

  processor nRF51822 extends Processors::ARM::Generic_ARM
  features
    uart_bus : requires bus access Buses::UART::UART.IMPL;

  properties
    Scheduling_Protocol => (RMS);
    Processor_Properties::PRocessor_Frequency => 168hz;
    --  XXX memory components ?
  end nRF51822;

  -------------
  -- MPU9250 --
  -------------

  device MPU9250
  features
    DOF6 : out data port Crazyflie_Types::Six_Axis.impl;
    i2c_bus : requires bus access Buses::I2C::I2C.impl;

  flows
    f1 : flow source DOF6 { latency => 200 us .. 500 us; };

  properties
    Dispatch_Protocol => Periodic;
    Period            => 10 ms;
    
  annex EMV2
   {**
     use types Crazyflie_Errors;
     use behavior Crazyflie_Errors::simple;

     error propagations
       DOF6 : out propagation{ValueErroneous};
     flows
       f1 : error source DOF6{ValueErroneous} when failed;
     end propagations; 
 
     properties
       EMV2::hazards => 
        ([  crossreference => "N/A";
            failure => "IMU value error";
            phases => ("in flight");
            description => "Accelerometer starts to send an erroneous value";
            comment => "Can be critical if not detected by the health monitoring";
        ]) applies to DOF6.ValueErroneous;
                
      EMV2::OccurrenceDistribution => [ ProbabilityValue => 3.4e-5 ; Distribution => Fixed;] applies to DOF6.ValueErroneous;     
   **};
  end MPU9250;

  ---------------
  -- Propeller --
  ---------------

  bus PWM
  end PWM;

  device Propeller
  features
    rate : in data port Crazyflie_Types::PWM_Rate;
    pwm_bus : requires bus access PWM;
  flows
    f1 : flow sink rate { latency => 100 us .. 100 us; };

  properties
    Dispatch_Protocol => Sporadic;

  end Propeller;

  ---------------
  -- Crazyflie --
  ---------------

  system Crazyflie
  end Crazyflie;

  system implementation Crazyflie.impl
  subcomponents
    STM32F405 : processor STM32F405;
    nrf51822 : processor nrf51822;

    MPU9250 : device MPU9250;
    M1 : device Propeller;
    M2 : device Propeller;
    M3 : device Propeller;
    M4 : device Propeller;

    UART : bus Buses::UART::UART.impl;
    I2C : bus Buses::I2C::I2C.impl;
    PWM : bus PWM;

  connections
    C1 : bus access STM32F405.uart_bus -> UART;
    C2 : bus access nrf51822.uart_bus -> UART;

    C3 : bus access STM32F405.i2c_bus -> i2c;
    C4 : bus access MPU9250.i2c_bus -> i2c;

    C5 : bus access M1.pwm_bus -> PWM;
    C6 : bus access M2.pwm_bus -> PWM;
    C7 : bus access M3.pwm_bus -> PWM;
    C8 : bus access M4.pwm_bus -> PWM;
    C9 : bus access STM32F405.pwm_bus -> PWM;

  end Crazyflie.impl;

end Crazyflie_Hardware;