Automated reasoning of inductive theorems is considered important in program verification. To verify inductive theorems automatically, several implicit induction methods like the inductionless induction and the rewriting induction methods have been proposed. In studying inductive theorems on higher-order rewritings, we found that the class of the theorems shown by known implicit induction methods does not coincide with that of inductive theorems, and the gap between them is a barrier in developing mechanized methods for disproving inductive theorems. This paper fills this gap by introducing the notion of primitive inductive theorems, and clarifying the relation between inductive theorems and primitive inductive theorems. Based on this relation, we achieve mechanized methods for proving and disproving inductive theorems.

In this paper, an eight-legged resonant element is proposed for a multiband and dual-polarized frequency selective surface (FSS). The FSS element has two resonant frequencies for constructing two reflection bands, of which the separation can be easily controlled by adjusting the shape of the element. The flexibility is demonstrated by the simulated results of transmission responses for various geometrical parameters. And it is shown that introducing resonant-grid and closely-packing techniques can improve the reflection bandwidth. Finally, the good agreement between the measured and the calculated results proves that the eight-legged element is useful for the design of a multiband FSS.

In this letter, a new channel-adaptive beamforming method is proposed for OFDMA systems with smart antennas. In the method, the size of a cluster for resource unit is determined adaptively according to a region-splitting criterion. It is shown by simulations that the proposed method shows good performance in both frequency-flat and frequency-selective channels.

It has been observed in the literature that the characteristic polynomial of a discrete system can be computed from the characteristic impulse response Gramian. In this letter it is shown that a given characteristic impulse response Gramian, in fact, contains information on two characteristic polynomials. The importance of this result is illustrated through an application to model reduction of discrete systems.

This paper presents a frequency-controllable image rejection mixer in heterodyne architecture for 2 GHz applications based on TSMC 0.18 µm CMOS technology. The designed mixer uses a notch filter to suppress the image signal and allows precise tuning the image frequencies. An image rejection of 20-70 dB is obtained in a 200 MHz of bandwidth. The simulation results show single-side band (SSB) NF is improved 3.7 dB, the voltage conversion gain of 14.7 dB, improved by more than 4 dB. The circuit operates at the supply voltage of 1.8 V, and dissipates 11.34 mW.

An order selection scheme for two-sided oblique projection-based interconnect reduction will be investigated. It will provide a guideline for terminating the conventional nonsymmetric Pade via Lanczos (PVL) iteration process. By exploring the relationship of the system Grammians of the original network and those of the reduced network, it can be shown that the system matrix of the reduced-order system generated by the two-sided oblique projection can also be expressed as those of the original interconnect model with some additive perturbations. The perturbation matrix only involves bi-orthogonal vectors at the previous step of the nonsymmetric Lanczos algorithm. This perturbation matrix will provide the stopping criteria in the order selection scheme and achieve the desired accuracy of the approximate transfer function.

The security of SHA-0 with various message schedules is discussed in this letter. SHA-0 employs a primitive polynomial of degree 16 over GF(2) in its message schedule. For each primitive polynomial, a SHA-0 variant can be constructed. The collision resistance and the near-collision resistance of SHA-0 variants to the Chabaud-Joux attack are evaluated. Moreover, the near-collision resistance of a variant to the Biham-Chen attack is evaluated. It is shown that the selection of primitive polynomials highly affects the resistance. However, it is concluded that these SHA-0 variants are not appropriate for making SHA-0 secure.

In [1], an algorithm based on phase variations of received pilot symbols was proposed to estimate one of the most important channel parameters, maximum Doppler shift, fd. However, AWGN (Additive white gauss noise) will cause large estimation error in some cases. In order to analyze the influence of noise, we extended the phase probability density function (pdf) in [1] to the scenario with both fading and AWGN, then the estimation error is characterized in closed-form expression. By this error expression, we found that power control will affect the estimator of [1] and we proposed a modification method based on SNR estimation to obtain accurate Doppler shift estimation in moderate low SNRs (signal-to-noise ratio). Simulation results show high accuracy in wide range of velocities and SNRs.

