From 3db72104ad5664ed320253a342e1b26ad2f7da28 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 13 May 2019 11:57:45 +0200 Subject: new example + moved random number generator to common files --- test/monniaux/heptagon_radio_transmitter/_main.c | 66 +++ test/monniaux/heptagon_radio_transmitter/_main.h | 9 + .../heptagon_radio_transmitter/pervasives.h | 45 ++ .../heptagon_radio_transmitter/radiotrans.c | 571 +++++++++++++++++++++ .../heptagon_radio_transmitter/radiotrans.h | 67 +++ .../radiotrans_controller.c | 160 ++++++ .../radiotrans_controller.h | 30 ++ .../radiotrans_controller_types.c | 9 + .../radiotrans_controller_types.h | 12 + .../heptagon_radio_transmitter/radiotrans_types.c | 149 ++++++ .../heptagon_radio_transmitter/radiotrans_types.h | 56 ++ 11 files changed, 1174 insertions(+) create mode 100644 test/monniaux/heptagon_radio_transmitter/_main.c create mode 100644 test/monniaux/heptagon_radio_transmitter/_main.h create mode 100644 test/monniaux/heptagon_radio_transmitter/pervasives.h create mode 100644 test/monniaux/heptagon_radio_transmitter/radiotrans.c create mode 100644 test/monniaux/heptagon_radio_transmitter/radiotrans.h create mode 100644 test/monniaux/heptagon_radio_transmitter/radiotrans_controller.c create mode 100644 test/monniaux/heptagon_radio_transmitter/radiotrans_controller.h create mode 100644 test/monniaux/heptagon_radio_transmitter/radiotrans_controller_types.c create mode 100644 test/monniaux/heptagon_radio_transmitter/radiotrans_controller_types.h create mode 100644 test/monniaux/heptagon_radio_transmitter/radiotrans_types.c create mode 100644 test/monniaux/heptagon_radio_transmitter/radiotrans_types.h (limited to 'test/monniaux/heptagon_radio_transmitter') diff --git a/test/monniaux/heptagon_radio_transmitter/_main.c b/test/monniaux/heptagon_radio_transmitter/_main.c new file mode 100644 index 00000000..707c921a --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/_main.c @@ -0,0 +1,66 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c -hepts -s main -target ctrln radiotrans.ept --- */ + +#include +#include +#include +#include "_main.h" +#include "../dm_random.c" + +static inline int get_bool(void) { + return dm_random_uint32() & 1; +} + +Radiotrans__main_mem mem; +int main(int argc, char** argv) { + int step_c; + int step_max; + int enter_tx; + int enter_rx; + int exit_rx; + int calibrate; + int sleep; + int wake_up; + int irq_tx_done; + int irq_on_packet; + int irq_end_of_packet; + int irq_end_of_calibration; + int irq_fifo_threshold; + int adc_on; + int adc_off; + Radiotrans__main_out _res; + step_c = 0; + step_max = 1000; + if ((argc==2)) { + step_max = atoi(argv[1]); + }; + Radiotrans__main_reset(&mem); + while ((!(step_max)||(step_c */ +/* */ +/***********************************************************************/ + +/* Pervasives module for the Heptagon compiler */ + +#ifndef DECADES_PERVASIVES_H +#define DECADES_PERVASIVES_H + +typedef float real; + +/* between(i, n) returns idx between 0 and n-1. */ +static inline int between(int idx, int n) +{ + int o = (idx >= n) ? n-1 : (idx < 0 ? 0 : idx); + return o; +} + +#endif + diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans.c b/test/monniaux/heptagon_radio_transmitter/radiotrans.c new file mode 100644 index 00000000..30d4f62d --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans.c @@ -0,0 +1,571 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c -hepts -s main -target ctrln radiotrans.ept --- */ + +#include +#include +#include +#include "radiotrans.h" + +void Radiotrans__transceiver_reset(Radiotrans__transceiver_mem* self) { + self->ck = Radiotrans__St_Idle; + self->pnr = false; +} + +void Radiotrans__transceiver_step(int enter_tx, int enter_rx, int exit_rx, + int calibrate, int sleep, int wake_up, + int irq_tx_done, int irq_on_packet, + int irq_end_of_packet, + int irq_end_of_calibration, + int irq_fifo_threshold, int ok, + Radiotrans__transceiver_out* _out, + Radiotrans__transceiver_mem* self) { + + int v_2; + Radiotrans__st v_1; + int v; + int v_3; + int v_13; + Radiotrans__st v_12; + int v_11; + Radiotrans__st v_10; + int v_9; + Radiotrans__st v_8; + int v_7; + int v_6; + int v_5; + int v_4; + int nr_St_Rx_Packet; + Radiotrans__st ns_St_Rx_Packet; + int red_St_Rx_Packet; + int nr_St_Rx; + Radiotrans__st ns_St_Rx; + int red_St_Rx; + int nr_St_Sleep; + Radiotrans__st ns_St_Sleep; + int red_St_Sleep; + int nr_St_Calibrate; + Radiotrans__st ns_St_Calibrate; + int red_St_Calibrate; + int nr_St_Tx; + Radiotrans__st ns_St_Tx; + int red_St_Tx; + int nr_St_Idle; + Radiotrans__st ns_St_Idle; + int red_St_Idle; + Radiotrans__st ns; + int r; + int nr; + r = self->pnr; + switch (self->ck) { + case Radiotrans__St_Rx_Packet: + if (irq_end_of_packet) { + ns_St_Rx_Packet = Radiotrans__St_Idle; + nr_St_Rx_Packet = true; + } else { + ns_St_Rx_Packet = Radiotrans__St_Rx_Packet; + nr_St_Rx_Packet = false; + }; + red_St_Rx_Packet = true; + ns = ns_St_Rx_Packet; + nr = nr_St_Rx_Packet; + _out->red = red_St_Rx_Packet; + break; + case Radiotrans__St_Rx: + v = (exit_rx&&ok); + if (v) { + v_1 = Radiotrans__St_Idle; + } else { + v_1 = Radiotrans__St_Rx; + }; + if (irq_on_packet) { + ns_St_Rx = Radiotrans__St_Rx_Packet; + } else { + ns_St_Rx = v_1; + }; + if (v) { + v_2 = true; + } else { + v_2 = false; + }; + if (irq_on_packet) { + nr_St_Rx = true; + } else { + nr_St_Rx = v_2; + }; + red_St_Rx = true; + ns = ns_St_Rx; + nr = nr_St_Rx; + _out->red = red_St_Rx; + break; + case Radiotrans__St_Sleep: + v_3 = (wake_up&&ok); + if (v_3) { + ns_St_Sleep = Radiotrans__St_Idle; + nr_St_Sleep = true; + } else { + ns_St_Sleep = Radiotrans__St_Sleep; + nr_St_Sleep = false; + }; + red_St_Sleep = false; + ns = ns_St_Sleep; + nr = nr_St_Sleep; + _out->red = red_St_Sleep; + break; + case Radiotrans__St_Calibrate: + if (irq_end_of_calibration) { + ns_St_Calibrate = Radiotrans__St_Idle; + nr_St_Calibrate = true; + } else { + ns_St_Calibrate = Radiotrans__St_Calibrate; + nr_St_Calibrate = false; + }; + red_St_Calibrate = false; + ns = ns_St_Calibrate; + nr = nr_St_Calibrate; + _out->red = red_St_Calibrate; + break; + case Radiotrans__St_Tx: + if (irq_tx_done) { + ns_St_Tx = Radiotrans__St_Idle; + nr_St_Tx = true; + } else { + ns_St_Tx = Radiotrans__St_Tx; + nr_St_Tx = false; + }; + red_St_Tx = true; + ns = ns_St_Tx; + nr = nr_St_Tx; + _out->red = red_St_Tx; + break; + case Radiotrans__St_Idle: + v_4 = (enter_tx&&ok); + v_5 = (calibrate&&ok); + v_6 = (sleep&&ok); + v_7 = (enter_rx&&ok); + if (v_7) { + v_8 = Radiotrans__St_Rx; + } else { + v_8 = Radiotrans__St_Idle; + }; + if (v_6) { + v_10 = Radiotrans__St_Sleep; + } else { + v_10 = v_8; + }; + if (v_5) { + v_12 = Radiotrans__St_Calibrate; + } else { + v_12 = v_10; + }; + if (v_4) { + ns_St_Idle = Radiotrans__St_Tx; + } else { + ns_St_Idle = v_12; + }; + ns = ns_St_Idle; + if (v_7) { + v_9 = true; + } else { + v_9 = false; + }; + if (v_6) { + v_11 = true; + } else { + v_11 = v_9; + }; + if (v_5) { + v_13 = true; + } else { + v_13 = v_11; + }; + if (v_4) { + nr_St_Idle = true; + } else { + nr_St_Idle = v_13; + }; + nr = nr_St_Idle; + red_St_Idle = false; + _out->red = red_St_Idle; + break; + default: + break; + }; + self->ck = ns; + self->pnr = nr;; +} + +void Radiotrans__adc_reset(Radiotrans__adc_mem* self) { + self->ck = Radiotrans__St_1_Off; + self->pnr = false; +} + +void Radiotrans__adc_step(int adc_on, int adc_off, int ok, + Radiotrans__adc_out* _out, + Radiotrans__adc_mem* self) { + + int v; + int v_14; + int nr_St_1_On; + Radiotrans__st_1 ns_St_1_On; + int o_St_1_On; + int nr_St_1_Off; + Radiotrans__st_1 ns_St_1_Off; + int o_St_1_Off; + Radiotrans__st_1 ns; + int r; + int nr; + r = self->pnr; + switch (self->ck) { + case Radiotrans__St_1_On: + v = (adc_off&&ok); + if (v) { + ns_St_1_On = Radiotrans__St_1_Off; + nr_St_1_On = true; + } else { + ns_St_1_On = Radiotrans__St_1_On; + nr_St_1_On = false; + }; + o_St_1_On = true; + ns = ns_St_1_On; + nr = nr_St_1_On; + _out->o = o_St_1_On; + break; + case Radiotrans__St_1_Off: + v_14 = (adc_on&&ok); + if (v_14) { + ns_St_1_Off = Radiotrans__St_1_On; + } else { + ns_St_1_Off = Radiotrans__St_1_Off; + }; + ns = ns_St_1_Off; + if (v_14) { + nr_St_1_Off = true; + } else { + nr_St_1_Off = false; + }; + nr = nr_St_1_Off; + o_St_1_Off = false; + _out->o = o_St_1_Off; + break; + default: + break; + }; + self->ck = ns; + self->pnr = nr;; +} + +void Radiotrans__main_reset(Radiotrans__main_mem* self) { + self->ck = Radiotrans__St_3_Idle; + self->pnr_1 = false; + self->ck_1 = Radiotrans__St_2_Off; + self->pnr = false; +} + +void Radiotrans__main_step(int enter_tx, int enter_rx, int exit_rx, + int calibrate, int sleep, int wake_up, + int irq_tx_done, int irq_on_packet, + int irq_end_of_packet, int irq_end_of_calibration, + int irq_fifo_threshold, int adc_on, int adc_off, + Radiotrans__main_out* _out, + Radiotrans__main_mem* self) { + Radiotrans_controller__main_ctrlr0_out Radiotrans_controller__main_ctrlr0_out_st; + + int v_15; + int v; + int ok_r; + int ok_a; + int v_18; + Radiotrans__st_3 v_17; + int v_16; + int v_19; + int v_29; + Radiotrans__st_3 v_28; + int v_27; + Radiotrans__st_3 v_26; + int v_25; + Radiotrans__st_3 v_24; + int v_23; + int v_22; + int v_21; + int v_20; + int nr_1_St_3_Rx_Packet; + Radiotrans__st_3 ns_1_St_3_Rx_Packet; + int red_1_St_3_Rx_Packet; + int nr_1_St_3_Rx; + Radiotrans__st_3 ns_1_St_3_Rx; + int red_1_St_3_Rx; + int nr_1_St_3_Sleep; + Radiotrans__st_3 ns_1_St_3_Sleep; + int red_1_St_3_Sleep; + int nr_1_St_3_Calibrate; + Radiotrans__st_3 ns_1_St_3_Calibrate; + int red_1_St_3_Calibrate; + int nr_1_St_3_Tx; + Radiotrans__st_3 ns_1_St_3_Tx; + int red_1_St_3_Tx; + int nr_1_St_3_Idle; + Radiotrans__st_3 ns_1_St_3_Idle; + int red_1_St_3_Idle; + int v_30; + int v_31; + int nr_St_2_On; + Radiotrans__st_2 ns_St_2_On; + int o_St_2_On; + int nr_St_2_Off; + Radiotrans__st_2 ns_St_2_Off; + int o_St_2_Off; + Radiotrans__st_3 ns_1; + int r_1; + int nr_1; + Radiotrans__st_2 ns; + int r; + int nr; + int adc_on_1; + int adc_off_1; + int ok_1; + int o; + int enter_tx_1; + int enter_rx_1; + int exit_rx_1; + int calibrate_1; + int sleep_1; + int wake_up_1; + int irq_tx_done_1; + int irq_on_packet_1; + int irq_end_of_packet_1; + int irq_end_of_calibration_1; + int irq_fifo_threshold_1; + int ok; + int red_1; + r_1 = self->pnr_1; + irq_fifo_threshold_1 = irq_fifo_threshold; + irq_end_of_calibration_1 = irq_end_of_calibration; + irq_end_of_packet_1 = irq_end_of_packet; + irq_on_packet_1 = irq_on_packet; + irq_tx_done_1 = irq_tx_done; + wake_up_1 = wake_up; + sleep_1 = sleep; + calibrate_1 = calibrate; + exit_rx_1 = exit_rx; + enter_rx_1 = enter_rx; + enter_tx_1 = enter_tx; + r = self->pnr; + adc_off_1 = adc_off; + adc_on_1 = adc_on; + switch (self->ck) { + case Radiotrans__St_3_Rx_Packet: + if (irq_end_of_packet_1) { + ns_1_St_3_Rx_Packet = Radiotrans__St_3_Idle; + nr_1_St_3_Rx_Packet = true; + } else { + ns_1_St_3_Rx_Packet = Radiotrans__St_3_Rx_Packet; + nr_1_St_3_Rx_Packet = false; + }; + red_1_St_3_Rx_Packet = true; + red_1 = red_1_St_3_Rx_Packet; + break; + case Radiotrans__St_3_Rx: + red_1_St_3_Rx = true; + red_1 = red_1_St_3_Rx; + break; + case Radiotrans__St_3_Sleep: + red_1_St_3_Sleep = false; + red_1 = red_1_St_3_Sleep; + break; + case Radiotrans__St_3_Calibrate: + if (irq_end_of_calibration_1) { + ns_1_St_3_Calibrate = Radiotrans__St_3_Idle; + nr_1_St_3_Calibrate = true; + } else { + ns_1_St_3_Calibrate = Radiotrans__St_3_Calibrate; + nr_1_St_3_Calibrate = false; + }; + red_1_St_3_Calibrate = false; + red_1 = red_1_St_3_Calibrate; + break; + case Radiotrans__St_3_Tx: + if (irq_tx_done_1) { + ns_1_St_3_Tx = Radiotrans__St_3_Idle; + nr_1_St_3_Tx = true; + } else { + ns_1_St_3_Tx = Radiotrans__St_3_Tx; + nr_1_St_3_Tx = false; + }; + red_1_St_3_Tx = true; + red_1 = red_1_St_3_Tx; + break; + case Radiotrans__St_3_Idle: + red_1_St_3_Idle = false; + red_1 = red_1_St_3_Idle; + break; + default: + break; + }; + _out->red = red_1; + switch (self->ck_1) { + case Radiotrans__St_2_On: + o_St_2_On = true; + o = o_St_2_On; + break; + case Radiotrans__St_2_Off: + o_St_2_Off = false; + o = o_St_2_Off; + break; + default: + break; + }; + _out->a_on = o; + Radiotrans_controller__main_ctrlr0_step(adc_off, adc_on, calibrate, + self->ck, self->ck_1, enter_rx, + enter_tx, exit_rx, + irq_end_of_calibration, + irq_end_of_packet, + irq_fifo_threshold, irq_on_packet, + irq_tx_done, self->pnr, + self->pnr_1, sleep, wake_up, + &Radiotrans_controller__main_ctrlr0_out_st); + ok_a = Radiotrans_controller__main_ctrlr0_out_st.ok_a; + ok_r = Radiotrans_controller__main_ctrlr0_out_st.ok_r; + ok = ok_r; + ok_1 = ok_a; + switch (self->ck) { + case Radiotrans__St_3_Rx: + v_16 = (exit_rx_1&&ok); + if (v_16) { + v_17 = Radiotrans__St_3_Idle; + } else { + v_17 = Radiotrans__St_3_Rx; + }; + if (irq_on_packet_1) { + ns_1_St_3_Rx = Radiotrans__St_3_Rx_Packet; + } else { + ns_1_St_3_Rx = v_17; + }; + if (v_16) { + v_18 = true; + } else { + v_18 = false; + }; + if (irq_on_packet_1) { + nr_1_St_3_Rx = true; + } else { + nr_1_St_3_Rx = v_18; + }; + ns_1 = ns_1_St_3_Rx; + nr_1 = nr_1_St_3_Rx; + break; + case Radiotrans__St_3_Sleep: + v_19 = (wake_up_1&&ok); + if (v_19) { + ns_1_St_3_Sleep = Radiotrans__St_3_Idle; + nr_1_St_3_Sleep = true; + } else { + ns_1_St_3_Sleep = Radiotrans__St_3_Sleep; + nr_1_St_3_Sleep = false; + }; + ns_1 = ns_1_St_3_Sleep; + nr_1 = nr_1_St_3_Sleep; + break; + case Radiotrans__St_3_Idle: + v_20 = (enter_tx_1&&ok); + v_21 = (calibrate_1&&ok); + v_22 = (sleep_1&&ok); + v_23 = (enter_rx_1&&ok); + if (v_23) { + v_24 = Radiotrans__St_3_Rx; + } else { + v_24 = Radiotrans__St_3_Idle; + }; + if (v_22) { + v_26 = Radiotrans__St_3_Sleep; + } else { + v_26 = v_24; + }; + if (v_21) { + v_28 = Radiotrans__St_3_Calibrate; + } else { + v_28 = v_26; + }; + if (v_20) { + ns_1_St_3_Idle = Radiotrans__St_3_Tx; + } else { + ns_1_St_3_Idle = v_28; + }; + ns_1 = ns_1_St_3_Idle; + if (v_23) { + v_25 = true; + } else { + v_25 = false; + }; + if (v_22) { + v_27 = true; + } else { + v_27 = v_25; + }; + if (v_21) { + v_29 = true; + } else { + v_29 = v_27; + }; + if (v_20) { + nr_1_St_3_Idle = true; + } else { + nr_1_St_3_Idle = v_29; + }; + nr_1 = nr_1_St_3_Idle; + break; + case Radiotrans__St_3_Rx_Packet: + ns_1 = ns_1_St_3_Rx_Packet; + nr_1 = nr_1_St_3_Rx_Packet; + break; + case Radiotrans__St_3_Calibrate: + ns_1 = ns_1_St_3_Calibrate; + nr_1 = nr_1_St_3_Calibrate; + break; + case Radiotrans__St_3_Tx: + ns_1 = ns_1_St_3_Tx; + nr_1 = nr_1_St_3_Tx; + break; + default: + break; + }; + switch (self->ck_1) { + case Radiotrans__St_2_On: + v_30 = (adc_off_1&&ok_1); + if (v_30) { + ns_St_2_On = Radiotrans__St_2_Off; + nr_St_2_On = true; + } else { + ns_St_2_On = Radiotrans__St_2_On; + nr_St_2_On = false; + }; + ns = ns_St_2_On; + nr = nr_St_2_On; + break; + case Radiotrans__St_2_Off: + v_31 = (adc_on_1&&ok_1); + if (v_31) { + ns_St_2_Off = Radiotrans__St_2_On; + } else { + ns_St_2_Off = Radiotrans__St_2_Off; + }; + ns = ns_St_2_Off; + if (v_31) { + nr_St_2_Off = true; + } else { + nr_St_2_Off = false; + }; + nr = nr_St_2_Off; + break; + default: + break; + }; + self->ck = ns_1; + self->pnr_1 = nr_1; + self->ck_1 = ns; + self->pnr = nr; + v = (_out->a_on&&_out->red); + v_15 = !(v);; +} + diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans.h b/test/monniaux/heptagon_radio_transmitter/radiotrans.h new file mode 100644 index 00000000..1d68ad5c --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans.h @@ -0,0 +1,67 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c -hepts -s main -target ctrln radiotrans.ept --- */ + +#ifndef RADIOTRANS_H +#define RADIOTRANS_H + +#include "radiotrans_types.h" +#include "radiotrans_controller.h" +typedef struct Radiotrans__transceiver_mem { + Radiotrans__st ck; + int pnr; +} Radiotrans__transceiver_mem; + +typedef struct Radiotrans__transceiver_out { + int red; +} Radiotrans__transceiver_out; + +void Radiotrans__transceiver_reset(Radiotrans__transceiver_mem* self); + +void Radiotrans__transceiver_step(int enter_tx, int enter_rx, int exit_rx, + int calibrate, int sleep, int wake_up, + int irq_tx_done, int irq_on_packet, + int irq_end_of_packet, + int irq_end_of_calibration, + int irq_fifo_threshold, int ok, + Radiotrans__transceiver_out* _out, + Radiotrans__transceiver_mem* self); + +typedef struct Radiotrans__adc_mem { + Radiotrans__st_1 ck; + int pnr; +} Radiotrans__adc_mem; + +typedef struct Radiotrans__adc_out { + int o; +} Radiotrans__adc_out; + +void Radiotrans__adc_reset(Radiotrans__adc_mem* self); + +void Radiotrans__adc_step(int adc_on, int adc_off, int ok, + Radiotrans__adc_out* _out, + Radiotrans__adc_mem* self); + +typedef struct Radiotrans__main_mem { + Radiotrans__st_3 ck; + Radiotrans__st_2 ck_1; + int pnr_1; + int pnr; +} Radiotrans__main_mem; + +typedef struct Radiotrans__main_out { + int a_on; + int red; +} Radiotrans__main_out; + +void Radiotrans__main_reset(Radiotrans__main_mem* self); + +void Radiotrans__main_step(int enter_tx, int enter_rx, int exit_rx, + int calibrate, int sleep, int wake_up, + int irq_tx_done, int irq_on_packet, + int irq_end_of_packet, int irq_end_of_calibration, + int irq_fifo_threshold, int adc_on, int adc_off, + Radiotrans__main_out* _out, + Radiotrans__main_mem* self); + +#endif // RADIOTRANS_H diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans_controller.c b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller.c new file mode 100644 index 00000000..8cc6d512 --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller.c @@ -0,0 +1,160 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c radiotrans_controller.ept --- */ + +#include +#include +#include +#include "radiotrans_controller.h" + +void Radiotrans_controller__main_ctrlr0_step(int adc_off, int adc_on, + int calibrate, + Radiotrans__st_3 ck, + Radiotrans__st_2 ck_1, + int enter_rx, int enter_tx, + int exit_rx, + int irq_end_of_calibration, + int irq_end_of_packet, + int irq_fifo_threshold, + int irq_on_packet, + int irq_tx_done, int pnr, + int pnr_1, int sleep, + int wake_up, + Radiotrans_controller__main_ctrlr0_out* _out) { + + int v_22; + int v_21; + int v_20; + int v_19; + int v_18; + int v_17; + int v_16; + int v_15; + int v_14; + int v_13; + int v_12; + int v_11; + int v_10; + int v_9; + int v_8; + int v_7; + int v_6; + int v_5; + int v_4; + int v_3; + int v_2; + int v_1; + int v; + int l52; + int l51; + int l50; + int l49; + int l48; + int l47; + int l46; + int l45; + int l44; + int l43; + int l42; + int l41; + int l40; + int l39; + int l38; + int l37; + int l36; + int l35; + int l34; + int l33; + int l32; + v_22 = (ck==Radiotrans__St_3_Rx_Packet); + v_21 = !(adc_on); + l51 = (v_21||irq_end_of_packet); + v_20 = (ck==Radiotrans__St_3_Tx); + v_19 = !(adc_on); + l49 = (v_19||irq_tx_done); + v_18 = (ck==Radiotrans__St_3_Rx); + v_17 = !(adc_on); + v_16 = !(adc_on); + v_15 = !(adc_on); + v_14 = !(irq_on_packet); + l45 = (v_14||v_15); + if (exit_rx) { + l46 = l45; + } else { + l46 = v_16; + }; + v_12 = (ck==Radiotrans__St_3_Idle); + v_13 = !(v_12); + v_11 = (ck_1==Radiotrans__St_2_On); + v_9 = !(adc_on); + v_8 = !(adc_on); + v_7 = !(enter_tx); + l38 = (v_7||v_8); + if (sleep) { + l39 = l38; + } else { + l39 = v_9; + }; + if (enter_rx) { + l40 = l39; + } else { + l40 = l38; + }; + if (calibrate) { + l41 = l38; + } else { + l41 = l40; + }; + v_5 = (ck==Radiotrans__St_3_Rx); + v_3 = (ck==Radiotrans__St_3_Calibrate); + v_2 = (ck==Radiotrans__St_3_Sleep); + v_4 = (v_2||v_3); + v_6 = (v_4||v_5); + v_1 = (ck_1==Radiotrans__St_2_Off); + v = !(enter_tx); + l32 = (v||adc_off); + if (sleep) { + l33 = l32; + } else { + l33 = adc_off; + }; + if (enter_rx) { + l34 = l33; + } else { + l34 = l32; + }; + if (calibrate) { + l35 = l32; + } else { + l35 = l34; + }; + l36 = (v_1||l35); + l37 = (v_6||l36); + _out->ok_r = l37; + if (_out->ok_r) { + l47 = l46; + } else { + l47 = v_17; + }; + v_10 = !(_out->ok_r); + l42 = (v_10||l41); + l43 = (v_11||l42); + l44 = (v_13||l43); + if (v_18) { + l48 = l47; + } else { + l48 = l44; + }; + if (v_20) { + l50 = l49; + } else { + l50 = l48; + }; + if (v_22) { + l52 = l51; + } else { + l52 = l50; + }; + _out->ok_a = l52;; +} + diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans_controller.h b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller.h new file mode 100644 index 00000000..45681ada --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller.h @@ -0,0 +1,30 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c radiotrans_controller.ept --- */ + +#ifndef RADIOTRANS_CONTROLLER_H +#define RADIOTRANS_CONTROLLER_H + +#include "radiotrans_controller_types.h" +#include "radiotrans.h" +typedef struct Radiotrans_controller__main_ctrlr0_out { + int ok_a; + int ok_r; +} Radiotrans_controller__main_ctrlr0_out; + +void Radiotrans_controller__main_ctrlr0_step(int adc_off, int adc_on, + int calibrate, + Radiotrans__st_3 ck, + Radiotrans__st_2 ck_1, + int enter_rx, int enter_tx, + int exit_rx, + int irq_end_of_calibration, + int irq_end_of_packet, + int irq_fifo_threshold, + int irq_on_packet, + int irq_tx_done, int pnr, + int pnr_1, int sleep, + int wake_up, + Radiotrans_controller__main_ctrlr0_out* _out); + +#endif // RADIOTRANS_CONTROLLER_H diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans_controller_types.c b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller_types.c new file mode 100644 index 00000000..a3c3972f --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller_types.c @@ -0,0 +1,9 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c radiotrans_controller.ept --- */ + +#include +#include +#include +#include "radiotrans_controller_types.h" + diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans_controller_types.h b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller_types.h new file mode 100644 index 00000000..9a081213 --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans_controller_types.h @@ -0,0 +1,12 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c radiotrans_controller.ept --- */ + +#ifndef RADIOTRANS_CONTROLLER_TYPES_H +#define RADIOTRANS_CONTROLLER_TYPES_H + +#include "stdbool.h" +#include "assert.h" +#include "pervasives.h" +#include "radiotrans_types.h" +#endif // RADIOTRANS_CONTROLLER_TYPES_H diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans_types.c b/test/monniaux/heptagon_radio_transmitter/radiotrans_types.c new file mode 100644 index 00000000..cc62575d --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans_types.c @@ -0,0 +1,149 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c -hepts -s main -target ctrln radiotrans.ept --- */ + +#include +#include +#include +#include "radiotrans_types.h" + +Radiotrans__st_3 Radiotrans__st_3_of_string(char* s) { + if ((strcmp(s, "St_3_Tx")==0)) { + return Radiotrans__St_3_Tx; + }; + if ((strcmp(s, "St_3_Sleep")==0)) { + return Radiotrans__St_3_Sleep; + }; + if ((strcmp(s, "St_3_Rx_Packet")==0)) { + return Radiotrans__St_3_Rx_Packet; + }; + if ((strcmp(s, "St_3_Rx")==0)) { + return Radiotrans__St_3_Rx; + }; + if ((strcmp(s, "St_3_Idle")==0)) { + return Radiotrans__St_3_Idle; + }; + if ((strcmp(s, "St_3_Calibrate")==0)) { + return Radiotrans__St_3_Calibrate; + }; +} + +char* string_of_Radiotrans__st_3(Radiotrans__st_3 x, char* buf) { + switch (x) { + case Radiotrans__St_3_Tx: + strcpy(buf, "St_3_Tx"); + break; + case Radiotrans__St_3_Sleep: + strcpy(buf, "St_3_Sleep"); + break; + case Radiotrans__St_3_Rx_Packet: + strcpy(buf, "St_3_Rx_Packet"); + break; + case Radiotrans__St_3_Rx: + strcpy(buf, "St_3_Rx"); + break; + case Radiotrans__St_3_Idle: + strcpy(buf, "St_3_Idle"); + break; + case Radiotrans__St_3_Calibrate: + strcpy(buf, "St_3_Calibrate"); + break; + default: + break; + }; + return buf; +} + +Radiotrans__st_2 Radiotrans__st_2_of_string(char* s) { + if ((strcmp(s, "St_2_On")==0)) { + return Radiotrans__St_2_On; + }; + if ((strcmp(s, "St_2_Off")==0)) { + return Radiotrans__St_2_Off; + }; +} + +char* string_of_Radiotrans__st_2(Radiotrans__st_2 x, char* buf) { + switch (x) { + case Radiotrans__St_2_On: + strcpy(buf, "St_2_On"); + break; + case Radiotrans__St_2_Off: + strcpy(buf, "St_2_Off"); + break; + default: + break; + }; + return buf; +} + +Radiotrans__st_1 Radiotrans__st_1_of_string(char* s) { + if ((strcmp(s, "St_1_On")==0)) { + return Radiotrans__St_1_On; + }; + if ((strcmp(s, "St_1_Off")==0)) { + return Radiotrans__St_1_Off; + }; +} + +char* string_of_Radiotrans__st_1(Radiotrans__st_1 x, char* buf) { + switch (x) { + case Radiotrans__St_1_On: + strcpy(buf, "St_1_On"); + break; + case Radiotrans__St_1_Off: + strcpy(buf, "St_1_Off"); + break; + default: + break; + }; + return buf; +} + +Radiotrans__st Radiotrans__st_of_string(char* s) { + if ((strcmp(s, "St_Tx")==0)) { + return Radiotrans__St_Tx; + }; + if ((strcmp(s, "St_Sleep")==0)) { + return Radiotrans__St_Sleep; + }; + if ((strcmp(s, "St_Rx_Packet")==0)) { + return Radiotrans__St_Rx_Packet; + }; + if ((strcmp(s, "St_Rx")==0)) { + return Radiotrans__St_Rx; + }; + if ((strcmp(s, "St_Idle")==0)) { + return Radiotrans__St_Idle; + }; + if ((strcmp(s, "St_Calibrate")==0)) { + return Radiotrans__St_Calibrate; + }; +} + +char* string_of_Radiotrans__st(Radiotrans__st x, char* buf) { + switch (x) { + case Radiotrans__St_Tx: + strcpy(buf, "St_Tx"); + break; + case Radiotrans__St_Sleep: + strcpy(buf, "St_Sleep"); + break; + case Radiotrans__St_Rx_Packet: + strcpy(buf, "St_Rx_Packet"); + break; + case Radiotrans__St_Rx: + strcpy(buf, "St_Rx"); + break; + case Radiotrans__St_Idle: + strcpy(buf, "St_Idle"); + break; + case Radiotrans__St_Calibrate: + strcpy(buf, "St_Calibrate"); + break; + default: + break; + }; + return buf; +} + diff --git a/test/monniaux/heptagon_radio_transmitter/radiotrans_types.h b/test/monniaux/heptagon_radio_transmitter/radiotrans_types.h new file mode 100644 index 00000000..826ed65c --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/radiotrans_types.h @@ -0,0 +1,56 @@ +/* --- Generated the 13/5/2019 at 10:21 --- */ +/* --- heptagon compiler, version 1.05.00 (compiled mon. may. 13 10:18:8 CET 2019) --- */ +/* --- Command line: /local/STATOR/packages/opam-root/4.07.1/bin/heptc -target c -hepts -s main -target ctrln radiotrans.ept --- */ + +#ifndef RADIOTRANS_TYPES_H +#define RADIOTRANS_TYPES_H + +#include "stdbool.h" +#include "assert.h" +#include "pervasives.h" +#include "radiotrans_controller_types.h" +typedef enum { + Radiotrans__St_3_Tx, + Radiotrans__St_3_Sleep, + Radiotrans__St_3_Rx_Packet, + Radiotrans__St_3_Rx, + Radiotrans__St_3_Idle, + Radiotrans__St_3_Calibrate +} Radiotrans__st_3; + +Radiotrans__st_3 Radiotrans__st_3_of_string(char* s); + +char* string_of_Radiotrans__st_3(Radiotrans__st_3 x, char* buf); + +typedef enum { + Radiotrans__St_2_On, + Radiotrans__St_2_Off +} Radiotrans__st_2; + +Radiotrans__st_2 Radiotrans__st_2_of_string(char* s); + +char* string_of_Radiotrans__st_2(Radiotrans__st_2 x, char* buf); + +typedef enum { + Radiotrans__St_1_On, + Radiotrans__St_1_Off +} Radiotrans__st_1; + +Radiotrans__st_1 Radiotrans__st_1_of_string(char* s); + +char* string_of_Radiotrans__st_1(Radiotrans__st_1 x, char* buf); + +typedef enum { + Radiotrans__St_Tx, + Radiotrans__St_Sleep, + Radiotrans__St_Rx_Packet, + Radiotrans__St_Rx, + Radiotrans__St_Idle, + Radiotrans__St_Calibrate +} Radiotrans__st; + +Radiotrans__st Radiotrans__st_of_string(char* s); + +char* string_of_Radiotrans__st(Radiotrans__st x, char* buf); + +#endif // RADIOTRANS_TYPES_H -- cgit From 1792797a37be314ab8a257b55b2f5530b15f08f1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 13 May 2019 12:03:34 +0200 Subject: clock the time in heptagon --- test/monniaux/heptagon_radio_transmitter/_main.c | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'test/monniaux/heptagon_radio_transmitter') diff --git a/test/monniaux/heptagon_radio_transmitter/_main.c b/test/monniaux/heptagon_radio_transmitter/_main.c index 707c921a..635d660f 100644 --- a/test/monniaux/heptagon_radio_transmitter/_main.c +++ b/test/monniaux/heptagon_radio_transmitter/_main.c @@ -6,6 +6,7 @@ #include #include #include "_main.h" +#include "../clock.h" #include "../dm_random.c" static inline int get_bool(void) { @@ -35,6 +36,9 @@ int main(int argc, char** argv) { if ((argc==2)) { step_max = atoi(argv[1]); }; + + clock_prepare(); + clock_start(); Radiotrans__main_reset(&mem); while ((!(step_max)||(step_c Date: Thu, 6 Jun 2019 12:01:53 +0200 Subject: some more benchmarks --- test/monniaux/heptagon_radio_transmitter/make.proto | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 test/monniaux/heptagon_radio_transmitter/make.proto (limited to 'test/monniaux/heptagon_radio_transmitter') diff --git a/test/monniaux/heptagon_radio_transmitter/make.proto b/test/monniaux/heptagon_radio_transmitter/make.proto new file mode 100644 index 00000000..40de14dc --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/make.proto @@ -0,0 +1,3 @@ +sources: "$(wildcard *.c)" +target: radiotrans +measures: [cycles] -- cgit From b288b587378984c3c419d26a13dcf93686d1b779 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 17 Jul 2019 12:03:39 +0200 Subject: All working benches ported --- test/monniaux/heptagon_radio_transmitter/Makefile | 3 +++ test/monniaux/heptagon_radio_transmitter/make.proto | 3 --- 2 files changed, 3 insertions(+), 3 deletions(-) create mode 100644 test/monniaux/heptagon_radio_transmitter/Makefile delete mode 100644 test/monniaux/heptagon_radio_transmitter/make.proto (limited to 'test/monniaux/heptagon_radio_transmitter') diff --git a/test/monniaux/heptagon_radio_transmitter/Makefile b/test/monniaux/heptagon_radio_transmitter/Makefile new file mode 100644 index 00000000..75420a10 --- /dev/null +++ b/test/monniaux/heptagon_radio_transmitter/Makefile @@ -0,0 +1,3 @@ +TARGET=radiotrans + +include ../rules.mk diff --git a/test/monniaux/heptagon_radio_transmitter/make.proto b/test/monniaux/heptagon_radio_transmitter/make.proto deleted file mode 100644 index 40de14dc..00000000 --- a/test/monniaux/heptagon_radio_transmitter/make.proto +++ /dev/null @@ -1,3 +0,0 @@ -sources: "$(wildcard *.c)" -target: radiotrans -measures: [cycles] -- cgit