Optimization of linear max-plus systems with application to timing analysis

This work provides a joint solution to two different problems--the temporal verification of hardware interface logic, and the solution and optimization of linear max-plus systems.; The interface timing verification problem seeks to determine the maximum time separations possible among the input and output signal changes of two or more interconnected hardware modules. These possible separations are then compared against the time separations allowed by the hardware modules' communication protocols. We present here the ShortCircuit algorithm, which is the first correct algorithm for this problem. In addition, we discuss the difficulties inherent in solving the interface hardware timing synthesis problem, which asks us to choose time separations between signal transitions to ensure that the timing requirements of all hardware modules' communication protocols are met.; The ShortCircuit algorithm leads to the first reasonable method for solving arbitrarily sized systems in the linear max-plus algebra. The linear max-plus algebra is similar to the familiar linear algebra except that the binary maximum and scalar addition operations take the place of addition and scalar multiplication.; The linear max-plus system solution employs an iterative technique in which the system is re-phrased with a system of simpler constraints. Maximum solutions to special subsets of these constraints are then found using the max-plus matrix closure operation. Each such maximum solution bounds the system's maximum solution from above, and guides the search for a new subset which yields a tighter bound on the system's solution. The technique is easily extended to maximize and minimize linear max-plus expressions over a linear max-plus system and is thus the max-plus analogue of linear programming.; While the practical motivation and examples discussed in this work are drawn from the realm of hardware interface logic, the solutions provided apply to any system of events whose temporal relationships can be described as a combination of two primitives: synchronization and bounded delay. An event synchronizes a set of events if it occurs immediately after all events of the set have occurred. Two events have a bounded delay relationship if one always happens within a specified bounded time interval after the other.