Refinement maps as types

You may have observed that it is getting a bit tedious to refinement maps for each stage of the implementation, when they are actually all the same. SMV provides a way to avoid this by specifying abstract definitions of a signal as part of its data type. We can also give a type a parameter, so that we can specify in the type declaration which abstract object an implementation object corresponds to. A parameterized type in SMV is otherwise known as a module. Let's declare a type with a refinement map as follows:

  module byte_intf(bytes){

    bytes : array INDEX of BYTE;

    valid : boolean;
    idx : INDEX;
    data : BYTE;

    layer spec:
      if(valid) data := bytes[idx];
}

This defines an interface type that transfers an array bytes of bytes according to a specific protocol. This protocol is defined by layer spec. Now, lets rewrite our example using this type:

module main(){

  /* the abstract model */
        
  bytes : array INDEX of BYTE;
  next(bytes) := bytes;  

  /* the input and output signals */

  inp, out : byte_intf(bytes);

  /* the implementation */

  stage1, stage2 : byte_intf(bytes);

  init(stage1.valid) := 0;
  next(stage1) := inp;
  init(stage2.valid) := 0;
  next(stage2) := stage1;
  init(out.valid) := 0;
  next(out) := stage2;

  /* abstraction choices */

  using stage2.valid//free, stage2.idx//free prove out.data//spec;
  using stage1.valid//free, stage1.idx//free prove stage2.data//spec;
}

Notice that there's no need to write the intermediate refinement maps. They are part of the data type.