-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathREADME.CMurphi.3.1
91 lines (59 loc) · 3.17 KB
/
README.CMurphi.3.1
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
===========================================================================
Cached Murphi Release 3.1
Finite-state Concurrent System Verifier with State Space Caching.
Responsible for this release: Giuseppe Della Penna ([email protected])
Enrico Tronci ([email protected])
===========================================================================
This release is based on the original Murphi Release 3.1 and has been
modified to implement state space caching. Responsible for the
original Murphi Release 3.1 is Ulrich Stern ([email protected]).
For more information about this release and the state space caching,
see the paper
E. Tronci, G. Della Penna, B. Intrigila, M. Venturini Zilli,
"Exploiting Transition Locality in Automatic Verification",
Proceedings of: 11th Advanced Research Working Conference on
Correct Hardware Design and Verification Methods (CHARME),
4-7 September 2001, Livingston-Edinburgh (Scotland), LNCS, Springer-Verlag
Co-sponsored by the IFIP TC10/WG10.5 Working Group on:
Design and Engineering of Electronic Systems
Postscript version of the above paper is in directory doc,
file charme01.ps.
1. Modifications to the distribution files
Directories bin, ex, doc are the same as in Murphi 3.1.
Directories src, include have been modified w.r.t. Murphi 3.1.
See the README.cmurphi files in each of these directories for
more information.
2. Modifications to the Murphi Compiler
The following option has been added to the mu compiler:
--cache enables the state caching
When this option is specified, state space caching is enabled
in the generated verifiers. If the option is not specified,
the compiler generates the same verifiers as Murphi 3.1
3. Modifications to the Murphi Verifier
The following options have been added to the verifier:
-maxc<n> highest admitted collision rate. Zero for no limit.
(percent value, default 90).
This option tells the verifier to stop when the collision rate
in the state cache it too high. The collision rate is the ratio
states_overwritten(collisions) / states_written in the state
cache. When this rate is too high, the cache is forgetting too
many visited states and the state exploration may loop indefinitely.
The default value for this option, 90, tells the verifier to stop
when the 90% of the visited states overwrite an already visited state
in the state cache.
-maxl<n> maximum reachable bfs level. Zero for no limit.
(default is no limit).
This option tells the verifier to stop when it begins the
exploration of a particular level in the BFS tree.
This may help to stop explorations that are looping when
height of the search tree is known or can be estimated.
The following options have been disabled:
-s
-vdfs
The Cached Murphi state space caching algorithm works only
with Breadth First Search, so the DFS and simulation options
are disabled.
3. Compiling the Cached Murphi Compiler and Verifier
To compile the Cached Murphi Compiler, follow the instructions
in the Readme file in src directory.
===========================================================================