diana - a delay insensitive circuit analysis tool

This file documents diana version 0.4.0, which is a delay insensitive circuit analysis tool

1. Description

diana is intended to be used by circuit designers as a tool for modeling and verification of delay insensitive circuits (i.e., the most robust class of clockless digital circuits, for which traditional methods of logic design are largely useless and good CAD support is scarce). Taking Petri nets or circuit descriptions as input, diana can compute the answers to questions like

• Can a given circuit ever deadlock?
• Are there any possible glitches or hazards?
• Does a circuit meet its specification?
• Does it exceed the specification?
• Are two circuits equivalent?
• What can one do that the other can't?
• What happens if we assume no contention?
• What if the environment is limited in some other way?
• What does the state graph look like?
• What would a Petri net model look like?

In cases where the answers to these questions require an explanation, diana can construct a graphical representation explaining it, such as one that depicts the set of all sequences of events leading up to a deadlock, or it can output a listing of such events to a text file.

Impatient readers can probably learn enough to get started by skipping to 8. Examples.

2. Options

diana accepts the following parameters, all of which may be recognizably truncated:

--help

Show a short summary of diana's usage and options.

--version

Show the version number and the time stamp of the diana source file.

--warranty

Show a short copyleft message and a reminder about the lack of a warranty.

--optimize

Apply obvious local optimizations to input files in Petri net format prior to any other analysis.

--list

Output a text file with a .lis suffix describing each requested Petri net --plot, and also one for each input file in DI netlist format showing the netlist after macro expansion.

--traces

Output a text file with a .trc suffix listing a small arbitrarily chosen sample of accepted traces for each requested trace oriented --plot (see 4.3 Trace Oriented Plot Types).

--core-dump

Output all relevant run-time data structures in an encoded binary format to files with .cor suffixes in addition to normal output (for hackers only).

--k-hot-code [number]

Use the given number in conjunction with the k-hot-petrinet plot type (see 4.1 Petri Net Plot Types).

--open-specification

Use the environment to restrict only the implementation, not the specification (see 3. Files).

--plots [plot-type,[plot-type]]

Generate one or more graphical representations based on the input files (see 4. Plot Types).

--style [style-type,[style-type]]

Adjust the --plot rendering style according to the given preferences (see 5. Style Types).

--tests [test-type,[test-type]]

Check one or more behavioral properties based on the input files (see 6. Test Types).

--dimensions ["any text"]

Analyze a specification constructed on the fly by applying an avram virtual machine code file to the given text (for hackers only).

3. Files

Up to three file parameters may be passed to diana on the command line.

spec-file

This file contains a circuit specification either in Petri net format (see 3.1 Petri net File Format)) or as a DI netlist (see 3.2 DI Netlist File Format), or else contains the virtual code to generate one for the given --dimensions.

implementation-file

If the first file contains a circuit specification, this one contains a proposed way of implementing it, and is required by those --tests and --plots that are applicable to pairs of systems. The systems described in these two files must have exactly the same sets of input and output signals. The implementation-file may be expressed as either a Petri net or a DI netlist (and in either case by text or virtual code).

environment-file

If this file is given, it must have input and output signals that are complementary to the others, and will express assumptions about the environment in terms of a Petri net or DI circuit model itself. Virtual code may be used here as well. If the --open-specification option is given, the environment applies only to the implementation-file, but otherwise applies to both.

Note that if only two files are given, then the second is interpreted either as an implementation or an environment based on whether its input and output signals are equal or complementary to those of the first.

