Myers Research Group
University of Utah
People
Research
Tools
Publications
Book
Home Page
ATACS Manual
- File type
- Timing methods
- Technology
- Action
- ATACS errors
- Production rules
- /* 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
-
delay mygates = <2,3; 1,2>;
- 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. */
- [ guard1 -> statements1
- | guard2 -> statements2
- | etc.
-
]
- [ a+ & b+ -> c+
- | c- | d- -> e+
-
]
- [ done- -> req+; [ack+]; req-; [ack-]; *
- | done+ -> skip
- ]; end+
- process inverter;
- [ true -> [a+ -> skip]; b-; [a- -> skip]; b+; * ]
- endprocess
- process inverter;
- *[ [a+]; b-; [a-]; b+ ]
- endprocess
- /* 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
-
delay mygates = <2,3; 1,2>;
- 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. */
- [ guard1 -> statements1
- | guard2 -> statements2
- | etc.
-
]
- [ a & b -> c+
- | ~a | ~b -> d+
-
]
- [ ~done -> req+; [ack]; req-; [~ack]; *
- | done -> skip
- ]; end+
- process inverter;
- [ true -> [a -> skip]; b-; [~a -> skip]; b+; * ]
- endprocess
- process inverter;
- *[ [a]; b-; [~a]; b+ ]
- endprocess
- [ 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.
- [+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.
File type
There are five input file types. There are csp files, handshaking expansion files (HSE), VHDL files, signal transition graph files (G), and burst-mode state machine files (UNC). Each type is described in detail below.CSP Files
A brief description of the constructs found in CSP files is given below.Modules
A module is composed of a name, set of delay macros, signal declarations, and process statements. For example: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: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: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: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 both rise, then c is set to true. Otherwise, if either c or d fall, then e is set to true.
Guarded commands can also loop back to the beginning of the statement when the list of statements ends with a "*". For example,
The guarded commands above loops until done rises, 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,
Can be rewritten as:
HSE Files
A brief description of the constructs found in HSE files is given below.Modules
A module is composed of a name, set of delay macros, signal declarations, and process statements. For example: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: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: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: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.
Guarded commands can also loop back to the beginning of the statement when the list of statements ends with a "*". For example,
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,
Can be rewritten as:
VHDL Files
A brief description of the constructs found in VHDL files is given below.G Files
A brief description of the constructs found in G files is given below.UNC Files
A brief description of the constructs found in UNC files is given below.Timing Methods
There are six possible timing methods to choose from: untimed, geometric, POSETs, BAG, BAP, and BAPTDC. The untimed method ignores all timing information which has been provided and synthesizes a speed-independent circuit. The geometric method uses geometric regions (or zones) to represent the timing information during state space exploration. The POSETs method also uses zones, but it also uses a POSET matrix to track timing relationships between events. The usual result is that larger zones are produced resulting in a smaller number of zones being needed to represent the timed state space. This typically results in much faster and memory efficient timed state space exploration. The BAG (Bourne Again Geometric) method is the same as the geometric method except that it uses a time-independent choice semantics. In other words, when there is a choice in the specification, the choice is made first and only then is a timing assignment made. The BAP (Bourne Again POSETs) method is similar to POSETs except that it uses only one matrix to represent each time state, the POSET matrix, rather than two. The BAP method is time-independent while BAPTDC (BAP Time-Dependent Choice) uses a time-dependent choice semantics.Technology
There are five possible target technologies: atomic gates, generalized-C, standard-C, burst-mode gC, and burst-mode 2-level. An atomic gate is one in which all delay can be assumed to be at the output of the logic function. Using this technology, one combinational logic gate is created for each output signal. 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. The burst-mode gC options produces correct generalized C-element circuits under burst-mode assumptions while burst-mode 2-level produces correct 2-level sum of products solutions also under burst-mode assumptions.Action
You can select to either do synthesis and verification. The result of synthesis is either a logic description of a circuit as a set of production rules that implements the given specification, or an error message stating why the circuit could not be produced. The result of verification is either a message that no errors were found during state space exploration or a trace that indicates a sequence of transitions leading to the error.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: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: