We demonstrated a compact 16×16 multicast switch (MCS) made from a silica-based planar lightwave circuit (PLC). The switch utilizes a new electrical connection method based on surface mount technology (SMT). Five electrical connectors are soldered directly to the PLC by using the standard reflow process used for electrical devices. We reduced the chip size to half of one made with conventional wire bonding technology. We obtained satisfactory solder contacts and excellent switching properties. These results indicate that the proposed method is suitable for large-scale optical switches including MCSs, variable optical attenuators, dispersion compensators, and so on.

Simultaneous multithreading (SMT) technology improves CPU throughput, but also causes unpredictable performance fluctuations for co-running workloads. Although recent major SMT processors have adopted some techniques to promote hardware support for quality-of-service (QoS), achieving both precise performance guarantees and high throughput on SMT architectures is still a challenging open problem. In this paper, we demonstrate through some comprehensive investigations on a cycle-accurate simulator that not only almost all in-core resources suffer from severe contention as workloads vary but also there is a non-linear relationship between performance and available quotas of resources. We consider these observations as the fundamental reason leading to the challenging problem above. Thus, we introduce QoSMT, a novel hardware scheme that leverages a closed-loop controlling mechanism consisting of detection, prediction and adjustment to enforce precise performance guarantees for specific targets, e.g. achieving 85%, 90% or 95% of the performance of a workload running alone respectively. We implement a prototype on GEM5 simulator. Experimental results show that the average control error is only 1.4%, 0.5% and 3.6%.

Safety critical systems are often modeled using Time Petri Nets (TPN) for analyzing their reliability with formal verification methods. This paper proposed an efficient verification method for TPN introducing bounded model checking based on satisfiability solving. The proposed method expresses time constraints of TPN by Difference Logic (DL) and uses SMT solvers for verification. Its effectiveness was also demonstrated with an experiment.

This paper presents a formal approach for generating train timetables in a mesoscopic level that is more concrete than the macroscopic level, where each station is simply expressed in a black-box, and more abstract than the microscopic level, where the infrastructure in each station-area is expressed in detail. The accuracy of generated timetable and the computational effort for the generation is a trade-off. In this paper, we design a formal mesoscopic modeling language by analyzing real railways, for example Tazawako-line as the first step of this work. Then, we define the constraint formulae for generating train timetables with the help of SMT (Satisfiability Module Theories)-Solver, and explain our tool RW-Solver that is an implementation of the constraint formulae. Finally, we demonstrate how RW-Solver with the help of SMT-Solver can be used for generating timetables in a case study of Tazawako-line.

In multiprocessors, memory models are introduced to describe the executions of programs among processors. Relaxed memory models, which relax the order of executions, are used in the most of the modern processors, such as ARM and POWER. Due to a relaxed memory model could change the program semantics, the executions of the programs might not be the same as our expectation that should preserve the program correctness. In addition to relaxed memory models, the way to execute an instruction is described by an instruction semantics, which varies among processor architectures. Dealing with instruction semantics among a variety of assembly programs is a challenge for program verification. Thus, this paper proposes a way to verify a variety of assembly programs that are executed under a relaxed memory model. The variety of assembly programs can be abstracted as the way to execute the programs by introducing an operation structure. Besides, there are existing frameworks for modeling relaxed memory models, which can realize program executions to be verified with a program property. Our work adopts an SMT solver to automatically reveal the program executions under a memory model and verify whether the executions violate the program property or not. If there is any execution from the solver, the program correctness is not preserved under the relaxed memory model. To verify programs, an experimental tool was developed to encode the given programs for a memory model into a first-order formula that violates the program correctness. The tool adopts a modeling framework to encode the programs into a formula for the SMT solver. The solver then automatically finds a valuation that satisfies the formula. In our experiments, two encoding methods were implemented based on two modeling frameworks. The valuations resulted by the solver can be considered as the bugs occurring in the original programs.

Simulation-based verification of hardware designs, in particular, register-transfer-level (RTL) designs, has been widely used, and has been one of the major bottlenecks in design processes. One of the approaches is coverage-driven verification, of its target is improvement of some metric called coverage. In a prior work of ours, we have proposed a coverage-driven verification using both randomly generated simulation patterns and patterns generated by a SAT (satisfiability) solver, and have shown its effectiveness. In this paper, we extend this approach with an SMT (satisfiability modulo theory) solver, which can handle arithmetic relations among integer, floating-point or bit-vector variables. Experimental results show that the more arithmetic modules are included, the more an SMT-based method gets superior to the method using only a SAT solver.

Approximate computing is considered as a promising approach to design of power- or area-efficient digital circuits. This paper proposes a systematic methodology for design and worst-case accuracy analysis of approximate array multipliers. Our methodology systematically designs a series of approximate array multipliers with different area, delay, power and accuracy characteristics so that an LSI designer can select the one which best fits to the requirements of her/his applications. Our experiments explore the trade-offs among area, delay, power and accuracy of the approximate multipliers.

In a real-time system, tasks are required to be completed before their deadlines. Under normal workload conditions, a scheduler with a proper scheduling policy can make all the tasks meet their deadlines. However, in practical environment, system workload may vary widely. Once system workload becomes too heavy, so that there does not exist a feasible schedule can make all the tasks meet their deadlines, we say the system is overloaded under which some tasks will miss their deadlines. To alleviate the degrees of system performance degradation caused by the missed deadline tasks, the design of scheduling is crucial. Many design objectives can be considered. In this paper, we first focus on maximizing the total number of tasks that can be completed before their deadlines. A scheduling method based on satisfiability modulo theories (SMT) is proposed. In the method, the problem of scheduling is treated as a satisfiability problem. The key work is to formalize the satisfiability problem using first-order language. After the formalization, a SMT solver (e.g., Z3, Yices) is employed to solve this satisfiability problem. An optimal schedule can be generated based on the solution model returned by the SMT solver. The correctness of this method and the optimality of the generated schedule can be verified in a straightforward manner. The time efficiency of the proposed method is demonstrated through various simulations. Moreover, in the proposed SMT-based scheduling method, we define the scheduling constraints as system constraints and target constraints. This means if we want to design scheduling to achieve other objectives, only the target constraints need to be modified. To demonstrate this advantage, we adapt the SMT-based scheduling method to other design objectives: maximizing effective processor utilization and maximizing obtained values of completed tasks. Only very little changes are needed in the adaption procedure, which means the proposed SMT-based scheduling method is flexible and sufficiently general.

Web Service Business Process Execution Language (BPEL) has become the de facto standard for developing instant service-oriented workflow applications in open environment. The correctness and reliability of BPEL processes have gained increasing concerns. However, the unique features (e.g., dead path elimination (DPE) semantics, parallelism, etc.) of BPEL language have raised enormous problems to it, especially in path feasibility analysis of BPEL processes. Path feasibility analysis of BPEL processes is the basis of BPEL testing, for it relates to the test case generation. Since BPEL processes support both parallelism and DPE semantics, existing techniques can't be directly applied to its path feasibility analysis. To address this problem, we present a novel technique to analyze the path feasibility for BPEL processes. First, to tackle unique features mentioned above, we transform a BPEL process into an intermediary model — BPEL control flow graph, which is proposed to abstract the execution flow of BPEL processes. Second, based on this abstraction, we symbolically encode every path of BPEL processes as some Satisfiability formulas. Finally, we solve these formulas with the help of Satisfiability Modulo Theory (SMT) solvers and the feasible paths of BPEL processes are obtained. We illustrate the applicability and feasibility of our technique through a case study.

We present a method to constrain a statistical generative word alignment model with the output from a discriminative model. The discriminative model is trained using a small set of hand-aligned data that ensures higher precision in alignment. On the other hand, the generative model improves the recall of alignment. By combining these two models, the alignment output becomes more suitable for use in developing a translation model for a phrase-based statistical machine translation (SMT) system. Our experimental results show that the joint alignment model improves the translation performance. The improvement in average of BLEU and METEOR scores is around 1.0-3.9 points.

We propose a low-power resource-shared VLIW processor (RSVP) for future leaky nanometer process technologies. It consists of several single-way independent processor units (IPUs) that share parallel processor resources. Each IPU works as a variable-way VLIW processor sharing the parallel resources according to priorities of given tasks. RSVP allocates shared parallel resources to the IPUs cycle by cycle. It can minimize the number of NOPs that is wasting power. The performance per power (P3) of a 4-parallel 4-way RSVP that corresponds to four 4way VLIWs is 3.7% better than a conventional 4-parallel 4-way VLIW multiprocessor in the current 90 nm process. We estimate that the RSVP achieves 36% less leakage power and 28% better P3 in the future 25 nm process. We have fabricated an RSVP test chip that contains two IPU and a shared resource equivalent to two 2way VLIWs in a 180 nm process. It is functional at 100 MHz clock speed and its power is 130 mW.

Optical surface mount technology (O-SMT), which was proposed to provide a possible solution to growing serious problems in manufacturing process of optoelectronic products, is introduced. After discussing the basic idea of O-SMT, experimental results are also described to show its feasibility.