source: Deliverables/D5.1/cost-plug-in/wrapper/tests/parity/README @ 1462

Last change on this file since 1462 was 1462, checked in by ayache, 8 years ago

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File size: 1.5 KB
1Modified : Jan  9 1995
2Modified : Jul  1 1997
5A verification program illustrating the use of arrays and recursive nodes.
6The goal is to compare a combinatorial operator "P", computing the parity bit
7of a bit-string, to a sequential version "parity".
9The size of the bit-string is a constant of the program, here 8.
11The node XOR implements exclusive "or"
13The 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.
18The sequential parity-bit operator proceeds by shifting its parameter b. At
19any 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)
24In 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.
26It is shifted to the left at any cycle, until its only "true" element becomes
27the leftmost. Then the variable "done" becomes true, and the parity-bit has
28been computed.
30The verification program compares the result of the combinatorial operator
31with the one of the sequential operator, when the computation of the last
32one is terminated.
34The Makefile gives 3 ways for verification :
35        GenThenMin => generate full automaton then minimize
36        GenMin => generate minimal automaton
37        Verif => use the verification tool
Note: See TracBrowser for help on using the repository browser.