This paper shows a design method for a sequential circuit by using a Look-Up Table (LUT) ring. The method consists of two steps: The first step partitions the outputs into groups. The second step realizes them by LUT cascades, and allocates the cells of the cascades into the memory. The system automatically finds a fast implementation by maximally utilizing available memory. With the presented algorithm, we can easily design sequential circuits satisfying given specifications. The paper also compares the LUT ring with logic simulator to realize sequential circuits: the LUT ring is 25 to 237 times faster than a logic simulator that uses the same amount of memory.

Simple closed-form expressions for efficiently calculating on-chip interconnect capacitances are presented. The formulas are expressed with second-order polynomial functions which do not include exponential functions. The runtime of the proposed formulas is about 2-10 times faster than those of existing formulas. The root mean square (RMS) errors of the proposed formulas are within 1.5%, 1.3%, 3.1%, and 4.6% of the results obtained by a field solver for structures with one line above a ground plane, one line between ground planes, three lines above a ground plane, and three lines between ground planes, respectively. The proposed formulas are also superior in accuracy to existing formulas.

By inserting a slot and metallic strips at the widened stub in a single layer and fed by coplanar waveguide (CPW) transmission line, novel dual-band and broadband operations are presented. The proposed antennas are designed to have dual-band operation suitable for applications in DCS (1720-1880 MHz), PCS (1850-1990 MHz), IMT-2000 (1920-2170 MHz), and IEEE 802.11 WLAN standards in the 2.4 GHz (2400-2484 MHz) and 5.2 GHz (5150-5350 MHz) bands. The dual-band antennas are simple in design, and the two operating modes of the proposed antennas are associated with perimeter of slots and loading metallic strips, in which the lower operating band can be controlled by varying the perimeters of the outer square slot and the higher band depend on the inner slot of the widened stub. The experimental results of the proposed antennas show the impedance bandwidths of the two operating bands, determined from 10-dB return loss, larger than 61% and 27% of the center frequencies, respectively.

In deep submicron designs, predicting gate slews and delays for interconnect loads is vitally important for Static Timing Analysis (STA). The effective capacitance Ceff concept is usually used to calculate the gate delay of interconnect loads. Many Ceff algorithms have been proposed to compute gate delay of interconnect loads. However, less work has been done to develop a Ceff algorithm which can accurately predict gate slew. In this paper, we propose a novel method for calculating the Ceff of interconnect load for gate slew. We firstly establish a new expression for Ceff in 0.8Vdd point. Then the Integration Approximation method is used to calculate the value of Ceff in 0.8Vdd point. In this method, the integration of a complicated nonlinear gate output is approximated with that of a piecewise linear waveform. Based on the value of Ceff in 0.8Vdd point, Ceff of interconnect load for gate slew is obtained. The simulation results demonstrate a significant improvement in accuracy.

This paper proposes a novel cache architecture for low power consumption, called "Adaptive Way-Predicting Cache (AWP cache)." The AWP cache has multi-operation modes and dynamically adapts the operation mode based on the accuracy of way-prediction results. A confidence counter for way prediction is implemented to each cache set. In order to analyze the effectiveness of the AWP cache, we perform a SRAM design using 0.18 µm CMOS technology and cycle-accurate processor simulations. As the results, for a benchmark program (179.art), it is observed that a performance-aware AWP cache reduces the 49% of performance overhead caused by an original way-predicting cache to 17%. Furthermore, a energy-aware AWP cache achieves 73% of energy reduction, whereas that obtained from the original way-predicting scheme is only 38%, compared to an non-optimized conventional cache. For the consideration of energy-performance efficiency, we see that the energy-aware AWP cache produces better results; the energy-delay product of conventional organization is reduced to only 35% in average which is 6% better than the original way-predicting scheme.

Design of portable battery operated multimedia devices requires energy-efficient multiplication circuits. This paper proposes a novel architectural technique to reduce power consumption of digital multipliers. Unlike related approaches which focus on multiplier transition activity reduction, we concentrate on dynamic reduction of supply voltage. Two implementation schemes capable of dynamically adjusting a double voltage supply to input data variation are presented. Simulations show that using these schemes we can reduce energy consumption of 1616-bit multiplier by 34% and 29% on peak and by 10% and 7% on average with area overhead of 15% and 4%, respectively, while maintaining the performance of traditional multiplier.

