MODULES
A module is composed of a name, set of delay macros,
signal declarations, and process
statements. For example:
-
/* A simple inverter */
-
module mycircuit;
-
delay mygates = <2,3; 1,2>;
-
input a;
-
output b = {true, mygates};
-
process inverter;
-
*[ [a]; b-; [~a]; b+ ]
-
endprocess
-
process environment;
-
*[ a+; [~b]; a-; [b] ]
-
endprocess
-
endmodule
NOTE: text enclosed in /* and */ are comments.
DELAY MACROS
A delay macro is composed of the keyword delay, an identifier, a lower
and upper bound for rising transitions, and a lower and upper bound for
falling transitions. For example:
-
delay mygates = <2,3; 1,2>;
This delay macro is used to specify signals which have rising signal
transtions that occur between 2 and 3 time units after becoming enabled,
and falling transitions that occur between 1 and 2 time units after becoming
enabled.
SIGNAL DECLARATIONS
A signal declaration is composed of a type (either it is an input or
an output signal), an identifier, an intial value for the signal
(either true or false, where false is the default),
and a delay specification (where <0,infinity> is the default).
For example:
-
input a = {false, mygates};
/* a is an input signal which is initially false with a
-
delay of 0 to infinity. */
-
output b = {true, mygates}; /*
b is an output signal which is initially true with a
-
delay specified by the delay macro mygates. */
PROCESS STATEMENTS
A process statement is composed of a name and a sequence of statements
describing the behavior of the process. These statements can be combined
either in sequence ";" or in parallel "||". There are two basic types
of statements: signal transitions and guarded commands. For each
signal s, there are two signal transitions s+ which indicates that s goes
from false to true and s- which indicates that s goes from true to false.
A guarded command is of the form:
-
[ guard1 -> statements1
-
| guard2 -> statements2
-
| etc.
-
]
Each guard is a boolean condition which when true allows the statements
following it to occur. For example, the following guarded command
states that if signals a and b are both true, then c is set to true.
Otherwise, if neither a or b is true, then d is set to true.
-
[ a & b -> c+
-
| ~a | ~b -> d+
-
]
Guarded commands can also loop back to the beginning of the statement
when the list of statements ends with a "*". For example,
-
[ ~done -> req+; [ack]; req-; [~ack]; *
-
| done -> skip
-
]; end+
The guarded commands above loops until done is true, then it sets end
to true. Finally, there are a couple of shorthands of interest.
The first is [guard -> skip] is abbreviated as [guard]. The second is
[true -> statements;*] is abbreviated as *[statements]. For
example,
-
process inverter;
-
[ true -> [a -> skip]; b-; [~a -> skip]; b+; * ]
-
endprocess
Can be rewritten as:
-
process inverter;
-
*[ [a]; b-; [~a]; b+ ]
-
endprocess
TIMING METHODS
There are three possible timing methods to choose from: untimed, geometric,
and POSETs. The untimed method ignores all timing information which
has been provided and synthesizes a speed-independent circuit. The
geometric method uses geometric regions to represent the timing information
during state space exploration. The POSETs method also uses geometric region
representations, but it uses partial orders to form larger regions.
This typically results in much faster and memory efficient timed state
space exploration.
SYNTHESIS METHODS
There are two possible synthesis methods: single-cube and BDD. The
single cube method uses a very fast explicit method for finding a
timed circuit implementation. The BDD method uses binary decision
diagrams to implicit represent the timed state space and from this representation
it is possible to find all possible timed circuit implementations.
TECHNOLOGY
There are two possible target technologies: generalized-C and standard-C.
A generalized C-element is a gate which is composed of an arbitrary sum-of-products
function to pullup the signal as well as an arbitrary pulldown network.
The generalized-C switch states that you are mapping to such gates.
These gC gates can be decomposed into ANDs, ORs, and a single Muller C-element.
This structure is called a standard C-element and requires differenct correctness
conditions to guarantee hazard-freedom on all internal signals. Selecting
standard-C produces correct timed circuits for libraries with only ANDs,
ORs, and a C-element.
ATACS ERRORS
There are several reasons that ATACS may not be able to produce a circuit.
The first is there is a syntax error in your specification. If this
is the case, a line number where the error is discovered should be reported.
The second is the graph generated from the timed handshaking expansion
may have some problems. It may not be live which means that there
is not enough tokens in the graph and the system will deadlock. It
may not be safe which indicates that there are too many tokens in the graph.
Your specification needs to modified to make it work. Be sure that
your initial values for your signals is set properly.
The third is during state space exploration an error may be encountered
such as an unexpected deadlock. Again, this indicates a problem with
your initial specification.
Fourth, your specification may not satisfy complete state coding (or
CSC). This means there exists two states with the same binary code
which have different outputs enabled to change. In such a situation,
a circuit cannot be produced as it is unable to tell what to do when it
is in such a state. If this is the case, you need to either add a
state variable to solve the state coding problem, rearrange your signal
transitions (i.e., reshuffling), or change the timing specification to
remove the state(s).
Fifth, your specification may be non-persistent. For example if
a+ causes b+ and c+, but
a- can occur after b+ but before c+, it is said that a is non-persistent
with respect to c+. In such a situation, no single cube cover existes.
To fix this problem, try using the BDD synthesis method.
Finally, you may have a unresolvable conflict. This indicates
again that no single-cube cover exists, try using the BDD method.
PRODUCTION RULES
After a circuit is synthesized successfully, ATACS outputs a set of production
rules describing the circuit implementation that is needed to realize the
specified circuit. The simplest forms are for combinational gates.
For example:
-
[ c: (a & b)] combinational
An AND gate with inputs a and b and output c.
-
[~c: (a & b)] combinational
A NAND gate with inputs a and b and output c.
-
[ c: (a)] combinational
The next two represent an OR gate with inputs
-
[ c: (b)] combinational
a and b and output c.
Often, the implementation uses gates called generalized C-elements
(or gC). These gates an aribitrary sum-of-products pullup stack to
set the signal to true, and an arbitrary sum-of-products pulldown stack
to set the signal to false. For example:
-
[+c:(a & b)] These two productions
describe a Muller C-element.
-
[-c:(~a & ~b)]
-
[+c:(a & b)] These two productions
describe a gC-element which sets c to true
-
[-c:(~a)]
when a and b are true, but resets when only a is false.
-