This paper presents an automatic hierarchical formal verification method for arithmetic circuits over Galois fields (GFs) which are dedicated digital circuits for GF arithmetic operations used in cryptographic processors. The proposed verification method is based on a combination of a word-level computer algebra procedure with a bit-level PPRM (Positive Polarity Reed-Muller) expansion procedure. While the application of the proposed verification method is not limited to cryptographic processors, these processors are our important targets because complicated implementation techniques, such as field conversions, are frequently used for side-channel resistant, compact and low power design. In the proposed method, the correctness of entire datapath is verified over GF(2m) level, or word-level. A datapath implementation is represented hierarchically as a set of components' functional descriptions over GF(2m) and their wiring connections. We verify that the implementation satisfies a given total-functional specification over GF(2m), by using an automatic algebraic method based on the Gröbner basis and a polynomial reduction. Then, in order to verify whether each component circuit is correctly implemented by combination of GF(2) operations, i.e. logic gates in bit-level, we use our fast PPRM expansion procedure which is customized for handling large-scale Boolean expressions with many variables. We have applied the proposed method to a complicated AES (Advanced Encryption Standard) circuit with a masking countermeasure against side-channel attack. The results show that the proposed method can verify such practical circuit automatically within 4 minutes, while any single conventional verification methods fail within a day or even more.

To use millimeter wave bands in future cellular and outdoor wireless networks, understanding the multipath cluster characteristics such as delay and angular spread for different polarization is very important besides knowing the path loss and other large scale propagation parameters. This paper presents result from analysis of wide-band full polarimetric double directional channel measurement at the millimeter wave band in a typical urban pico-cell environment. Only limited number of multipath clusters with gains ranging from -8dB to -26.8dB below the free space path loss and mainly due to single reflection, double reflection and diffraction, under both line of sight (LOS) and obstructed LOS conditions are seen. The cluster gain and scattering intensity showed strong dependence on polarization. The scattering intensities for ϑ-ϑ polarization were seen to be stronger compared to ϕ-ϕ polarization and on average 6.1dB, 5.6dB and 4.5dB higher for clusters due to single reflection, double reflection and scattering respectively. In each cluster, the paths are highly concentrated in the delay domain with delay spread comparable to the delay resolution of 2.5ns irrespective of polarization. Unlike the scattering intensity, the angular spread of paths in each cluster did not show dependence on polarization. On the base station side, average angular spread in azimuth and in elevation were almost similar with ≤3.3° spread in azimuth and ≤3.2° spread in elevation for ϑ-ϑ polarization. These spreads were slightly smaller than those observed for ϕ-ϕ polarization. On the mobile station side the angular spread in azimuth was much higher compared to the base station side. On average, azimuth angular spread of ≤11.4° and elevation angular spread of ≤5° are observed for ϑ-ϑ polarization. These spreads were slightly larger than in ϕ-ϕ polarization. Knowing these characteristics will be vital for more accurate modeling of the channel, and in system and antenna design.

Previously, it is not obvious to what extent was accepted for the assessors when we see the 3D image (including multi-view 3D) which the luminance change may affect the stereoscopic effect and assessment generally. We think that we can conduct a general evaluation, along with a subjective evaluation, of the luminance component using both the S-CIELAB color space and CIEDE2000. In this study, first, we performed three types of subjective evaluation experiments for contrast enhancement in an image by using the eight viewpoints parallax barrier method. Next, we analyzed the results statistically by using a support vector machine (SVM). Further, we objectively evaluated the luminance value measurement by using CIEDE2000 in the S-CIELAB color space. Then, we checked whether the objective evaluation value was related to the subjective evaluation value. From results, we were able to see the characteristic relationship between subjective assessment and objective assessment.

Decentralized channel assignment schemes are proposed to obtain low system-wide spatial overlap regions in wireless local area networks (WLANs). The important point of channel assignment in WLANs is selecting channels with fewer contending stations rather than mitigating interference power due to its medium access control mechanism. This paper designs two potential game-based channel selection schemes, basically each access point (AP) selects a channel with smaller spatial overlaps with other APs. Owing to the property of potential games, each decentralized channel assignment is guaranteed to converge to a Nash equilibrium. In order that each AP selects a channel with smaller overlaps, two metrics are proposed: general overlap-based scheme yields the largest overlap reduction if a sufficient number of stations (STAs) to detect overlaps are available; whereas decomposed overlap-based scheme need not require such STAs, while the performance would be degraded due to the shadowing effect. In addition, the system-wide overlap area is analytically shown to be upper bounded by the negative potential functions, which derives the condition that local overlap reduction by each AP leads to system-wide overlap reduction. The simulation results confirm that the proposed schemes perform better reductions in the system-wide overlap area compared to the conventional interference power-based scheme under the spatially correlated shadowing effect. The experimental results demonstrate that the channel assignment dynamics converge to stable equilibria even in a real environment, particularly when uncontrollable APs exist.

