// ABRO - the "hello world" for SSMs
// Example from Charles André, Semantics of SyncCharts,
// ISRN I3S/RR-2003-24-FR, April 2003, Figure 5-12
//
// rvh, 17 mar 2009

#define _SC_SSA

#include "scl.h"

// ======================================
// Program-specific definitions

// Signals
typedef enum {_A, _B, _O1, _O2} signaltype;
int A, B, O1, O2;
const char *s2signame[] = {"A", "B", "O1", "O2"};

#define _SC_ID_MAX  6           // Highest thread id in use
#define _SC_SIG_MAX 4           // Highest signal id in use

#define RUNMAX  2               // # of runs to execute
#define TICKMAX 3               // # of ticks to execute

#include "sc.h"

// PRE() for now is just a hint for analysis/scheduling.
// Two variants for handling this:
// 1) schedule x = PRE(y) before any definition of y.
//    This requires that y must be pre-initialized.
// 2) schedule x = PRE(y) after any use of x.
//    This requires that x must be pre-initialized.
// We here chose 2), as it separates handling of registers from 
// the other combinational control logic, and seems slightly more efficient
#define PRE(x)  x


// Inputs for RUNMAX runs of TICKMAX ticks
sigset inputs[RUNMAX][TICKMAX] =
  {{u2b(_A), 0, u2b(_B)},
   {0, u2b(_A), 0}};
//{{0, 0, 0,}, {0, 0, 0,}};

// Expected outputs
sigset outputs[RUNMAX][TICKMAX] =
  {{u2b(_A)|u2b(_B)|u2b(_O1), u2b(_O1), u2b(_B)|u2b(_O2)},
   {0, u2b(_A)|u2b(_B)|u2b(_O2), u2b(_O2)}};
//{{0, 0, 0,}, {0, 0, 0,}};

// May want to exclude non-tick functions, to measure object code size for tick function
#ifndef _SC_ONLY_TICK_FUNCTION
void getInputs(int runCnt, int tickCnt)
{
  signals = inputs[runCnt][tickCnt];

  // Variables are persistent - therefore must initialize them
  // at every run
  if (tickCnt==0) {
    O1 = false;
    O2 = false;
  }
}

// Set reference outputs and check valued signals, if there are any.
// Return 1 unless valued signal outputs are wrong.
// No valued signals here, therefore always return 1.
int checkOutputs(int runCnt, int tickCnt, _setPartType *tickOutputs)
{
  *tickOutputs = outputs[runCnt][tickCnt];
  return 1;
}

// No valued signals to print
void printVal(int id)
{
}

// The following functions serve to make input/output signal traces
// available for variables

// Copy input signals to variables
void signals2vars() {
  A = _sigContains(signals,_A);
  B = _sigContains(signals,_B);
}

// Copy output variables to signals
void vars2signals() {
  if (A) EMIT(_A);
  if (B) EMIT(_B);
  if (O1) EMIT(_O1);
  if (O2) EMIT(_O2);
}
#endif

#define UNDEFINED -1