In addition to these input files, diana requires the virtual machine emulator avram in order to run (even if the input files don't contain virtual code). The avram executable must be found somewhere in your default search path, which can be verified by typing avram --version at your shell prompt. See http://www.lsbu.ac.uk/~fureyd/avram for notes on downloading and installing it.

Output files depend on the particular options selected, as documented below. With most options, an additional file called profile.txt is written to the current working directory, which contains a table of the percentages of time spent on each phase of the analysis in relative time units.

3.1 Petri net File Format

Files in Petri net format have five sections, each beginning with one of the words .inputs, .outputs, .dummy, .graph, or .marking at the beginning of a line, with sections in the order indicated. The word .end may optionally appear after the last section.

Each section contains a sequence of identifiers (consisting of case sensitive letters or digits) separated by spaces or line breaks, except the .marking section, for which the identifiers are separated by spaces and also enclosed collectively in braces. Furthermore, some line breaks in the .graph section are compulsory, as implied below. The identifiers in each section have the following interpretations.

.inputs

These are the input signals to the circuit, which are identified with transitions in the Petri net.

.outputs

These are the output signals from the circuit, which are also identified with transitions in the Petri net.

.dummy

These are all remaining transitions in the Petri net.

.graph

This section expresses the adjacency relation of the Petri net. Each line begins with the identifier of a place or transition, which is followed by the identifiers of its postset members on the remainder of the line.

.marking

This section indicates the set of initially marked places.

For example,

       .inputs r0 r1
       .outputs g0 g1
       .dummy n o p q
       .graph
       g0
       g1
       r0 j
       r1 k
       h g0
       i g1
       j p o
       k q n
       l p o n
       m q o n
       n r m i
       o r l h
       p m l h
       q m l i
       r q p
       .marking {l m}
       .end

This format is fully compatible with syndi and is syntactically but not always semantically compatible with petrify. Similarly to petrify, diana infers a place between two connected transitions, but otherwise requires a proper Petri net rather than an STG (unlike petrify). Hence, there may be only one of each transition, and signed transitions such as s+ and s- are not supported.

Furthermore, unlike petrify, diana accepts input transitions with empty presets and output transitions with empty postsets, and in fact requires them in environment-file parameters and their associated systems when Petri net format is used. Open Petri nets such as these may have empty initial markings, which petrify does not allow.

3.2 DI Netlist File Format

The alternative to Petri net format when specifying a circuit is to use a netlist of Delay Insensitive primitive circuit components.

In this format, the components are not numbered, but the interconnecting nodes are. There is one line in the file for each component in the circuit. The line contains the input node numbers followed by the component mnemonic followed by the output node numbers, all separated by spaces. Tab characters are treated as spaces.

Anything following a hash symbol on a line is treated as a comment. Empty lines, blank lines, and lines containing only comments are ignored.

An input signal is expressed on a line containing the signal name followed by the node number, separated by a space. Output signals are expressed similarly but with the node number preceding.

For example,

       a 0         # this input is connected to the fork
       1 c           # this output comes from a celement
       2 b               # this comes from the other one
       0 fork 4 3               # this leads to the xors
       16 toggle 13 17                            # etc.
       9 17 celement 1
       11 5 diverter 20 19
       20 toggle 14 18
       18 19 diverter 21 16
       21 toggle 15 10
       3 12 xor 22
       15 22 xor 7
       24 toggle 11 25
       10 25 celement 2
       13 6 diverter 28 27
       28 toggle 12 26
       26 27 diverter 29 24
       29 toggle 23 9
       14 4 xor 30
       23 30 xor 8
       7 8 mutex 5 6

The eight available DI primitives work as follows, where the node numbers below have been chosen arbitrarily.

1 wire 2

acknowledges an input on node 1 with an output on node 2 (superfluous in most circuits)

1 iwire 2

sends an output on node 2 first, then waits for an input from node 1, then sends another output, and so on

1 fork 2 3

waits for an input on node 1, then concurrently sends outputs on nodes 2 and 3

1 toggle 2 3

acknowledges consecutive inputs on node 1 with outputs alternating between nodes 2 and 3, starting with 2

1 2 celement 3

acknowledges a pair of concurrent inputs on nodes 1 and 2 with an output on node 3

1 2 xor 3

acknowledges an input on either of node 1 or node 2 (but not both) with an output on node 3

1 2 diverter 3 4

normally acknowledges input 1 with output 3, and 2 with 4, but will acknowledge the next 2 after a 1 with 3; concurrent inputs and consecutive inputs on 1 aren't allowed

1 2 mutex 3 4

acknowledges 1 with 3 and 1 with 3 again, or 2 with 4 and 2 with 4 again, allowing concurrent inputs but not acknowledging the alternative until a pending sequence completes

Other DI primitives than these may be emulated by the use of macros. A macro definition begins with the word .macro on a line by itself (or with comments) and ends with a line containing the word .endmacro by itself. The first line following the .macro line (other than nested macro definitions) contains one or more input node numbers, followed by a user-selected macro name, followed by one or more output node numbers, all separated by spaces. The macro name must not coincide with that of any built in primitive, must not begin with a period, and must contain at least one non-numeric character.

The remainder of the macro definition has the same format as the main netlist, but may not contain input or output signal namess, and must satisfy the constraint that input node numbers on components within a macro are either outputs from components within it or inputs declared on the first line. Outputs are similarly constrained, and all input and output node numbers in the declaration must be used in the body.

For example,

       .macro
       0 1 2 three_input_xor 3         # the declaration
       0 1 xor 4                       # the body
       2 4 xor 3
       .endmacro

A macro may be invoked on a line with a similar form to that of a built in primitive, where the macro name is used instead of the name of a primitive, and lengths of the input and output node number sequences match those defined in the macro. The effect will be as if the macro body is textually inserted into the netlist at the point where it is invoked, with appropriate node number substitutions, and with additional unique node numbers for internal nodes created as needed.

The example above could make use of a three-input xor gate macro as follows.

       # inputs and outputs

       a 0
       1 c
       2 b

       # reusable IP core ;)

       .macro
       0 1 2 three_input_xor 3
       0 1 xor 4
       2 4 xor 3
       .endmacro

       # the main netlist

       0 fork 4 3
       16 toggle 13 17
       9 17 celement 1
       11 5 diverter 20 19
       20 toggle 14 18
       18 19 diverter 21 16
       21 toggle 15 10
       3 12 15 three_input_xor 7    # macro invoked here
       24 toggle 11 25
       10 25 celement 2
       13 6 diverter 28 27
       28 toggle 12 26
       26 27 diverter 29 24
       29 toggle 23 9
       14 4 23 three_input_xor 8              # and here
       7 8 mutex 5 6

As this example shows, node numbers within a macro are not required to be distinct from those outside it, and are not identified with them where they coincide. Nested macros are allowed, and will observe the name priority and static scope rules you would expect. (I.e., you can cut and paste macros between files without worrying about name clashes if the macros they use are contained inside them.) Macro definitions must textually precede their use, and hence cyclic dependences are precluded.

If the --list option is selected, a file will be written showing the netlist after macro expansion for each spec-file or implementation-file parameter that uses this format.

4. Plot Types

Any of the keywords below (or any unambiguous abbreviation thereof) may appear in a comma separated list following the --plots option on the command line.

Each requested plot type causes a file to be written with a suffix of .dot, and the remainder of the name composed from the keyword and an input file name, as in canonical-petrinet-myfile.dot. The files contain instructions for the dot graph rendering tool, allowing it to generate a Postscript rendering of the associated Petri net (see 8. Examples).

4.1 Petri Net Plot Types

If a spec-file and an implementation-file are both given, each requested plot type causes a plot to be generated for each file. If the --list option is indicated, another file is written for each plot with a suffix of .lis, containing the Petri net expressed in the format described above.

Here is an explanation of each Petri net plot type.

petrinet

This plot could mean several things.

• If the specification is a Petri net, this plot will simply render it either as given or with local optimizations in case of the --optimize option.
• If an environment has been specified, both the system and the environment are depicted as a combined closed Petri net.
• If the specification is in the form of a DI netlist with no environment, the plot depicts an open Petri net that models the circuit in the sense that the possible non-hazardous interactions with the circuit are precisely those that are also possible for the Petri net and can never enable multiple tokens to inhabit the same place.
• If the specification is a DI netlist with an environment, the plot depicts the (closed) Petri net whose reachable safe firing sequences projected onto the observable transitions constitute the range of possible interactions between the circuit and that environment.

canonical-petrinet

This plot is similar to the above except that the result is always an open Petri net modeling the circuit, even if the original specification is closed or has an environment (with any environmental constraints now having become implicit in the system). It is obtained from a direct translation of the refined-transducer plot into an open Petri net. This plot may take exponential time to generate.

k-hot-petrinet

This plot is a generalization of the canonical form in which a state of the system is encoded by a set of places, some k of which are are always marked. The general form is usually more complex despite sometimes requiring fewer places. The value of k should be specified with the k-hot-code option (see above).

half-hot-petrinet

This plot is similar to the k-hot-petrinet but chooses the value of k automatically to minimize the number n of places needed to encode the state, which implies that k is half of n.

quasi-canonical

This plot is similar to the canonical-petrinet plot but is derived from a combination of the refined-tranducer and serial-refinement models. It is usually simpler and equivalent to the canonical form but there is no assurance of it being so.

quasi-k-hot

This plot is to the k-hot-petrinet as the quasi-canonical is to the canonical. That is, it will be simpler or identical but may or may not be equivalent. It also requires the parameter k to be specified using the k-hot-code option.

semi-canonical

This plot is constructed by building both the canonical-petrinet and semi-canonical models and testing them for equivalence. If they are equivalent, the smaller one is chosen, but otherwise the canonical form is chosen, and in either case the result is then locally optimized. This plot is therefore the most time consuming but gives the best results.

4.2 Reachability Graph Plot Types

Any of these keywords may also be included in a comma separated list following the --plots option, and will call for the construction of a picture of a reachability graph, which is a directed graph whose nodes are Petri net markings and whose edges may be labeled with transitions.

A plot is generated for each requested type and for each spec-file and implementation-file parameter, with a name derived from the keyword combined with the file name and a suffix of .dot.

full-graph

This type of plot shows the conventional reachability graph for the Petri net associated with the original specification, with the exception that paths are sometimes truncated where a marking is found to enable an unobservable unsafe transition.

• An edge connects one node to another if and only if the firing of a single transition will transform the origin to the terminus.
• The edge is labeled with this transition if it is observable.
• Disabled transitions and those leading to an unsafe marking are not depicted (although this distinction is maintained internally).

reachability-graph

This type of plot depicts an abbreviated form of the above graph wherein one marking can be adjacent to another whenever the collective firing of a set of "independent" transitions effects the transformation. Markings reached only by firing individual members of such sets are not shown, nor are disabled or unsafe transitions, and edges are labeled as above. (This is the graph that is used internally for property testing.)

reduced-graph

In this plot type, a further simplified version of the above graph is shown. This graph is used internally as the basis for constructing state machines and transducer models.

• All nodes having unsafe enabled transitions that are either unobservable or associated with output signals of the circuit are themselves deemed unsafe and deleted.
• All remaining unlabeled edges are eliminated by connecting their origins directly to the successors of their termini, except those that are needed to indicate non-determinacy.
• All nodes rendered unreachable by this transformation are deleted.
• All resulting "equivalent" markings are merged.

4.3 Trace Oriented Plot Types

Any of these keywords may also be included in a comma separated list following the --plots option. Their effect is the construction of graphical representations that express a set of sequences of input and output signals of a circuit (a.k.a. traces) in the form of a directed graph whose nodes are considered states of the circuit. The edges in the graph are labeled with signals and the traces are those sequences of signals that can be read off the edges by following any path from the initial to an accepting state. Accepting states are indicated as circles within circles.

Some of these will apply individually to each of a spec-file and an implementation-file parameter, but others produce a single plot based jointly on them.

If the --traces option is selected, a file with a .trc suffix will also be written for each of these plots, and will contain some examples of accepted traces. The examples are obtained by way of a breadth first search of the graph to find a short path to each accepting state, and will not include all possible traces or even all shortest traces.

quiescences

This plot type shows the set of traces in which the circuit will normally engage, with the accepting states being those in which the circuit may withhold further output. Such states may or may not indicate an error due to deadlock, depending on what the specification requires.

divergences

A plot of this type illustrates the traces that will cause the circuit to glitch (i.e., the graph deliberately accepts only the unsafe traces). Accepting states in these graphs are always trap states, indicating that no trace can be considered safe after the first glitch.

failures

This type of plot depicts the union of the quiescences and the divergences, and is used mainly for purposes of comparison between circuits or specifications.

hazards

For this type of plot, both a spec-file and an implementation-file are required. This plot depicts the set of traces that suffice to cause the implementation either to crash or to produce an output prohibited by the specification, even though all inputs in the traces are allowed by the specification. If the implementation is correct, this plot should be empty, but otherwise it identifies the causes of errors due to glitches.

deadlocks

This type of plot also requires both a spec-file and an implementation-file. It shows the traces that are quiescent for the implementation and not quiescent but nevertheless safe for the specification. The existence of such traces constitutes an implementation error due to deadlock. If the implementation is correct, this plot should be empty, but otherwise it gives an indication of how it gets hung up.

extras

Both a spec-file and an implementation-file are required for this plot type. The graph shows the traces that are quiescent for the implementation but only after receiving at least one input signal that is prohibited according to the specification. These traces can be interpreted as unrequired or extra features of the implementation. A large graph may indicate that the implementation contains some unnecessary circuitry and could be designed more economically. Whether empty or not, this graph does not imply that the circuit meets the specification.

4.4 Transducer Plot Types

The following keywords are also acceptable plot types that may be used with the --plots option. In these plots, a circuit or specification is depicted as a directed graph whose nodes are identified with states, and whose edges are labeled with two sets of signals, one containing inputs and the other outputs.

The interpretation is that the system may undergo a state change when all members of the set of input signals labeling an edge originating on its current state are furnished by the environment, and in so doing transmits all outputs associated with the edge. In the event of a set of inputs which is not a subset of any of those labeling the edges originating on its current state, the transducer plot does not depict the effect. It may be associated either with deadlock or divergence.

A circle within a circle represents a state in which the system may choose not to proceed even when a suitable set of inputs is available (always a bad sign).

All of these plots pertain to a spec-file or an implementation-file individually.

transducer

This plot type calls for the construction of a transducer plot that is equivalent to the original description in the input file.

serial-approximation

For this plot type, the transducer excludes all edges whose input sets are proper supersets of those of other edges originating on the same state, as well as any states that become unreachable when these edges are excluded. This transducer is therefore not generally equivalent to the original file, but may be interpreted as an approximation to it that would serve as an acceptable substitute in an environment that sends only one input at a time and pauses long enough for a state change after each.

unit-transducer

The transducer depicted in this plot type is equivalent to that of the serial-approximation, but will have been further transformed so as to retain at most one element in every edge's set of inputs (by inserting extra intermediate states if necessary).

refined-transducer

This plot depicts the result of an aggressive optimization of the standard transducer plot made possible when the requirement of equivalence is relaxed. The transducer will be an acceptable substitute for the original in any environment, but may prescribe a behavior for the system where the original specification left it undefined.

serial-refinement

This plot is to the refined-transducer as the serial-approximation is to the standard one.

unit-refinement

This plot is the the refined-transducer as the unit-approximation is to the standard one.

5. Style Types

A modest choice of style parameters is supported, which will apply to all plots generated during the run. Any combination of these parameters may appear in a comma separated list following the --style option on the command line.

inverse

Use a color scheme suitable for display on a dark background, as in a poster or slide presentation.

horizontal

Construct the plot in a manner conducive to making the graph turn out wider than it is long.

expanded

Put some extra distance into the plot, thereby allowing easier viewing in cases of densely concentrated edges.

6. Test Types

Any combination of these keywords may be supplied on the command line in a comma separated list following the --tests option. Each of them causes the result of a property test described below to be printed to standard output, along with some run time statistics.

These tests are most useful when verification by visual inspection of a plot is infeasible due to the size or complexity of a circuit. Typically a circuit to be tested would be expressed as a netlist, with the environment and perhaps the specification expressed as Petri nets that are presumably correct. The environment can be constructed to become unsafe or to deadlock when interacting with the circuit unless the circuit responds exactly as it should. In the course of these tests, the circuit is converted internally to a Petri net and combined with the environment.

safety

This property means no marking is reachable in which any place is occupied by more than one token. It implies that the circuit is free of hazards and that it sends no unexpected signals to the environment. It also means that the environment sends no unexpected signals to the circuit, so you will have to specify a compatible environment in order to get any useful information from this test.

liveness

This property means that every reachable marking has at least one successor. If it holds, the circuit is free of deadlock and always sends the signals expected by the environment (if any).

reusability

This property means that the initial marking is reachable from any other reachable marking, and implies that the circuit never gets stuck in a mode from which it can't escape. It should be true of most circuits unless they are deliberately designed to have an initialization phase that is never re-entered.

fairness

This property means that for every output signal, there is at least one reachable marking in which it is enabled, and for every input signal, there is at least one reachable marking in which it is safe. If reusability and fairness both hold, it is an indication that the circuit is fair in the conventional sense, at least as far as it can be established without an analog simulation.

equivalence

This test requires both a spec-file and an implementation-file parameter, but not necessarily an environment-file. With no environment, it implies that the specification and the implementation behave indistinguishably in all circumstances. With an environment, it implies that the environment does not exercise any features whereby they differ. It can be used to test whether two circuits are equivalent, but is stronger than necessary to test whether a circuit meets its specification.

refinement

This test also requires both a spec-file and an implementation-file parameter, but not necessarily an environment-file. If it holds, it implies that the implementation meets the specification (or at least that it does within the given environment). They are not necessarily equivalent because the implementation may prescribe a behavior where the specification leaves it undefined. Note that this relation is not commutative and requires that the parameters be given in the right order on the command line.

anti-refinement

This test is exactly the same as refinement except that the roles of the spec-file and the implementation-file are reversed.

weak-refinement

This test requires both a spec-file and an implementation-file parameter, but not necessarily an environment-file. It works by converting both the specification and the implementation to refined transducers as in the refined-transducer plot type, and then testing whether the specification is a subgraph of the implementation. This condition does not always imply refinement, but in some situations it is a more appropriate test of compatibility, e.g., when the specification is a blocking approximation of a non-blocking implementation.

7. Diagnostics

A selection of run-time diagnostic messages is explained here in case their meanings are not obvious. Most of these are written to standard output, usually with some additional contextual information such as file names, line numbers, or offending keywords, but overflow errors, i/o errors, and serious internal errors not listed here are written to standard error.

exec: avram: not found

The short answer is that you need to install a program called avram in order for diana to run, which can be downloaded from the author's home page http://www.lsbu.ac.uk/~fureyd/avram for free. If it's already installed, its directory needs to be included in your PATH environment variable. diana is a shell script containing virtual machine code that is executed by avram.

avram: cannot execute

See above, and also check that you have execute permission set on the avram executable file.

memory overflow

This error is most likely the result of state explosion when analyzing a large system. Input files in Petri net format are somewhat more memory efficient than netlists and may be a possible workaround. Otherwise, the standard remedy is to buy a bigger computer, but anything that takes more memory than you have just to build is probably infeasibly time consuming to analyze.

7.1 general usage errors

These messages pertain erroneous or inconsistent selections of command line options or parameters. Although some of these may seem picky, they are based on the assumption that it is less annoying to read one of them than to find out only at the end of a long run that some inconsistent choice of options was silently disregarded or misinterpreted.

plots required but not specified

The --style and --list options have no effect unless you're doing some --plots. If you've forgotten to mention them, here's your chance to remember.

no options specified

without which diana is instructed to do nothing; surely not your intention

input file(s) required

Almost any option is useless without input files, so this is a reminder to specify them. If you have, check their positions on the command line to make sure the file names weren't mistaken for option parameters or keywords, which can be avoided by putting all the file names first.

too many input files

A specification, an implementation, and an environment make three. Check your dashes and commas to ensure that an option or other parameter keyword was not mistaken for a file name. If you want to use more than one file to store a netlist or a Petri net, there are Unix ways to concatenate them.

unrecognized option(s)

Something other than one of the required keywords was entered as an option on the command line, or maybe a keyword for a plot type or test type was given by itself without a --plots or --tests option.

unrecognized plot type(s)

Something other than one of the required plot type keywords came after a --plots option. Perhaps it was a test type in the wrong place.

unrecognized test type(s)

similar

unrecognized style type(s)

similar

plot type(s) required

The --plots option was specified but no particular plot type keywords were listed after the option, which may mean they were mistakenly omitted.

test type(s) required

similar

ambiguous option(s)

The keyword used for an option was too short to distinguish it from another one with a common prefix. Type the whole keyword or at least enough to make it unambiguous.

ambiguous test type(s)

similar to an ambiguous option, but pertains to the parameters associated with the --tests option

ambiguous plot type(s)

similar to an ambiguous option, but pertains to the parameters associated with the --plots option

missing or invalid --k-hot-code number

This option must be used when the k-hot-petrinet plot is requested, and the number must be provided and must be a decimal string other than 0.

two systems required

Certain plot types and test types such as equivalence involve the comparison of two entities, and are not meaningful when only one is given. This message indicates either that one of them has been left out, or that the associated plot or test was requested in error.

--open-specification: not applicable

This option is meaningful only when there are three input files, one of which represents the environment, as it directs diana to associate the environment with the implementation but not with the specification. The message occurs when you attempt to use it with only one or two files.

virtual code file required

diana wondered why you used the --dimensions option when the input files are only text files, for which it has no effect. This option is meant to be used when the input file contains the virtual code to generate any of a family of specifications parameterized by operands following the --dimensions option. If this explanation makes no sense, you can fix the problem by not using this option.

7.2 Petri net parsing errors

These messages refer to problems with an input file in Petri net format.

signed transitions not supported

Things like s+ and s- may be ok for petrify but not for diana, which requires a real Petri net and not just an STG. Besides, logic levels are not modeled in any way because only the changes in levels matter.

invalid arc(s)

Either a connection was made directly from a place to a place, or a transition used in the .graph section was not previously declared in the .inputs, .outputs or .dummy sections.

misused transition(s)

A name appears to be refer to both a place and a transition, possibly as the indirect result of an input transition being connected directly to another input or an output connected to another output.

7.3 netlist parsing errors

These messages refer to problems with an input file in netlist format.

netlist format error

A line contains something other than a sequence of numbers followed by an identifier followed by another sequence of numbers, or a comment, or the words .macro or .endmacro. The error can also be caused by an input or output signal with more than one node number. If the error is on line 1, make sure you didn't specify an input file name with the wrong suffix. Then check the indicated line number for spurious characters.

duplicate input node(s)

The same node number is used as an input to two different components, or twice for the same component, which is not allowed. If you want to use the same signal in two places, put it through a fork.

duplicate output node(s)

The same node number is used as an output from two different components, or twice for the same component, which is not allowed. If you want a signal to come from two places, put them through an xor or a celement, depending on whether you want the result from either or both.

duplicate signal name(s)

The same name was used for more than one signal, albeit with different node numbers, such as two outputs both called ack. The names of all input and output signals must be unique.

wrongly connected

A primitive DI component was used with the wrong number of input or output connections. Each primitive requires a fixed number of connections. See 3.2 DI Netlist File Format for examples.

unrecognized name

The name of something is neither a built in primitive nor a user defined macro. You could either have made a spelling error, or attempted to invoke a macro ahead of its definition, or if you have nested macros, then you might have tried to invoke one outside of the macro in which it is defined.

floating input node(s)

A macro body contains an input node number that's neither an output from anywhere else in the macro nor an input in the declaration, or the declaration contains an input that's not used in the body. Macros must have no "global" node numbers.

floating output node(s)

analogous to the above error

external signal in a macro

Named signal declarations (like a,b,send,ack, etcetera) can appear only in the main body of the netlist and not within a macro. This error could also result from an attempt to define some sort of a sink or source macro with only inputs or only outputs, which is not allowed and BTW useless because it would not be delay insensitive except in very restricted cases.

misused macro

A macro was invoked with the wrong number of node number parameters. It must have the same number of inputs and outputs as the declaration. Variable numbers of parameters are not supported. Check for missing spaces between the numbers or other typos.

unmatched .endmacro

The keywords .macro and .endmacro must occur in matched pairs like parentheses, and one of them is missing somewhere. If you have lots of them in the file, check that none is misspelled or mistakenly commented out.

unfinished .macro

see above

7.4 semantic errors

These errors pertain to inconsistencies among syntactically correct input files.

incompatible interfaces

This message means input and output signals don't match up between file parameters, and shows the sets of signals inferred from each. If a spec-file and an implementation-file parameter are given, they should have identical inputs and outputs. If an environment-file parameter is given, the inputs of the environment-file should be the outputs of the other(s), and vice versa. Otherwise no meaningful comparisons are possible.

can't connect closed transitions

This message means that an environment could not be combined with a specification or implementation because at least one is a closed or partly closed Petri net. For environments to work, both the environment and at least one of the specification or implementation must be either a DI netlist or an open Petri net. In an open Petri net, no arcs come out of output transitions and none come into input transitions. The message lists the inputs and outputs that do not meet this condition.

7.5 internal errors

Don't waste any time on these beyond reporting them to the author or maintainer, unless you feel like hacking the code yourself. Bug reports are most helpful when they include a small input file that consistently causes the error. Other internal errors that should be reported would be the word unsupported or anything other than yes or no as a property test result.

can't plot due to internal errors

Inconsistencies in the graph data structures were discovered when it was time to plot them.

unsupported plot type

A new feature was added but not all the necessary places were updated.

invalid deconstruction

An error was so bad that no more informative diagnostic message was possible. This error could originate from diana itself or from virtual code input files if they are used.

(unprintable error message)

Similar to the above, but in this case the error was so bad that another error occurred on top of it in the course of reporting the first one.

undiagnosed run-time error

see above

8. Examples

The circuit below was proposed for a two-to-four phase protocol converter, which interfaces an active two phase handshaking port (ls,la) with a passive four phase port (rs,ra).

       ls 0
       3 la
       6 rs
       ra 7
       0 fork 1 2
       2 4 celement 3
       7 toggle 5 4
       1 5 xor 6

It was pointed out to me by Steve Furber that the C element is unnecessary and the following circuit should work just as well.

       ls 0
       4 la
       2 rs
       ra 3
       3 toggle 1 4
       0 1 xor 2

To investigate this claim, we put the first specification in a file named pcon and the second in rpcon, and run

       $ diana pcon rpcon --plots petrinet,quiescences
       diana: writing `quiescences-pcon.dot'
       diana: writing `petrinet-pcon.dot'
       diana: writing `quiescences-rpcon.dot'
       diana: writing `petrinet-rpcon.dot'

To create Postscript renderings of each of these plots we run

       $ dot -Tps -o quiescences-pcon.ps quiescences-pcon.dot
       $ dot -Tps -o petrinet-pcon.ps petrinet-pcon.dot
       $ dot -Tps -o quiescences-rpcon.ps quiescences-rpcon.dot
       $ dot -Tps -o petrinet-rpcon.ps petrinet-rpcon.dot

and then use gv to view each one, as in

       $ gv quiescences-pcon.ps &

On this basis they do not appear equivalent, but we recall that the environment is assumed to follow a handshaking protocol, so we model it by the following simple Petri net.

       .inputs la rs
       .outputs ls ra
       .dummy 
       .graph
       la i
       ls
       ra
       rs y
       i ls
       y ra
       .marking {i}
       .end

To check that this Petri net was constructed as intended we put it in a file called pcenv and run

       $ diana pcenv --plots pet
       diana: writing `petrinet-pcenv.dot'
       $ dot -Tps -o petrinet-pcenv.ps petrinet-pcenv.dot
       $ gv petrinet-pcenv.ps

We can investigate the behavior of each circuit within this restricted environment by running

       $ diana pcon rpcon pcenv --plots=transducer
       diana: writing `transducer-pcon.dot'
       diana: writing `transducer-rpcon.dot'

where we have opted to construct the transducer plots instead this time. They are now easily seen to be identical by viewing the Postscript renderings. However, if these circuits had been too big or complicated to compare the transducer plots by inspection, we could have used

       $ diana pcon rpcon pcenv --tests=equivalence

       specification: pcon
       8 places
       6 transitions
       8 markings
       6 reduced markings

       implementation: rpcon
       7 places
       6 transitions
       8 markings
       6 reduced markings

       equivalence: yes

9. Environment

On GNU systems, you can set an environment variable AVMINPUTS to a colon separated list of directories similarly to the PATH environment variable, and diana will search them for input files.

10. Bugs

There are no known bugs currently outstanding. A known issue is that equivalence can hold between an open system and a closed system (which could be compared by using the --open-specification option, among other ways) insofar as they can have the same failures, even though safety will differ between them due to their environments. This issue seems to be down to safety being a feature of the Petri net model, whereas equivalence is extensional.

11. Acknowledgements

Many thanks to all participants in the U.K. Asynchronous Forum meetings for peer-reviewing the ideas on which diana is based, and to Mark Josephs and Hemangee Kapoor for testing it and bringing several bugs to my attention.

I'm available for any kind of part time consulting work related to design or analysis of DI circuits, which might not seem so far fetched by the end of the decade when propagation delays on wires will typically exceed component delays by an order of magnitude or more. Although the source code is freely distributed, I can also customize diana for those who don't care to do it themselves.

GNU GENERAL PUBLIC LICENSE

Copyright © 1989, 1991 Free Software Foundation, Inc.
675 Mass Ave, Cambridge, MA 02139, USA

Everyone is permitted to copy and distribute verbatim copies
of this license document, but changing it is not allowed.

Preamble

The licenses for most software are designed to take away your freedom to share and change it. By contrast, the GNU General Public License is intended to guarantee your freedom to share and change free software--to make sure the software is free for all its users. This General Public License applies to most of the Free Software Foundation's software and to any other program whose authors commit to using it. (Some other Free Software Foundation software is covered by the GNU Library General Public License instead.) You can apply it to your programs, too.

When we speak of free software, we are referring to freedom, not price. Our General Public Licenses are designed to make sure that you have the freedom to distribute copies of free software (and charge for this service if you wish), that you receive source code or can get it if you want it, that you can change the software or use pieces of it in new free programs; and that you know you can do these things.

To protect your rights, we need to make restrictions that forbid anyone to deny you these rights or to ask you to surrender the rights. These restrictions translate to certain responsibilities for you if you distribute copies of the software, or if you modify it.

For example, if you distribute copies of such a program, whether gratis or for a fee, you must give the recipients all the rights that you have. You must make sure that they, too, receive or can get the source code. And you must show them these terms so they know their rights.

We protect your rights with two steps: (1) copyright the software, and (2) offer you this license which gives you legal permission to copy, distribute and/or modify the software.

Also, for each author's protection and ours, we want to make certain that everyone understands that there is no warranty for this free software. If the software is modified by someone else and passed on, we want its recipients to know that what they have is not the original, so that any problems introduced by others will not reflect on the original authors' reputations.

Finally, any free program is threatened constantly by software patents. We wish to avoid the danger that redistributors of a free program will individually obtain patent licenses, in effect making the program proprietary. To prevent this, we have made it clear that any patent must be licensed for everyone's free use or not licensed at all.

The precise terms and conditions for copying, distribution and modification follow.

1. This License applies to any program or other work which contains a notice placed by the copyright holder saying it may be distributed under the terms of this General Public License. The "Program", below, refers to any such program or work, and a "work based on the Program" means either the Program or any derivative work under copyright law: that is to say, a work containing the Program or a portion of it, either verbatim or with modifications and/or translated into another language. (Hereinafter, translation is included without limitation in the term "modification".) Each licensee is addressed as "you".

   Activities other than copying, distribution and modification are not covered by this License; they are outside its scope. The act of running the Program is not restricted, and the output from the Program is covered only if its contents constitute a work based on the Program (independent of having been made by running the Program). Whether that is true depends on what the Program does.

2. You may copy and distribute verbatim copies of the Program's source code as you receive it, in any medium, provided that you conspicuously and appropriately publish on each copy an appropriate copyright notice and disclaimer of warranty; keep intact all the notices that refer to this License and to the absence of any warranty; and give any other recipients of the Program a copy of this License along with the Program.

   You may charge a fee for the physical act of transferring a copy, and you may at your option offer warranty protection in exchange for a fee.

3. You may modify your copy or copies of the Program or any portion of it, thus forming a work based on the Program, and copy and distribute such modifications or work under the terms of Section 1 above, provided that you also meet all of these conditions:
   1. You must cause the modified files to carry prominent notices stating that you changed the files and the date of any change.

   2. You must cause any work that you distribute or publish, that in whole or in part contains or is derived from the Program or any part thereof, to be licensed as a whole at no charge to all third parties under the terms of this License.

   3. If the modified program normally reads commands interactively when run, you must cause it, when started running for such interactive use in the most ordinary way, to print or display an announcement including an appropriate copyright notice and a notice that there is no warranty (or else, saying that you provide a warranty) and that users may redistribute the program under these conditions, and telling the user how to view a copy of this License. (Exception: if the Program itself is interactive but does not normally print such an announcement, your work based on the Program is not required to print an announcement.)

   These requirements apply to the modified work as a whole. If identifiable sections of that work are not derived from the Program, and can be reasonably considered independent and separate works in themselves, then this License, and its terms, do not apply to those sections when you distribute them as separate works. But when you distribute the same sections as part of a whole which is a work based on the Program, the distribution of the whole must be on the terms of this License, whose permissions for other licensees extend to the entire whole, and thus to each and every part regardless of who wrote it.

   Thus, it is not the intent of this section to claim rights or contest your rights to work written entirely by you; rather, the intent is to exercise the right to control the distribution of derivative or collective works based on the Program.

   In addition, mere aggregation of another work not based on the Program with the Program (or with a work based on the Program) on a volume of a storage or distribution medium does not bring the other work under the scope of this License.

4. You may copy and distribute the Program (or a work based on it, under Section 2) in object code or executable form under the terms of Sections 1 and 2 above provided that you also do one of the following:
   1. Accompany it with the complete corresponding machine-readable source code, which must be distributed under the terms of Sections 1 and 2 above on a medium customarily used for software interchange; or,

   2. Accompany it with a written offer, valid for at least three years, to give any third party, for a charge no more than your cost of physically performing source distribution, a complete machine-readable copy of the corresponding source code, to be distributed under the terms of Sections 1 and 2 above on a medium customarily used for software interchange; or,

   3. Accompany it with the information you received as to the offer to distribute corresponding source code. (This alternative is allowed only for noncommercial distribution and only if you received the program in object code or executable form with such an offer, in accord with Subsection b above.)

   The source code for a work means the preferred form of the work for making modifications to it. For an executable work, complete source code means all the source code for all modules it contains, plus any associated interface definition files, plus the scripts used to control compilation and installation of the executable. However, as a special exception, the source code distributed need not include anything that is normally distributed (in either source or binary form) with the major components (compiler, kernel, and so on) of the operating system on which the executable runs, unless that component itself accompanies the executable.

   If distribution of executable or object code is made by offering access to copy from a designated place, then offering equivalent access to copy the source code from the same place counts as distribution of the source code, even though third parties are not compelled to copy the source along with the object code.

5. You may not copy, modify, sublicense, or distribute the Program except as expressly provided under this License. Any attempt otherwise to copy, modify, sublicense or distribute the Program is void, and will automatically terminate your rights under this License. However, parties who have received copies, or rights, from you under this License will not have their licenses terminated so long as such parties remain in full compliance.

6. You are not required to accept this License, since you have not signed it. However, nothing else grants you permission to modify or distribute the Program or its derivative works. These actions are prohibited by law if you do not accept this License. Therefore, by modifying or distributing the Program (or any work based on the Program), you indicate your acceptance of this License to do so, and all its terms and conditions for copying, distributing or modifying the Program or works based on it.

7. Each time you redistribute the Program (or any work based on the Program), the recipient automatically receives a license from the original licensor to copy, distribute or modify the Program subject to these terms and conditions. You may not impose any further restrictions on the recipients' exercise of the rights granted herein. You are not responsible for enforcing compliance by third parties to this License.

8. If, as a consequence of a court judgment or allegation of patent infringement or for any other reason (not limited to patent issues), conditions are imposed on you (whether by court order, agreement or otherwise) that contradict the conditions of this License, they do not excuse you from the conditions of this License. If you cannot distribute so as to satisfy simultaneously your obligations under this License and any other pertinent obligations, then as a consequence you may not distribute the Program at all. For example, if a patent license would not permit royalty-free redistribution of the Program by all those who receive copies directly or indirectly through you, then the only way you could satisfy both it and this License would be to refrain entirely from distribution of the Program.

   If any portion of this section is held invalid or unenforceable under any particular circumstance, the balance of the section is intended to apply and the section as a whole is intended to apply in other circumstances.

   It is not the purpose of this section to induce you to infringe any patents or other property right claims or to contest validity of any such claims; this section has the sole purpose of protecting the integrity of the free software distribution system, which is implemented by public license practices. Many people have made generous contributions to the wide range of software distributed through that system in reliance on consistent application of that system; it is up to the author/donor to decide if he or she is willing to distribute software through any other system and a licensee cannot impose that choice.

   This section is intended to make thoroughly clear what is believed to be a consequence of the rest of this License.

9. If the distribution and/or use of the Program is restricted in certain countries either by patents or by copyrighted interfaces, the original copyright holder who places the Program under this License may add an explicit geographical distribution limitation excluding those countries, so that distribution is permitted only in or among countries not thus excluded. In such case, this License incorporates the limitation as if written in the body of this License.

10. The Free Software Foundation may publish revised and/or new versions of the General Public License from time to time. Such new versions will be similar in spirit to the present version, but may differ in detail to address new problems or concerns.

    Each version is given a distinguishing version number. If the Program specifies a version number of this License which applies to it and "any later version", you have the option of following the terms and conditions either of that version or of any later version published by the Free Software Foundation. If the Program does not specify a version number of this License, you may choose any version ever published by the Free Software Foundation.

11. If you wish to incorporate parts of the Program into other free programs whose distribution conditions are different, write to the author to ask for permission. For software which is copyrighted by the Free Software Foundation, write to the Free Software Foundation; we sometimes make exceptions for this. Our decision will be guided by the two goals of preserving the free status of all derivatives of our free software and of promoting the sharing and reuse of software generally.
    NO WARRANTY

12. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

13. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGES.

How to Apply These Terms to Your New Programs

If you develop a new program, and you want it to be of the greatest possible use to the public, the best way to achieve this is to make it free software which everyone can redistribute and change under these terms.

To do so, attach the following notices to the program. It is safest to attach them to the start of each source file to most effectively convey the exclusion of warranty; and each file should have at least the "copyright" line and a pointer to where the full notice is found.

one line to give the program's name and an idea of what it does.
Copyright (C) 19yy  name of author

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Also add information on how to contact you by electronic and paper mail.

If the program is interactive, make it output a short notice like this when it starts in an interactive mode:

Gnomovision version 69, Copyright (C) 19yy name of author
Gnomovision comes with ABSOLUTELY NO WARRANTY; for details
type `show w'.  This is free software, and you are welcome
to redistribute it under certain conditions; type `show c' 
for details.

The hypothetical commands `show w' and `show c' should show the appropriate parts of the General Public License. Of course, the commands you use may be called something other than `show w' and `show c'; they could even be mouse-clicks or menu items--whatever suits your program.

You should also get your employer (if you work as a programmer) or your school, if any, to sign a "copyright disclaimer" for the program, if necessary. Here is a sample; alter the names:

Yoyodyne, Inc., hereby disclaims all copyright
interest in the program `Gnomovision'
(which makes passes at compilers) written 
by James Hacker.

signature of Ty Coon, 1 April 1989
Ty Coon, President of Vice

This General Public License does not permit incorporating your program into proprietary programs. If your program is a subroutine library, you may consider it more useful to permit linking proprietary applications with the library. If this is what you want to do, use the GNU Library General Public License instead of this License.

Concept Index

Table of Contents

1. Description
2. Options
3. Files

3.1 Petri net File Format
3.2 DI Netlist File Format

4. Plot Types

4.1 Petri Net Plot Types
4.2 Reachability Graph Plot Types
4.3 Trace Oriented Plot Types
4.4 Transducer Plot Types

5. Style Types
6. Test Types
7. Diagnostics

7.1 general usage errors
7.2 Petri net parsing errors
7.3 netlist parsing errors
7.4 semantic errors
7.5 internal errors

8. Examples
9. Environment
10. Bugs
11. Acknowledgements
GNU GENERAL PUBLIC LICENSE

Preamble
How to Apply These Terms to Your New Programs

Concept Index

Short Table of Contents

1. Description
2. Options
3. Files
4. Plot Types
5. Style Types
6. Test Types
7. Diagnostics
8. Examples
9. Environment
10. Bugs
11. Acknowledgements
GNU GENERAL PUBLIC LICENSE
Concept Index

About this document

where the Example assumes that the current position is at Subsubsection One-Two-Three of a document of the following structure:

• 1. Section One
  • 1.1 Subsection One-One
    • ...
  • 1.2 Subsection One-Two
    • 1.2.1 Subsubsection One-Two-One
    • 1.2.2 Subsubsection One-Two-Two
    • 1.2.3 Subsubsection One-Two-Three     <== Current Position
    • 1.2.4 Subsubsection One-Two-Four
  • 1.3 Subsection One-Three
    • ...
  • 1.4 Subsection One-Four