Differences

This shows you the differences between two versions of the page.

--- language:langs:spec [2022/06/23 17:59]
rajit created
+++ language:langs:spec [2024/12/19 07:18] (current)
rajit [Exclusive directives]
@@ Line 1: / Line 1: @@
 ===== The spec sublanguage =====
-The ''spec'' sublanguage is used to specify properties or requirements for the circuit.
+The ''spec'' sublanguage is used to specify properties or requirements for the circuit. A standard ''spec'' directive has the following syntax:
+<code act>
+spec {
+    directive_name (sig1, sig2, ...)
+    directive_name (sig1, sig2, ...)
+    ...
+}
+</code>
+==== Exclusive directives ====
+There are four exclusive directives, two for exclusive high and two for exclusive low. The directive
+<code act>
+ spec {
+   exclhi (a,b)
+ }
+</code>
+states that the signals ''a'' and ''b'' will not be true (high) simultaneously, and this is guaranteed by the production rules in the circuit. Violations of this requirement can be detected by ''actsim'' when it is run with the ''-m'' option.
+To simplify modeling of arbiters that cannot be modeled purely at the digital level of abstraction, we include a specific directive that we call "make exclusive high".
+<code act>
+spec {
+  mk_exclhi(a,b)
+ }
+</code>
+This //forces// the signals ''a'' and ''b'' to be exclusive high in the digital simulation model.
+There are symmetric variations (''excllo'' and ''mk_excllo'') for exclusive low constraints.
+==== Simulation directives ====
+The directive ''rand_init'' is used to let the simulator know that a signal might be undefined on power-up, but will initialize to either 0 or 1 at random. The directive ''hazard'' is used to let the simulator know that a particular signal can have a switching hazard.
+==== Timing directives ====
+There are two types of timing directives: constraints, and tick specifiers on timing edges.
+=== Tick specifiers ===
+Asynchronous circuits oscillate, and each oscillation can be viewed as an iteration of the circuit. For [[asic:timing:graph|timing analysis]], it is important to indicate connections from one iteration to the next---i.e. when a signal transition from the current indication leads to a transition from the next iteration. Such directives can be computed during logic synthesis, and ACT expects all logic synthesis tools to emit these directives along with the gate-level implementation.
+<code act>
+spec {
+   timing a+ -> c-
+ }
+</code>
+This directive says that ''a+'' on a particular iteration directly leads to ''c-'' in the next iteration. (Sometimes these are called //ticked// edges in the timing graph.((S.M. Burns and A.J. Martin. Performance Analysis and Optimization of Asynchronous Circuits. Proc. ARVLSI, 1991.))((Wenmian Hua and Rajit Manohar. Exact Timing Analysis for Asynchronous Systems. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 37(1):203-216 (TCAD), January 2018.))
+=== Timing constraints ===
+Timing constraints in ACT are specified using [[asic:timing:forks|timing forks]]. Timing forks are used to specify a point of divergence relative timing constraint. The constraint
+<code act>
+spec {
+  timing a+ : b- < c+
+}
+</code>
+states that after ''a'' makes a zero-to-one transition, ''b'' makes a one-to-zero transition //before// ''c'' makes a zero-to-one transition. ''a+'' is the //root// of the timing fork, ''b-'' is the //fast// leg of the fork, and ''c+'' is the slow leg of the fork.
+<code act>
+spec {
+  timing a+ : b- < [15] c+
+}
+</code>
+This specifies that the timing fork has a margin of 15 delay units. The conversion from delay units to actual time uses the ''prs2net.conf'' [[config:netlist#Device generation and parameters|configuration parameter]] ''net.delay''.
+If a circuit violates a timing fork, that is an error that is flagged by the ACT simulation tools. During the implementation flow, these timing forks have to be checked. If they are violated, then the circuit must be adjusted to ensure that they are satisfied. There are two ways to satisfy a fork: (i) make the slow path faster; or (ii) make the fast path slower. Adding delays to a fast path is one way to satisfy a timing fork, but that may result in slowing down the circuit. Hence, the default optimizations will attempt to make the slow path faster.
+In some cases, a user may want the circuit synthesis and optimization tools to insert the appropriately sized delay line to make the fast path slower. In other words, rather than manually specifying the delay line, a timing fork can be specified where the implementation flow should just add the appropriately sized, technology-dependent delay line. In such cases, a timing fork can be specified as follows:
+<code act>
+spec {
+  timing a+ : b- << [15] c+
+}
+</code>
+This has the same meaning as the earlier fork, except that the tools are provided with a hint that says that it is okay to add delays to correct any violations of this fork.
+Finally, timing forks may relate transitions from adjacent iterations.
+<code act>
+spec {
+  timing a+ : b*- < c+
+}
+</code>
+The ''*'' indicates that the ''b-'' transition is from the following iteration. The ''*'' indicator can appear on any signal except the root of the timing fork (in this case ''a+'').
+When computing conservative approximations to timing graphs, ACT may add extra edges to the timing graph that are in fact not present in the true timing graph for the system. This can occur, for example, when a gate is modified to incorporate extra signals to simplify the circuit implementation but the new input has no bearing on event causality in the asynchronous circuit. If the automated timing graph construction algorithm includes such edges, they can be explicitly deleted using the following directive:
+<code act>
+spec {
+   timing a- #> c+
+ }
+</code>
+This directive says that the ''a-''  to ''c+'' edge should be deleted from the timing graph.