// Tick function
/* SSA-version inspired by Esterel's circuit semantics [1]
 *
 * [1] Gerard Berry, "The Constructive Semantics of Pure Esterel, Draft Version 3," July 1999
 * http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.46.2076&rep=rep1&type=pdf
 *
 * The following is written in a variant of SSA (Static Single
 * Assignment).
 *
 * 1) Variables that are written to multiple times, possibly including
 * input assignments, are split up into distinct copies for each
 * write.
 *
 * 2) Writes are "merged", depending on their sequential order of
 * execution.
 *
 * Notes: (i) This merging must only be done for variables that can be
 * written to in the same tick. At least for an initial
 * implementation, we may conservatively assume that all writes can
 * occur in the same tick. (ii) Sequential constructiveness requires
 * that concurrent writes must be confluent (otherwise the program
 * would have to be rejected). Thus we merge concurrent writes in
 * arbitrary sequential order. (iii) As a result, we have a total
 * order for all writes that can be executed in the same tick.
 *
 * 3) To determine which writes are "active", ie, whether control
 * reaches them in the current tick, each basic block is augmented
 * with an "activation flag" that is set to true when the basic block
 * is executed. This roughly corresponds to the guards in guarded
 * command (see eg. Schneider et al.).
 *
 * 4) Reads must pick the one "right" merged write.
 * Sketch for an approach: consider all potentially relevant writes
 * that may take place in the same tick (using write-read
 * dependencies), pick from those writes the "latest merge", according
 * to aforementioned total ordering of the writes. If there can be no
 * concurrent write, then use pre-Value.
 * 
 * For HW synthesis, the code can be translated directly to a net
 * list. Only registers need special treatment.
 *
 * For SW synthesis, one might have to reorder assignments such that
 * writes occur before reads. In this example, this is not necessary,
 * as the only concurrent write-read dependence, on B, orders a
 * statement of the first thread before another statement of the
 * second thread, which already corresponds to the ordering of the
 * code.
 *
 * Both HW and SW synthesis might reject programs, when they do not
 * permit a static schedule. For example, with this approach, HW
 * synthesis does not permit "instantenous loops", which can be
 * handled naturally in SW; conversely, SW synthesis might reject some
 * programs that still result in deterministic circuits, such as the
 * Token Ring Arbiter. However, the intersection of the SW- or
 * HW-synthesizable subsets should still be quite large. Eg, it
 * encompasses all of what was acceptable for Esterel, plus many more
 * programs that can be handled by permitting sequential
 * assignments. This includes the following example, which can be
 * synthesized into both HW and SW, but would be rejected by Esterel
 * Studio or SCADE.
 */
