In this paper we propose a method of formal verification of totally self-checking (TSC) properties of combinational circuits using logic function manipulation. We show that the problem of verification of TSC properties can be transformed to a satisfiability problem of decision functions formed from characteristic functions of a circuit's output code words. Then the problem can be solved using binary decision diagrams (BDD). Experimental results show the effectiveness of the proposed method.

This paper proposes a fully self-timing data-bus (FSD) architecture which includes a dual data-bus driven by the read-out data itself and a complementary output differential (COD) amplifier. The proposed COD amplifier achieves a high voltage gain and a high speed data transfer with low power consumption. The read-out data is transmitted from the COD amplifier to the output terminal without the timing control caused by the fluctuation of the device parameters. Therefore the proposed FSD architecture eliminates the timing delay and achieves a timing-free data transfer even in DRAMs with a small signal level at the sense amplifier and the data line. Applying this architecture to a 64-Mb DRAM, a fast column address access time of 16 ns and a RAS access time of 32 ns have been achieved.

Kalman filter is an essential tool in signal processing, modern control and communications. The filter estimates the states of a given system from noisy measurements, using a mean-square error criterion. Although Kalman filter has been shown to be very versatile, it has always been computationally intensive since a great number of matrix computations must be performed at each iteration. Thus the exploitation of this technique in broadband real time applications is restricted. The solution to these limitations appears to be in VLSI (very large scale integration) architectures for the parallel processing of data, in the form of systolic architectures. Systolic arrays are networks of simple processing cells connected only to their nearest neighbors. Each cell consists of some simple logic and has a small amount of local memory. Overall data flows through the array are synchronously controlled by a single main clock pulse. In parallel with the development of Kalman filter, the square root covariance and the square root information methods have been studied in the past. These square root methods are reported to be more accurate, stable and efficient than the original algorithm presented by Kalman. However it is known that standard SRIF is less efficient than the other algorithms, simply because standard SRIF has additional matrix inversion computation and matrix multiplication which are difficult to implement in terms of speed and accuracy. To solve this problem, we use the modified Faddeeva algorithm in computing matrix inversion and matrix multiplication. The proposed algorithm avoids the direct matrix inversion computation and matrix multiplication, and performs these matrix manipulations by Gauss elimination. To evaluate the proposed method, we constructed an efficient systolic architecture for standard SRIF using the COMPASS design tools. Actual VLSI design and its simulation are done on the circuits of four type processors that perform Gauss elimination and the modified Givens rotation.