Using pure structures

A pure structure is a user-defined data type that contains only int/bool or other pure structures. An example of a pure structure is:

deftype cache_entry (bool valid; int<32> data; int<24> tag) { }

An example CHP program that uses this as the data type is:

defproc cache(chan?(int<32>) A; chan?(bool) RD; chan!(int<32>) DI; chan!(int<32>) DO)
{
   cache_entry C[256];
   int<32> addr;
   bool cmd;
   cache_entry ce;
 
   chp {
     *[ A?addr,RD?cmd;
        [cmd -> // read command
              ce := C[addr{7..0}];
             [ ce.valid & ce.tag = addr{31..8} -> log ("cache hit!"); DO!ce.data
             [] else -> log ("cache miss!"); DO!0
             ]
     []~cmd -> // write command
             ce.valid+;
             DI?ce.data;
             ce.tag := addr{31..8};
             C[addr{7..0}] := ce
      ]
   ]
  }                  
}

(Note: this is not meant to be a working cache!)

We can abstract away the matching function as follows:

deftype cache_entry (bool valid; int<32> data; int<24> tag) 
{ 
    methods {
        function match (int<32> addr) : bool
        {
           chp {
              self := valid & tag = addr{31..8}
           }
         }
    }
}
 
 
defproc cache(chan?(int<32>) A; chan?(bool) RD; chan!(int<32>) DI; chan!(int<32>) DO)
{
   cache_entry C[256];
   int<32> addr;
   bool cmd;
   cache_entry ce;
 
   chp {
     *[ A?addr,RD?cmd;
        [cmd -> // read command
              ce := C[addr{7..0}];
             [ ce.match(addr) -> log ("cache hit!"); DO!ce.data
             [] else -> log ("cache miss!"); DO!0
             ]
     []~cmd -> // write command
             ce.valid+;
             DI?ce.data;
             ce.tag := addr{31..8};
             C[addr{7..0}] := ce
      ]
   ]
  }                  
}