Formal verification has become an increasing prominent technique towards establishing the correctness of hardware designs. We present a framework to specifying and verifying the design of systolic architectures. Our approach allows users to represent systolic arrays in Z specification language and to justify the design semi-automatically using the verifier. Z is a notation based on typed set theory and enriched by a schema calculus. We describe how a systolic array for matrix-vector multiplication can be specified and justified with respect to its algorithm.

This paper presents an optimal constraint graph generation algorithm for graph-based one-dimensional layout compaction. The first published algorithm for this problem was the shadow-propagation algorithm. However, without sophisticated implementation of a shadow-front, complexity of the algorithm could fall into O(n²), where n is the number of layout objects. Although our algorithm, called the enhanced plane-sweep based graph generation algorithm, is an extension of the shadow-propagation algorithm, such a drawback is resolved by introducing an enhanced plane-sweep technique. The algorithm maintains multiple shadow-fronts simultaneously by storing them in a work-list called previous-boundary. Since a balanced search tree is selected for implementation of the worklist, total complexity of the algorithm is O(n log n) which is optimal. Experimental results show that the enhanced plane-sweep based graph generation algorithm runs in almost linear time with respect to the number of layout objects and is faster than the perpendicular plane-sweep algorithm which is also optimal in terms of time complexity.

In this paper, we propose an algorithm of O(|V|min{k,|V|,|A|}|A|) time complexity for finding all k-edge-connected components of a given digraph D=(V,A) and a positive integer k. When D is symmetric, incorporating a preprocessing reduces this time complexity to O(|A|+|V|²+|V|min{k,|V|}min{k|V|,|A|}), which is at most O(|A|+k²|V|²).

The subject of the paper is to propose an O(|V|+|E|) algorithm for the 3-edge-connectivity augmentation problem (UW-3-ECA) defined by "Given an undirected graph G₀=(V,E), find an edge set E of minimum cardinality such that the graph (V,EE ) (denoted as G₀+E ) is 3-edge-connected, where each edge of E connects distinct vertices of V." Such a set E is called a solution to the problem. Let UW-3-ECA(S) (UW-3-ECA(M), respectively) denote UW-3-ECA in which G₀+E is required to be simple (G₀+E may have multiple edges). Note that we can assume that G₀ is simple in UW-3-ECA(S). UW-3-ECA(M) is divided into two subproblems (1) and (2) as follows: (1) finding all k-edge-connected components of a given graph for every k3, and (2) determining a minimum set of edges whose addition to G₀ result in a 3-edge-connected graph. Concerning the subproblem (1), we use an O(|V|+|E|) algorithm that has already been existing. The paper proposes an O(|V|+|E|) algorithm for the subproblem (2). Combining these algorithms makes an O(|V|+|E|) algorithm for finding a solution to UW-3-ECA(M). Furthermore, it is shown that a solution E to UW-3-ECA(M) is also a solution to UW-3-ECA(S) if |V|4, partly solving an open problem UW-k-ECA(S) that is a generalization of UW-3-ECA(S).

In this paper, we discuss secure protocols for shared computation of algorithms associated with digital signature schemes based on discrete logarithms. Generic solutions to the problem of cooperatively computing arbitraty functions, though formally provable according to strict security notions, are inefficient in terms of communication--bits and rounds of interaction--; practical protocols for shared computation of particular functions, on the other hand, are often shown secure according to weaker notions of security. We propose efficient secure protocols to share the generation of keys and signatures in the digital signature schemes introduced by Schnorr (1989) and ElGamal (1985). The protocols are built on a protocol for non-interactive verifiable secret sharing (Feldman, 1987) and a novel construction for non-interactively multiplying secretly shared values. Together with the non-interactive protocols for shared generation of RSA signatures introduced by Desmedt and Frankel (1991), the results presented here show that practical signature schemes can be efficiently shared.

