Guarded Actions Meta-Model


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:

  1. < 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) >
  2. < 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
  3. < 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.

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

  1. continuous assignments
  2. clocks and processes
  3. delays

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

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

is translated into the GA

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

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:

always @(x or y)
begin            // is equivalent to
    z <= x & y;  // assign z = x & y

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.


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


For guarded actions Guarded actions extraction method was implemented.
For clocks Clock extraction method was implemented.


  1. Integrating System Descriptions by Clocked Guarded Actions. J. Brandt, M. Gemünde, K. Schneider, S. Shukla, and J.-P. Talpin. Forum on Design Languages (FDL'11), 2011.
  2. Separate Translation of Synchronous Programs to Guarded Actions. J. Brand and K. Schneider. Internal Report 382/11, University of Kaiserslautern, 2011.

Updated by Alexander Kamkin almost 7 years ago · 1 revisions