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 |
---|