The refine sublanguage

The refine sub-language takes the form

refine {
    /* any standard ACT body element can appear here */
}

This is used to provide an implementation of a process that replaces the CHP, dataflow, HSE, or PRS body. For example, imagine you had a process defined at the CHP level

defproc example (...)
{
   int x;
   chp {
      *[ L?x; R!x ]
   }
}

You can include its production-rule level description in the same process definition, as follows:

defproc example (...)
{
   ...
   chp {
      *[ L?x; R!x ]
   }
   prs {
      // circuit goes here
   }
 }    

At this point, a tool can select the level of abstraction/detail for the process by picking one of the two sub-languages provided.

Now imagine that instead of writing the production rules directly, you'd like to instantiate a set of gates to implement the circuit. Suppose we write the following:

defproc example(...)
{
  ...
  chp {
    *[ L?x; R!x ]
  }
  inst1 i1;
  inst2 i2;
  // the other instances and connctions...
}

As written, this means that the process has a CHP definition, and in addition it has the specified instances! This is not what we intended to specify; we'd like to use the CHP definition or the instances.

To provide support for this, the refine body is used. The example would be written:

defproc example(...)
{
  ...
  chp {
    *[ L?x; R!x ]
  }
  refine {
     inst1 i1;
     inst2 i2;
     // the other instances and connctions...
   }
}

Now you can pick the refined version of the process by using the ACT command-line option -ref=1, and so a tool can pick either the chp or the refine sub-language, giving us the desired effect.

This approach is used in the chp2prs tool to provide an implementation of the CHP. This is the standard convention used in any tool that takes CHP and generates a circuit-level description. By augmenting the definition of the process in this manner, you can model the process at both the CHP level of abstraction as well as a more detailed representation containing a collection of instances that implement the CHP.

Since refine { … } blocks contain normal ACT statements, they can also include refine blocks within them. Hence, you can say:

refine {
    inst i1;
    chp { ... }
    refine { inst i2; }
}

When ACT selects the outer refinement block for the process, it decrements the refinement level before proceeding; the level is restored at the end of the refinement block. Hence, if -ref=1 were specified, then the block:

  inst i1;
  chp { ... }
  refine { inst i2; }

would be processed with the refinement level set to zero; hence, the chp { … } body would be selected, and not the nested refinement. To replace the CHP with the nested refinement block, use -ref=2. Note that in both cases the instance i1 would be processed.

While the nested refinement approach works nicely when designs are recursively refined, it may not be suitable for transformations where an existing refinement block needs to be completely replaced. ACT has a mechanism to support this in the following manner:

refine { 
    inst i1; 
    chp { ... }
}    
refine<2> {
    inst j1;
    prs { ... }
}

In this case, “-ref=2” will replace the first refine block with the second. In other words, instance i1 will not be created, and -ref=2 will select instance j2 and the prs { … } body.

In general, a refine block has an associated integer refinement level (the default is one). When ACT processes a block with refinement level r, it searches for the largest refinement block with level that is at most r. (Note: this may be no block, in which case the block is processed as normal.) If a refine block with level l is found, then it processes all non-language constructs within the block and then expands the refinement block with level l by decrementing the current refinement level by l.