In this paper, we consider a class of the languages that have (constant round) perfect zero-knowledge interactive proofs without assuming any complexity assumptions. Especially, we investigate the interactive protocol with the restricted prover who runs in probabilistic polynomial time and knows the complete factorization as a trapdoor information of the integer associated with the input. We give a condition of the existence of constant round perfect zero-knowledge interactive proofs without assuming any complexity assumptions. The bit commitment based on the quadratic residuosity has an important role in our protocol and the simulation is based on the technique developed by Bellare, Micali, and Ostrovsky in Ref. (9), so call double running process. However, the proof of perfect zero-knowledgeness needs a more powerful simulation technique. Our simulation extracts more knowledge, the complete factorization of the integer associated with the input, from a (cheating) verifier than Bellare-Micali-Ostrovsky's simulation does. Furthermore, our main result implies that Blum integer has a five move perfect zero-knowledge interactive proof without assuming any complexity assumptions. (All previous known zero-knowledge protocols for Blum integer required either unproven cryptographic assumptions or unbounded number of rounds of message exchange.)

An algorithm is presented to evaluate terminal pair reliability for complex systems. he approach is an extension of the minimal path set concept for non-target nodes, and uses the concept of disjoint branch sets. By means of disjoint branch set techniques, the partial disjoint features of subpaths (i.e., part of a path is disjoint to the rest of the path) are used to reduce the number of path intersections in the calculation of the system reliability.

This paper focuses on methodology underlying the application to fault tolerant computer systems with "no down communication" capability of stochastic Petri nets with general firing times. Based on a formal specification of the stochastic Petri net, we provide criteria for the marking process to be a regenerative process in continuous time with finite cycle-length moments. These results lead to strongly consistent point estimates and asymptotic confidence intervals for limiting system availability indices. We also show how the building blocks of stochastic Petri nets with general firing times facilitate the modeling of non-deterministic transition firing and illustrate the use of "interrupter input places" for graphical representation of transition interruptions.

Periodic schedules are seldom treated in the theory but abound in practice (air flight schedule, train schedule, manufacturing schedule, etc). This paper introduces a Petri Net based perspective to periodic schedules. These are classified, according to the time interpretation into single-server and multiple-server semantics and, according to transitions firing periodicity constraints, into strict and general periodic schedules. Using a net transformation rule, the computation of the general schedule class can be done through techniques for the strict subclass. Introducing truncation error terms ε for the floor functions, a necessary and sufficient condition for the feasibility of a strict periodic schedule is given in terms of a large size system of nonlinear inequalities containing ε terms. Moreover averaging this condition on subperiods allows to get a small size linear system of inequalities as necessary conditions for speeding up iterative computation processes. This paper aims to present qualitative analysis of periodic schedules for deterministically timed Petri net systems, as a precursor to quantitative analysis that requires large-scale computational experiments and hence will be dealt in later work.

This paper deals with the theory and design method of an efficient radix-4 divider using carry-propagation-free adders based on redundant binary {-1,0,+1} representation. The usual method of normalizing the divisor in the range [1/2,1) eliminates the advantages of using a higher radix than two, bacause many digits of the partial remainder are required to select the quotient digits. In the radix-4 case, it is shown that it is possible to select the quotient digits to refer to only the four (in the usual normalizing method it is seven) most significant digits of the partial remainder, by scaling the divisor in the range [12/8,13/8). This leads to radix-4 dividers more effective than radix-2 ones. We use the hyperstring graph representation proposed in Ref.(18) for redundant binary adders.

This paper studies a method for a parallel implementation of digital half toning technique, which converts continuous tone images into monotone one without losing fidelity of images. A new modified algorithm for half toning is proposed, which is able to be implemented on a rectangular or one dimensional parallel multi-processor array as a part of extensions of space partitioning image processings. The purpose of this paper is primarily to apply space partitioning local image processing technique to nonlinear recursive algorithms. The target is to achieve a fast half toning with high quality. For that propose, local directional error diffusion techniques will be introduced, which enable original recursive error diffusion half toning to be converted into a local processing algorithm without losing its original advantages of producing high quality images. The characteristics of proposed methods will be analyzed and the advantages of our algorithm of high speed processing and high quality will be demonstrated by showing the results of simulations for typical examples.

The authors recently proposed a design method of stable IIR digital filters based on the interpolation by rational characteristic functions of filters, for a set of values of these characteristic function and, in addition, their higher derivatives prescribed at a number of frequency. This method can be further extended so that, despite usage of a less number of interpolation points, almost the same filter characteristics as one obtained by the former method can be realized. This paper presents an improved design method for making the transfer function meet strict magnitude specifications. The method proposed in this paper is especially efficient for designing a filter whose characteristics is specified not only in the passband but also in the transition band with relatively narrow bandwidth.