Locally repairable codes have recently been applied in distributed storage systems because of their excellent local erasure-correction capability. A locally repairable code is a code with locality r, where each code symbol can be recovered by accessing at most r other code symbols. In this paper, we study the existence and construction of binary cyclic codes with locality 2. An overview of best binary cyclic LRCs with length 7≤n≤87 and locality 2 are summarized here.

This paper proposes 0-1-A-Ā LUT, a new programmable logic using atom switches, and a delay-optimal mapping algorithm for it. Atom switch is a non-volatile memory device of very small geometry which is fabricated between metal layers of a VLSI, and it can be used as a switch device of very small on-resistance and parasitic capacitance. While considerable area reduction of Look Up Tables (LUTs) used in conventional Field Programmable Gate Arrays (FPGAs) has been achieved by simply replacing each SRAM element with a memory element using a pair of atom switches, our 0-1-A-Ā LUT achieves further area and delay reduction. Unlike the conventional atom-switch-based LUT in which all k input signals are fed to a MUX, one of input signals is fed to the switch array, resulting area reduction due to the reduced number of inputs of the MUX from 2k to 2k-1, as well as delay reduction due to reduced fanout load of the input buffers. Since the fanout of this input buffers depends on the mapped logic function, this paper also proposes technology mapping algorithms to select logic function of fewer number of fanouts of input buffers to achieve further delay reduction. From our experiments, the circuit delay using our k-LUT is 0.94% smaller in the best case compared with using the conventional atom-switch-based k-LUT.

Linear phase maximally flat digital differentiators (DDs) with stopbands obtained by minimizing the Lp norm are filters with important practical applications, as they can differentiate input signals without distortion. Stopbands designed by minimizing the Lp norm can be used to control the relationship between the steepness in the transition band and the ripple scale. However, linear phase DDs are unsuitable for real-time processing because each group delay is half of the filter order. In this paper, we proposed a design method for a low-delay maximally flat low-pass/band-pass FIR DDs with stopbands obtained by minimizing the Lp norm. The proposed DDs have low-delay characteristics that approximate the linear phase characteristics only in the passband. The proposed transfer function is composed of two functions, one with flat characteristics in the passband and one that ensures the transfer function has Lp approximated characteristics in the stopband. In the optimization of the latter function, Newton's method is employed.

In this paper, a novel fusion center controlled media access control (MAC) protocol for physical wireless parameter conversion sensor networks (PHY-C SN), and a transmission power design for each sensor node are proposed. In PHY-C SN, the sensing information is converted to corresponding subcarrier number of orthogonal frequency division multiplexing (OFDM) signals, and all sensor nodes can send sensing information simultaneously. In most wireless sensor network standards, each sensor node detects the surrounding wireless signal through carrier sense. However, sensor nodes cannot send signals simultaneously if carrier sense is applied in PHY-C SN. Therefore, a protocol for PHY-C SN is devised. In the proposed protocol, the fusion center detects the surrounding wireless environment by carrier sense and requests sensing information transmission toward sensor nodes if no other wireless systems are detected. Once the sensor nodes receive the request signal, they transmit sensing information to the fusion center. Further, to avoid harmful interference with surrounding wireless systems, the transmission power of each sensor is designed to suit the considering communication range and avoid interference toward other wireless systems. The effectiveness of the proposed protocol is evaluated by computer simulation. The parameters for collection like the number of collecting sensor nodes and the radius of the collection area are also examined when determining the transmission power of sensor nodes. Results show that highly efficient information collection with reducing interference both from and towards surrounding wireless systems can be implemented with PHY-C SN.