int tick()
{
  // Guards for basic blocks
  //
  // Note that these might be computed even more efficiently using a
  // Program Dependence Graph (PDG), which could expose further parallelism.
  // However, we for now make do with a simpler, locally computed scheme.
  bool _g0,  //_entry,
    _g1,     //_go0_HandleA,
    _g2,     //_surf_HandleA_WaitA,
    _g4,     //_exit_HandleA,
    _g5,     //_surf_HandleB_WaitB,
    _g7,     //_exit_HandleB,
    _g8;     //_exit;

  // Registered guards, for basic blocks that end in pause statements
  // "true" indicates an active pause statement; initially pause statements are inactive
  static bool _g3,  //_depth_HandleA_WaitA,
    _g6;            //_depth_HandleB_WaitB;

  // Flags indicating that a region is empty (inactive),
  // ie, neither just started nor any active pause
  bool _e0,  //_empty_HandleA,
    _e1;     //_empty_HandleB;

  // Values; multiple instances of O1, O2, and (input) B
  // On Naming:
  // Use suffix derived from guards of the enclosing basic block.
  // If there are multiple assignments to the same variable within on basic block, 
  // use increasing counter, starting at 0, for the assignments - except for the last
  // assignment, as that is the one visible outside of the basic block.
  // The assignments with a counter suffix are only visible within the basic block.
  // Eg, assume we are in basic block "entry":
  //   X = 0; Y = X; X = 1
  // becomes
  //   X_entry0 = 0; Y_entry = X_entry0; X_entry = 1
  //bool O1_g0, O1_g4, O1_g7, O1_g8, O2_g0, O2_g8, B_g4;

  // Registered values of non-input variables
  // For SW, one would not need to make these explicit, one might instead just use O1 and O2
  // Note: O1 and O2 are declared globally, to make them visible outside of tick function
  //static bool _preO1, _preO2;

  // RESET() initializes _notInitial = 0;
  _g0 = !_notInitial;   // _g0 indicates initial tick

  // "Pre-initialize" registers in initial tick
  if (_g0) {
    _g3 = false;
    _g6 = false;
    //_preO1 = UNDEFINED;
    //_preO2 = UNDEFINED;
  }

  _signals2vars

  //if (!_notInitial)
  //  _notInitial = _notInitialDetect;
  //Replaced with code that avoids jump:
  _notInitial |= _notInitialDetect;

  if (_g0) {
    O1 = false;

    // Observations:
    // 1) The above assignment is only effective when _g0 holds
    // 2) If the assignment is effective, it overrides _preO1
    // Thus, we perform a "sequential merge" below.
    // This is somewhat similar to a phi node, except that the merged assignments
    // do not have to come from separate control paths.
    //_mergeFalse(O1_g0, _g0, _preO1);

    O2 = false;
    //_mergeFalse(O2_g0, _g0, _preO2);
  }

  //fork1(HandleB, 1) {
  //HandleA:

  // Merge paths before reaching conditional
  _g1 = _g0 | _g3;

  //  if (!A) {

  //  pause;  // WaitA
  // Replace this pause with a register "_g2" that indicates an active pause
  _g2 = _g1 & !A;  // _g3 is registered value

  //  goto HandleA;
  //}

  _g4 = _g1 & A;

  if (_g4) {
    // The input B constitutes a "0th" copy of B that is always present
    // Therefore, must create copy for following write to B
    B = true;
    // Possible optimization for SW: replace assignment to B_g4 by assignment
    // to just B, as it is the final value of B
    //_mergeTrue(B_g4, _g4, B);

    O1 = true;
    //_mergeTrue(O1_g4, _g4, O1_g0);
  }

  // Compute "output pins" of thread HandleA
  // This is analogous to the LEM/REM pins [1, Fig. 11.1]
  // Note: as "starting guard" we here use _g1, which guards the first block of the thread,
  // instead of _g0, which guards the fork node. This sometimes allows slight optimizations,
  // as for _e1
  _e0 = !(_g1 | _g2);   // Dead thread - neither just started nor any active register

  //} par {
  //  HandleB:
  //  pause;

  // Observation, regarding the read of B:
  // Possible writes to B are the input (called just "B") and B_g4.
  // As B_g4 is a "sequential successor" of B, the "merge" of these two is
  // already computed in B_g4
  _g5 = _g0 | (_g6 & !B);  // Set register _g5

  //  if (!B) {
  //    goto HandleB;
  //  }
  _g7 = _g6 & B;

  if (_g7) {
    O1 = true;

    // Observation:
    // The assignments to O1 that correspond to O1_g4 and O1_g7
    // are concurrent, i.e., not sequential, but confluent.
    // Thus we (arbitrarily) merge them by first computing O1_g4, and then
    // possibly overwriting this with "true" in the assignment to
    // O1_g7.
    // We could also have reversed this order.
    //_mergeTrue(O1_g7, _g7, O1_g4);
  }

  // Compute "output pins" of thread HandleB
  // Note: as "starting guard" we here use _g5, which guards the first block of the thread,
  // instead of _g0, which guards the fork node. For _e1, this reduces the operation/gate count, 
  // since _g5 also happens to guard the one surface node of the thread, thus the resulting
  // guard is !(_g5 | _g5), which reduces to just !_g5
  // Otherwise we would have to compute !(_g0 | _g5) instead of just !_g5
  _e1 = !_g5;

  //} join1(2);
  // This corresponds to output K0 of Sychronizer circuit [1, Fig. 11.10]
  // If this were not the basic block corresponding to the top-level exit node,
  // we would have called this "_join_WaitAB"
  _g8 = (_g4 | _g7)  // At least one thread must have just terminated
    & (_g4 | _e0)   // HandleA has terminated or was already dead
    & (_g7 | _e1);  // HandleB has terminated or was already dead

  if (_g8) {
    O1 = false;
    // O1_g8 is sequentially after O1_g4 and O1_g7.
    // As stated above, O1_g4 and O1_g7 are concurrent, but are merged in
    // O1_g7. Thus we here merge with O1_g7.
    //_mergeFalse(O1_g8, _g8, O1_g7);

    O2 = true;
    //_mergeTrue(O2_g8, _g8, O2_g0);
  }

  // Compute output values.
  // This is where the nature of sequentiality becomes apparent:
  // we always use the "last" write to a variable.
  // For HW synthesis, would have to replace these by A_out, B_out, O1_out, O2_out
  //A = A;       // Input A is not overwritten
  //B = B_g4;
  //O1 = O1_g8;
  //O2 = O2_g8;

  _vars2signals;

  // THE FOLLOWING CODE FOR SW SYNTHESIS ONLY:

  // Emulate registers by copying them for next tick
  _g3 = PRE(_g2);
  _g6 = PRE(_g5);
  //_preO1 = O1;
  //_preO2 = O2;

  return !_g8;  // Return true iff automaton continues running
}

// Local Variables:
// compile-command: "make ABRO; ABRO"
// End:
