The effect of decomposition

To see the effect of using refinement maps let's make two versions of our simple example, one with and one without intermediate refinement maps. We can easily do this by changing the types of the intermediate stages. To make it interesting, we'll use 32 delay stages. Here is the version with intermediate refinement maps:

  /* the implementation */

  stages : array 1..31 of byte_intf(bytes);


  init(stages[1].valid) := 0;
  next(stages[1]) := inp;

  for(i = 2; i <= 31; i = i + 1){
    init(stages[i].valid) := 0;
    next(stages[i]) := stages[i-1];
  }

  init(out.valid) := 0;
  next(out) := stages[31];

  /* abstraction choices */


  for(i = 2; i <= 31; i = i + 1)
    using stages[i-1].valid//free, stages[i-1].idx//free
    prove stages[i].data//spec;

  using stages[31].valid//free, stages[31].idx//free prove out.data//spec;

Here is the version without intermediate refinement maps:

  /* the implementation */

  stages : array 1..31 of
    struct{
      valid : boolean;
      idx : INDEX;
      data : BYTE;
    }

  init(stages[1].valid) := 0;
  next(stages[1]) := inp;

  for(i = 2; i <= 31; i = i + 1){
    init(stages[i].valid) := 0;
    next(stages[i]) := stages[i-1];
  }

  init(out.valid) := 0;
  next(out) := stages[31];

Note, we don't want to free any of the intermediate signals in this version. Now, open the first version, and select ``Props|Verify all''. It should verify all 256 properties in something like 15 seconds (depending on your machine). Now, open the second version (without refinement maps). There are only 8 properties to verify in this case (one for each output bit), bit SMV cannot verify these properties, as you may observe by select ``Prop|Verify all''. When you get bored of watching SMV do nothing, select ``Prop|Kill Verification'' (note, this may not work under Windows), and click the Cone tab. Observe that the cone contains 256 state variables, which is usually to large for SMV to handle (though occasionally SMV will solve a problem of this size, if the structure of the problem is appropriate for BDD's). Note that it is possible to construct even a fairly trivial example which cannot be verified directly by model checking, but can be verified by decomposition and model checking. Generally, when a direct model checking approach fails, it's best to look for a decomposition of the problem using refinement maps, rather than to try to determine why the BDD's exploded.