This paper explores the potential of orbital angular momentum (OAM) multiplexing as a means to enable high-speed wireless transmission. OAM is a physical property of electro-magnetic waves that are characterized by a helical phase front in the propagation direction. Since the characteristic can be used to create multiple orthogonal channels, wireless transmission using OAM can enhance the wireless transmission rate. Comparisons with other wireless transmission technologies clarify that OAM multiplexing is particularly promising for point-to-point wireless transmission. We also clarify three major issues in OAM multiplexing: beam divergence, mode-dependent performance degradation, and reception (Rx) signal-to-noise-ratio (SNR) reduction. To mitigate mode-dependent performance degradation we first present a simple but practical Rx antenna design method. Exploiting the fact that there are specific location sets with phase differences of 90 or 180 degrees, the method allows each OAM mode to be received at its high SNR region. We also introduce two methods to address the Rx SNR reduction issue by exploiting the property of a Gaussian beam generated by multiple uniform circular arrays and by using a dielectric lens antenna. We confirm the feasibility of OAM multiplexing in a proof of concept experiment at 5.2 GHz. The effectiveness of the proposed Rx antenna design method is validated by computer simulations that use experimentally measured values. The two new Rx SNR enhancement methods are validated by computer simulations using wireless transmission at 60 GHz.

A novel real-valued ESPRIT (RV-ESPRIT) algorithm is proposed to estimate the direction of arrival (DOA) and direction of departure (DOD) for noncircular signals in bistatic MIMO radar. By exploiting the property of signal noncircularity and Euler's formula, a new virtual array data of bistatic MIMO radar, which is twice that of the MIMO virtual array data, is established with real-valued sine and cosine data. Then the receiving/transmitting selective matrices are constructed to obtain the receiving/transmitting rotationally invariant factors. Compared to the existing angle estimation methods, the proposed algorithm has lower computational load. Simulation results confirm the effectiveness of the RV-ESPRIT.

A new class of visible light communication (VLC) systems, namely image sensor (IS) based VLC systems, has emerged. An IS consists of a two-dimensional (2D) array of photodetectors (PDs), and then VLC systems with an IS receiver are capable of exploiting the spatial dimensions invoked for transmitting information. This paper aims for providing a brief survey of topics related to the IS-based VLC, and then provides a matrix representation of how to map a series of one dimensional (1D) symbols onto a set of 2D symbols for efficiently exploit the associate grade of freedom offered by 2D VLC systems. As an example, the matrix representation is applied to the symbol mapping of layered space-time coding (L-STC), which is presented to enlarge the coverage of IS-based VLC that is limited by pixel resolution of ISs.

A power packet dispatching system is proposed to realize the function of power on demand. This system distributes electrical power in quantized form, which is called power processing. This system has extensibility and flexibility. Here, we propose to use the power packet dispatching system as the next generation power distribution system in self-established and closed system such as robots, cars, and aircrafts. This paper introduces the concept and the required researches to take the power packet dispatching system in practical phase from the total viewpoints of devices, circuits, power electronics, system control, computer network, and bio-inspired power consumption.

Locally repairable codes (LRCs) have attracted much interest recently due to their applications in distributed storage systems. In an [n,k,d] linear code, a code symbol is said to have locality r if it can be repaired by accessing at most r other code symbols. An (n,k,r) LRC with locality r for the information symbols has minimum distance d≤n-k-⌈k/r⌉+2. In this letter, we study single-parity LRCs where every repair group contains exactly one parity symbol. Firstly, we give a new characterization of single-parity LRCs based on the standard form of generator matrices. For the optimal single-parity LRCs meeting the Singleton-like bound, we give necessary conditions on the structures of generator matrices. Then we construct all the optimal binary single-parity LRCs meeting the Singleton-like bound d≤n-k-⌈k/r⌉+2.

The software development process is front-loaded when formal specification is deployed and as a consequence more problems are identified and solved at an earlier point of time. This places extra importance on the quality and efficiency of the different formal specification tasks. We use the term “exploratory modeling” to denote the modeling that is conducted during the early stages of software development before the requirements are clearly understood. We believe tools that support not only rigorous but also flexible construction of the specification at the same time are helpful in such exploratory modeling phases. This paper presents a web-based IDE named VDMPad to demonstrate the concept of exploratory modeling. VDMPad has been evaluated by experienced professional VDM engineers from industry. The positive evaluation resulting from such industrial users are presented. It is believed that flexible and rigorous tools for exploratory modeling will help to improve the productivity of the industrial software developments by making the formal specification phase more efficient.

We investigate a finite-sized self-complementary bow-tie antenna (SC-BTA) integrated with a semiconductor mesa with respect to radiation characteristics such as the peak radiation frequency and bandwidth around the fundamental radiation mode. For this investigation, we utilize an equivalent circuit model of the SC-BTA derived in our previous work and a finite element method solver. Moreover, we derive design guidelines for the radiation characteristics in the form of size scaling-rules with respect to the antenna outer size for a terahertz transmitter.

In general, semi-supervised clustering can outperform unsupervised clustering. Since 2001, pairwise constraints for semi-supervised clustering have been an important paradigm in this field. In this paper, we show that pairwise constraints (ECs) can affect the performance of clustering in certain situations and analyze the reasons for this in detail. To overcome these disadvantages, we first outline some exemplars constraints. Based on these constraints, we then describe a semi-supervised clustering framework, and design an exemplars constraints expectation-maximization algorithm. Finally, standard datasets are selected for experiments, and experimental results are presented, which show that the exemplars constraints outperform the corresponding unsupervised clustering and semi-supervised algorithms based on pairwise constraints.

Artificial lighting is responsible for a large portion of total energy consumption and has great potential for energy saving. This paper designs an LED light control algorithm based on users' localization using multiple battery-less binary human detection sensors. The proposed lighting control system focuses on reducing office lighting energy consumption and satisfying users' illumination requirement. Most current lighting control systems use infrared human detection sensors, but the poor detection probability, especially for a static user, makes it difficult to realize comfortable and effective lighting control. To improve the detection probability of each sensor, we proposed to locate sensors as close to each user as possible by using a battery-less wireless sensor network, in which all sensors can be placed freely in the space with high energy stability. We also proposed to use a multi-sensor-based user localization algorithm to capture user's position more accurately and realize fine lighting control which works even with static users. The system is actually implemented in an indoor office environment in a pilot project. A verification experiment is conducted by measuring the practical illumination and power consumption. The performance agrees with design expectations. It shows that the proposed LED lighting control system reduces the energy consumption significantly, 57% compared to the batch control scheme, and satisfies user's illumination requirement with 100% probability.

This letter introduces a new model for backscatter assisted wireless powered communication networks (BAWPCNs) that include a hybrid access point (HAP) and multiple backscatter communication (BackCom) and traditional wireless powered communication network (WPCN) users. To make full use of time to transmit information, both backscatter and harvest-then-transmit (HTT) modes are employed. In the proposed model, during the first time slot dedicated for energy transfer in traditional WPCNs, the traditional WPCN users harvest energy radiated by the HAP, and simultaneously the BackCom users reflect modulated signals to the HAP. The traditional WPCN users are scheduled during the remaining time slots via time division multiple access (TMDA). The optimal time allocation policies for the half-duplex (HD) and full-duplex (FD) BAWPCNs are obtained to maximize the system throughput. The tradeoff between backscatter and HTT modes is analyzed. Simulation results demonstrate the superiority of the proposed model.

In this paper, MWAN (Mobile Wireless Ad hoc Networks with internet connection) is considered, which is a solution for many tasks owing to its ease of use, and practicality. Recently, MWAN is required to support large data like multimedia data transfer and it is transferred through several relay nodes. There are 2 problems that cause difficulties for large data transfer through a mobile network. First one is rerouting delay by handoff and second one is network congestion caused by handoff. Also, faulty data transfer caused by handoff delay makes extra load and causes some problems for MWAN. To solve these problems and get network reliability, we propose a new multipath routing scheme that can provide solution for seamless connection while handoff. In the proposed scheme, our MWAN can support multiple paths for data transfer, maintain end-to-end connection while handoff and get new route quickly. The performance of the proposed scheme is evaluated and compared with other multipath routing scheme to show the improvement.

In this paper, we present sub-1-V CMOS-based electrophoresis method for small-form-factor biomolecule manipulation that is contained in a microchip. This is the first time this type of device has been presented in the literature. By combining CMOS technology with electroless gold plating, the electrode pitch can be reduced and the required input voltage can be decreased to less than 1 V. We fabricated the CMOS electrophoresis chip in a cost-competitive 0.6 µm standard CMOS process. A sample/hold circuit in each cell is used to generate a constant output from an analog input. After forming gold electrodes using an electroless gold plating technique, we were able to manipulate red food coloring with a 0-0.7 V input voltage range. The results shows that the proposed CMOS chip is effective for electrophoresis-based manipulation.