Interconnect Length Distribution (ILD) represents the correlation between the number of interconnects and their length. The ILD can predict power consumption, clock frequency, chip size, etc. High core utilization and small circuit area have been reported to improve chip performance. We propose an ILD model to predict the correlation between core utilization and chip performance. The proposed model predicts the influences of interconnect length and interconnect density on circuit performances. As core utilization increases, small and simple circuits improve the performances. In large complex circuits, decreasing the wire coupling capacitance is more important than decreasing the total interconnect length for improvement of chip performance. The proposed ILD model expresses the actual ILD more accurately than conventional models.

In order to eliminate the co-channel and multi-path interference of quasi-synchronous code division multiple access (QS-CDMA) systems, spreading sequences with low or zero correlation zone (LCZ or ZCZ) can be used. The significance of LCZ/ZCZ to QS-CDMA systems is that, even there are relative delays between the transmitted spreading sequences due to the inaccurate access synchronization and the multipath propagation, the orthogonality (or quasi-orthogonality) between the transmitted signals can still be maintained, as long as the relative delay does not exceed certain limit. In this paper, several lower bounds on the aperiodic autocorrelation and crosscorrelation of binary LCZ/ZCZ sequence set with respect to the family size, sequence length and the aperiodic low or zero correlation zone, are derived. The results show that the new bounds are tighter than previous bounds for the LCZ/ZCZ sequences.

The authors propose the simple and efficient method based on the shooting and bouncing rays (SBR) method in order to evaluate multi-reflection effects inside a radome. In this paper, we show the analysis procedure of the proposed method. Next, we compare calculated data with some measured data in order to verify the proposed method. We confirmed that the proposed method is effective for the objects with radome except the areas where strong edge diffraction appears.

Locality in high frequency diffraction is embodied in the Method of Moments (MoM) in view of the method of stationary phase. Local-domain basis functions accompanied with the phase detour, which are not entire domain but are much larger than the segment length in the usual MoM, are newly introduced to enhance the cancellation of mutual coupling over the local-domain; the off-diagonal elements in resultant reaction matrix evanesce rapidly. The Fresnel zone threshold is proposed for simple and effective truncation of the matrix into the sparse band matrix. Numerical examples for the 2-D strip and the 2-D corner reflector demonstrate the feasibility as well as difficulties of the concept; the way mitigating computational load of the MoM in high frequency problems is suggested.

A high quality-factor of active inductor has been implemented by using the 0.18 µm 1P6M CMOS technologies in this work. By adding a feedback resistance and a regulated gain stage transistor into the conventional cascade-grounded approach, the quality-factor and performance of CMOS active inductor can be improved. This novel active inductor demonstrated a maximum quality-factor of 540 and a 3.2 nH inductance at 4.3 GHz, where the self-resonant frequency was 5.4 GHz. An active CMOS bandpass filter was also fabricated including this tunable high quality factor active inductor, performing an insertion loss of 0.2 dB and a return loss more than 32 dB with a tuning range from 3.45 GHz to 3.6 GHz. The input IP3 was -2.4 dBm, and the noise figure was 14.1 dB with a 28 mW dc power consumption.

In this paper, we propose a method for detecting and tracking faces in video sequences in real time. It can be applied to a wide range of face scales. Our basic strategy for detection is fast extraction of face candidates with a Six-Segmented Rectangular (SSR) filter and face verification by a support vector machine. A motion cue is used in a simple way to avoid picking up false candidates in the background. In face tracking, the patterns of between-the-eyes are tracked while updating the matching template. To cope with various scales of faces, we use a series of approximately 1/ scale-down images, and an appropriate scale is selected according to the distance between the eyes. We tested our algorithm on 7146 video frames of a news broadcast featuring sign language at 320240 frame size, in which one or two persons appeared. Although gesturing hands often hid faces and interrupted tracking, 89% of faces were correctly tracked. We implemented the system on a PC with a Xeon 2.2-GHz CPU, running at 15 frames/second without any special hardware.