wrapper/tests/parity/README

   1 Modified : Jan  9 1995
   2 Modified : Jul  1 1997
   3
   4
   5 A verification program illustrating the use of arrays and recursive nodes.
   6 The goal is to compare a combinatorial operator "P", computing the parity bit
   7 of a bit-string, to a sequential version "parity".
   8
   9 The size of the bit-string is a constant of the program, here 8.
  10
  11 The node XOR implements exclusive "or"
  12
  13 The combinatorial parity-bit operator is recursive
  14 - applied to a bit-string of size 1, it returns the value of its unique bit.
  15 - applied to a bit-string of longer size n, it returns the exclusive "or" of
  16   the last bit of the string and the result of P applied to the n-1 first bits.
  17
  18 The sequential parity-bit operator proceeds by shifting its parameter b. At
  19 any cycle
  20   - the parity-bit is the exclusive "or" of its preceding value and the
  21     leftmost bit of b.
  22   - the array b is shifted to the left (and completed by "false" on the right)
  23
  24 In order to know when the whole array has been processed, an auxiliary array
  25 "todo" is used. All its elements but the rightmost are initialized to false.
  26 It is shifted to the left at any cycle, until its only "true" element becomes
  27 the leftmost. Then the variable "done" becomes true, and the parity-bit has
  28 been computed.
  29
  30 The verification program compares the result of the combinatorial operator
  31 with the one of the sequential operator, when the computation of the last
  32 one is terminated.
  33
  34 The Makefile gives 3 ways for verification :
  35         GenThenMin => generate full automaton then minimize
  36         GenMin => generate minimal automaton
  37         Verif => use the verification tool