We propose a design method for a two-channel perfect reconstruction FIR filter banks employing linear-phase filters. This type of filter bank is especially important in splitting image signals into frequency bands for subband image cording. Because in such an application, it is necessary to use the combination of linear-phase filters and symmetric image signal, namely linear phase signal to avoid the increase in image size caused by filtering. In this paper, first we summarize the design conditions for two-channel filter banks. Next, we show that the design problem is reduced to a very simple linear equation, by using a half-band filter as a lowpass filter. Also the proposed method is available to lead filters with fewer complexity, which enable us to use simple arithmetic operations. For subband coding, the property is important because it reduces hardware complexity.

This paper describes the novel relaxation-based algorithm for the harmonic analysis of nonlinear circuits. First, we present Iterated Spectrum Analysis based on harmonic balance method, where the harmonic balance method is applied to every node independently. As a result, we can avoid dealing with large scale Jacobian matrices and reduce the total simulation time, compared with the conventional method based on Galerkin's procedure or the harmonic balance method. Next, we define the frequency domain latency. Furthermore, we refer to the possibility for exploitation of three types of latency, i.e., relaxation iteration latency, frequency domain latency and Newton iteration latency. And we propose the multirate-sampling technique based on the consideration of the frequency domain latency. Finally, we apply the present technique to the simple analog circuit simulation and verify its availability for the harmonic analysis.

In this work, we introduce a fuzzy inference in conventional backpropagation learning algorithm, for networks of neuron like units. This procedure repeatedly adjusts the learning parameters and leads the system to converge at the earliest possible time. This technique is appropriate in a sense that optimum learning parameters are being applied in every learning cycle automatically, whereas the conventional backpropagation doesn't contain any well-defined rule regarding the proper determination of the value of learning parameters.

The three layer neural network (TLNN) is treated, where the nonlinearity of a neuron is of signum. First we propose an expression of the discriminant function of the TLNN, which is called a linear-homogeneous expression. This expression allows the differentiation in spite of the signum property of the neuron. Subsequently a learning algorithm is proposed based on the linear-homogeneous form. The algorithm is an error-correction procedure, which gives a mathematical foundation to heuristic error-correction learnings described in various literatures.

A model of a single neuron with chaotic dynamics is implemented with current-mode circuit design technique. The existence of chaotic dynamics in the circuit is demonstrated by simulation with SPICE3. The proposed circuit is suitable for implementing a chaotic neural network composed of such neuron models on a VLSI chip.

A speech analysis/synthesis system that relies on a time-varying Auto Regressive Moving Average (ARMA) process and the Short-Time Fourier Transform (STFT) is proposed. The narrowband components in speech are represented in the frequency domain by a set of harmonic components, while the broadband random components are represented by a time-varying ARMA process. The time-varying ARMA model has a dual function, namely, it creates a spectral envelope that fits accurately the harmonic STFT components, and provides for the spectral representation of the broadband components of speech. The proposed model essentially combines the features of waveform coders by employing the STFT and the features of traditional vocoders by incorporating an appropriately shaped noise sequence.

In formulating the motion constraint equation, we implicitly take it for granted that the spatial and temporal sampling intervals are very small. In real situations, since the intervals cannot be considered sufficiently small, an error will be introduced into the constraint equation and consequently the velocity estimate will be subject to an error due to inaccuracy of the constraint equation. We perform some experiments to analyze the effect of sampling interval on motion estimation. The understanding of experimental results will provide an insight into necessity and amount of image filtering prior to the application of motion estimation.

This paper describes a novel but simple method of implementing waveform relaxation technique for bipolar circuits involving ECL gates. This method performs gate level partitioning of ECL circuits not only during the cutoff state of the input transistor but also when the input transistor is in its active state. Partitioning at all times has become possible due to the favorable property of input and output stages of ECL gates. It is shown that this method is faster than direct method even when the circuits containing only few gates is simulated. Further, it is shown that the present method is applicable to the case where the interconnections between the ECL gates is treated as lossy transmission lines.

Gradient-based methods for the computation of the velocity from image sequences assume that the velocity field varies smoothly over image. This creates difficulties at regions where the image intensity changes abruptly such as the occluding contours or region boundaries. In this letter, we propose a method to overcome these difficulties by incorporating the information of discontinuities in image intensity into a standard local optimization method. The presented method is applied to the synthetic and real images. The results show that the velocity field computed by the proposed method is less blurred at region boundaries than that of the standard method.