Retrascope

h1. Guarded Actions Meta-Model

h2. Introduction

_Guarded actions_ (_GAs_) are widely used for the description of concurrent systems [1]. GA is a pair < _guard_ => _body_ >, where _guard_ is a Boolean condition and _body_ is a set of actions (assignments) over a set of variables. A body is executed if its guard is met in the current state. Usually, GAs are seen as an asynchronous model. In the current state, the guards of all actions are checked and any subset of the activated actions is selected for the execution (inside the body all the actions are executed in parallel). However, GAs have also been successfully used in the synchronous domain (in this case, they are usually referred to as _synchronous guarded actions_, _SGAs_). The synchronous model of computation does not only fire all activated actions, but the execution of the actions happens simultaneously with the evaluation of the guards so that there may be inter-dependencies among guards and actions (in practice, it means the execution to follow the data dependencies) [1].

The generalization of both kinds is called _clocked guarded actions_ (_CGAs_) [1]. Actions are defined over a set of explicitly declared clocks _Clk_ (one-bit signals indicating instants). The data flow is based on a set of explicitly declared variables _Var_. Each variable _var_ is related to a clock _clk_ (_clk_(_var_) denotes the clock of the variable _var_). CGAs have one of the following forms:

# < _guard_ => _var_ = _expr_ > (_immediate assignment_):

the value of the variable _var_ is changed in the given instant to the value of the expression _expr_; implicitly implies < _guard_ => _clk_(_var_) >

# < _guard_ => *next*(_var_) = _expr_ > (_delayed assignment_):

the value of the expresstion _expr_ is evaluated in the given instant, but the value of the variable _var_ is changed in the next _clk_(_var_) tick

# < _guard_ => *assume*(_cond_) > (_assumption_):

the Boolean condition _cond_ has to hold at the given instant

The CGAs representation is rather general and can be used for integrating system descriptions of different kinds [1,2]. On the other hand, this form is convenient for system analysis, synthesis and transformation.

To represent CGAs, [[AIF format]] can be used.

h2. HDL-to-CGAs Extraction

The motivation for the HDL-to-CGAs extraction is the above mentioned ability of CGAs to serve as a basis for effective analysis of systems, in particular hardware designs. Translating HDL to CGAs is not straightforward and requires additional assumptions on the source code (for example, a translator needs to know which signals encode clocks). Fortunately, typical designs usually meet the assumptions. Let us consider how some HDL-specific constructs are processed, including

# continuous assignments

# clocks and processes

# delays

...

h3. Continuous Assignments

Continuous assignment is the most usable construct in datapath modeling. Continuous assignments are special kind of processes that are always active and drive values into the left-hand-side nets whenever the right-hand-side value changes. The rule for translating such assignments into CGAs is obvious. A statement

<pre>

assign y = f(x1, ..., xn);

</pre>

is translated into the GA

<pre>

true => y = f(x1, ..., xn);

</pre>

h3. Clocks and Processes

In HDL, clocks are coded as events that activate processes (always blocks in Verilog). However, not all of the process activators are clocks. There are other types of activators (e.g. resets) that should be distinguished from clocks. For example, if output values are defined for all the values of the sensitive list inputs, the process defines combinational logic and can be expressed as a continuous assignment:

<pre>

always @(x or y)

begin            // is equivalent to

    z <= x & y;  // assign z = x & y

end

</pre>

which means that _x_ and _y_ are not clocks. Moreover, if some variable is used in an expression, it is unlikely to be a clock (exceptions are possible).

If clocks are extracted, there might be a problem in determining which one relates to a particular variable of the design (as it is required in the CGAs meta-model). Typical HDLs (Verilog and VHDL) do not specify clocks explicitly. Thus, one variable might turn out to be synchronized with multiple clock signals. To overcome the problem, we endow the set of clocks with algebraic (namely, monoid) structure (clock is a set of basic clocks; union of two clocks produces another clock). _clk_(_var_) is the union of all clocks synchronizing usage and definition of the variable _var_.

h3. Delays

As in synthesis, delays are ignored (they are replaced to delta-delays).

h2. Practice

For guarded actions [[Guarded actions extraction method]] was implemented.

For clocks [[Clock extraction method]] was implemented.

h2. References

# "Integrating System Descriptions by Clocked Guarded Actions":http://www.irisa.fr/prive/talpin/papers/fdl11.pdf. J. Brandt, M. Gemünde, K. Schneider, S. Shukla, and J.-P. Talpin. _Forum on Design Languages (FDL''11)_, 2011.

# "Separate Translation of Synchronous Programs to Guarded Actions":http://es.cs.uni-kl.de/publications/datarsg/BrSc11a.pdf. J. Brand and K. Schneider. _Internal Report 382/11, University of Kaiserslautern_, 2011.