This paper describes the effects of system LSI design with C language-based behavioral synthesis following several trials of design period reduction and quality improvement for a variety of circuit types. The results of these trials are analyzed from the viewpoints of description productivity, verification productivity, reusability and design flexibility as well as hardware and software co-verification. First the C-based design flow proposed by the authors is described, and the design productivity and verification productivity under this design flow is compared to RTL design. The reusability of the behavioral IP core and its efficiency with HW/SW co-verification are also shown using design examples. Next, using the example of an MPEG-4 video decoder design, a typical design process in a C-based design is shown with considerations regarding verification efficiency, reusability of the IP core and HW/SW co-verification. Finally, the authors' perspectives regarding future directions of system LSI design are discussed.

This paper investigates a new method for creating robust speaker models to cope with inter-session variation of a speaker in a continuous HMM-based speaker verification system. The new method estimates session-independent parameters by decomposing inter-session variations into two distinct parts: session-dependent and -independent. The parameters of the speaker models are estimated using the speaker adaptive training algorithm in conjunction with the equalization of session-dependent variation. The resultant models capture the session-independent speaker characteristics more reliably than the conventional models and their discriminative power improves accordingly. Moreover we have made our models more invariant to handset variations in a public switched telephone network (PSTN) by focusing on session-dependent variation and handset-dependent distortion separately. Text-independent speech data recorded by 20 speakers in seven sessions over 16 months was used to evaluate the new approach. The proposed method reduces the error rate by 15% relatively. When compared with the popular cepstral mean normalization, the error rate is reduced by 24% relatively when the speaker models were recreated using speech data recorded in four or more sessions.

In the last three decades of the 20th Century, research in speech recognition has been intensively carried out worldwide, spurred on by advances in signal processing, algorithms, architectures, and hardware. Recognition systems have been developed for a wide variety of applications, ranging from small vocabulary keyword recognition over dial-up telephone lines, to medium size vocabulary voice interactive command and control systems for business automation, to large vocabulary speech dictation, spontaneous speech understanding, and limited-domain speech translation. Although we have witnessed many new technological promises, we have also encountered a number of practical limitations that hinder a widespread deployment of applications and services. On one hand, fast progress was observed in statistical speech and language modeling. On the other hand only spotty successes have been reported in applying knowledge sources in acoustics, speech and language science to improving speech recognition performance and robustness to adverse conditions. In this paper we review some key advances in several areas of speech recognition. A bottom-up detection framework is also proposed to facilitate worldwide research collaboration for incorporating technology advances in both statistical modeling and knowledge integration into going beyond the current speech recognition limitations and benefiting the society in the 21st century.

Batch verification is a useful tool in verifying a large number of cryptographic items all at one time. It is especially effective in verifying predicates based on modular exponentiation. In some cases, however the items can be incorrect although they pass batch verification together. Such leniency can be eliminated by checking the domain of each item in advance. With this in mind, we introduce the strict batch verification and investigate if the strict batch verification can remain more effective than separate verification. In this paper, we estimate the efficiency of such strict batch verification in several types of groups, a prime subgroup of Zp with special/random prime p and prime subgroups defined on elliptic curves over Fp, F2m and Fpm, with are often used in DL-based cryptographic primitives. Our analysis concludes that the efficiency differs greatly depending on the choice of the group and parameters determined by the verifying predicate. Furthermore, we even show that there are some cases where batch verification, regardless of strictness, loses its computational advantage.

This paper describes an automatic interface insertion scheme for in-system verification of algorithm models. To insert the interface, an algorithm model described in C is translated into another source code that includes the communication with hardware components in the target system to be validated with the algorithm model. The communication between the algorithm model and hardware components is achieved using transactors that perform transformation between access operations and bus cycle transactions. I/O terminal is introduced as an interface model to relate the transactions to access operations during the execution of the algorithm model, i.e., accesses to I/O terminals invoke bus cycle transactions in hardware and vice versa. An automatic interface insertion tool is developed using the source-to-source translation to identify the I/O terminals and insert interface function calls in the source code. The proposed automatic interface insertion scheme is validated by emulating several multimedia algorithms written in C on real target systems.

This paper develops a framework to support trace theoretic verification of timed circuits and systems. A theoretical foundation for classifying timed traces as either successes or failures is developed. The concept of the semimirror is introduced to allow conformance checking thus supporting hierarchical verification of timed circuits and systems. Finally, we relate our framework to those previously proposed for timing verification.

This paper deals with formal verification of high-level designs, in particular, symbolic comparison of register-transfer-level descriptions and behavioral descriptions. We use state machines extended by quantifier-free first-order logic with equality, as models of those descriptions. We cannot adopt the classical notion of equivalence for state machines, because the signals in the corresponding outputs of such two descriptions do not change in the same way. This paper defines a new notion of consistency based on signal-transitions of the corresponding outputs, and proposes an algorithm for checking consistency of those descriptions, up to a limited number of steps from initial states. As an example of high-level designs, we take a simple hardware/software codesign. A C program for digital signal processing called PARCOR filter was compared with its corresponding design given as a register-transfer-level description, which is composed of a VLIW architecture and assembly code. Since this example terminates within approximately 4500 steps, symbolic exploration of a finite number of steps is sufficient to verify the descriptions. Our prototype verifier succeeded in the verification of this example in 31 minutes.

This paper describes an efficient symbolic model checking algorithm for verification of deadlock free property of high level robot control program called Task Control Architecture (TCA). TCA is a model of concurrent robot control processes. The verification tool we used is the Symbolic Model Verifier (SMV). Since the SMV is not so efficient for verification of liveness properties of many concurrent processes such as deadlock free property, we first described the deadlock free property by using safety properties that SMV can verify efficiently. In addition, we modify the symbolic model checking algorithm of the SMV so that it can handle many concurrent processes efficiently. Experimental measurements show that we can obtain more than 1000 times speed-up by these methods.

This paper presents a formal verification method based on logic simulation. In our method, some restricted class of circuits which include data paths can be verified without abstraction of data paths by using symbolic values. Our verifier extracts a transition relation from the state graph (given as a specification) which is expressed using symbolic values, and verifies based on simulation using those symbolic values if the circuit behaves correctly with respect to each transition of the specification. If the verifier terminates with "correct," then it can be guaranteed that for any applicable input vector sequence, the circuit and the specification behaves identically. We have implemented the proposed method on a Unix workstation and verified some FIFO and LIFO circuits by using it.

Personal identity verification has a great variety of applications including access to computer terminals, buildings, credit card verification as well as EC. Algorithms for personal identity verification can be roughly classified into four categories depending on static/dynamic and biometric/physical or knowledge based. Finger prints, iris, retina, DNA, face, blood vessels, for instance, are static and biometric. Algorithms which are biometric and dynamic include lip movements, body movements and on-line signatures. Schemes which use passwords are static and knowledge based, whereas methods using magnetic cards and IC cards are physical. Each scheme naturally has its own advantages and disadvantages. A new algorithm is proposed for pen-input on-line signature verification incorporating pen-position, pen-pressure and pen-inclinations trajectories. A preliminary experiment is performed on a data base consisting of 293 genuine writings and 540 forgery writings, from 8 individuals. Average correct verification rate was 97.6% whereas average forgery refection rate was 98.7%. Since no fine tuning was done, this preliminary result looks very promising.

Recently, biometrics such as a person's fingerprint, face, and voice has come to be used for personal authentication. At present, most biometrics authentication systems depend on verification (one-to-one matching) because such verification takes a short period of time and is expected to provide a quick response. In these systems, however, every single user has to enter an ID number for each authentication session and might feel incovenienced as a result. To improve the operation efficiency, identification (one-to-many matching) is required, but identification is currently assumed to require much more time than verification (i.e., the response time is not practical). After probing these problems, we developed a new method to achieve identification in a short period of time. This method shortens the response time by using a matching score matrix, which is constructed in the enrollment phase. The proposed method is shown to need only about 45 one-to-one matchings to identify data in a database with two thousand fingerprints, a count much less than by conventional methods.

Message Sequence Chart (MSC) standardized by International Telecommunication Union is a graphical and textual language for specification of concurrent systems. It has been used formally as well as informally to specify behavior of real-time systems, in particular telecommunication switching systems. Formal verification of a system specification is crucial to ensure that implementation of the system works correctly. In particular, verification methods based on finite states have been widely used in telecommunication systems design. The methods determine global system states and transitions between them (i. e. , build a global state transition graph (GSTG)), and verify the system's desired properties, such as safety and liveness, on the GSTG. In this paper, we focus on construction of GSTGs from MSC specifications. We propose action dependency graph as an intuitive description of semantics of MSC specifications and present an algorithm to translate MSC specifications to action dependency graphs as well as an algorithm to construct a global state transition graph from an action dependency graph.

Timing verification of digital synchronous designs is a complex process that is traditionally carried out deep in the design cycle, at the gate level. A method, embodied in a C++ based design system, is presented that allows modeling and verification of clock regions at a higher level. By combining event-driven, clock-cycle true and behavioral simulation, we are able to perform static and dynamic timing analysis of the clock regions.

Multi-cycle paths are paths between registers where 2 or more clock cycles are allowed to propagate signals, and the detection of multi-cycle paths is important in deciding proper clock period, timing verification and logic optimization. This paper presents a satisfiability-based multi-cycle path detection method, where the detection problems are reduced to CNF formulae and the satisfiability is checked using SAT provers. We also show heuristics on conversion from multi-level circuits into CNF formulae. We have applied our method to ISCAS'89 benchmarks and other sample circuits. Experimental results show the remarkable improvements on the size of manipulatable circuits.

Generating state spaces is one of important and general methods in the analysis of Petri nets. There are two reasons why state spaces of Petri nets become so large. One is concurrent occurring of transitions, and the other is periodic occurring of firing sequences. This paper focuses on the second problem, and proposes a new algorithm for exploring state spaces of finite capacity Petri nets with large capacities. In the proposed algorithm, the state space is represented in the form of a tree such that a set of markings generated by periodic occurrences of firing sequences is associated with each node, and it is much smaller than the reachability graph.

We propose an extraction method of personal features based on on-line handwriting information. Most recent research has been focused on signature verification, especially in the field of on-line writer verification. However, signature verification has a serious problem in that it will accept forged handwriting. To solve this problem, we have introduced an on-line writer verification method which uses ordinary characters. In this method, any handwritten characters (i.e., ordinary characters) are accepted as a text in the verification process, and the text used in the verification process can be different from that in the enrollment process. However, in the proposed method, personal features are extracted only from the shape of strokes, and it is still uncertain how efficient other on-line information, such as writing pressure or pen inclination, is for extracting personal features. Therefore, we propose an extraction method of personal features based on on-line handwriting information, including writing-pressure and pen-inclination information. In the proposed method, handwriting information is described by a set of three-dimensional curves, and personal features are described by a set of Fourier descriptors for the three-dimensional curves. We also discuss the reliability of the proposed method with some simulation results using handwritten data. From these simulation results, it is clear that the proposed method effectively extracts personal features from ordinary characters.

Most of current codesign tools or methodologies only support validation in the form of cosimulation and testing of design alternatives. The results of hardware-software codesign of a distributed system are often not verified, because they are not easily verifiable. In this paper, we propose a new formal coverification approach based on linear hybrid automata, and an algorithm for automatically converting codesign results to the linear hybrid automata framework. Our coverification approach allows automatic verification of real-time constraints such as hard deadlines. Another advantage is that the proposed approach is suitable for verifying distributed systems with arbitrary communication patterns and system architecture. The feasibility of our approach is demonstrated through several application examples. The proposed approach has also been successfully used in verifying deadline violations when there are inter-task communications between tasks with different period lengths.

This paper proposes a model checking method for microcomputer programs. To deal with the state explosion problem, we adopt a compositional verification approach. Based on the proposed method, a microcomputer program for a real-life air-conditioner is verified. The program is large enough to cause state explosion. Among fourteen typical properties of the program, five properties are successfully verified by our method.

This paper proposes a method of automatically eliciting knowledge which is used to detect feature interactions in telecommunication services. With conventional methods, the knowledge is provided manually. With the proposed method, the knowledge is automatically elicited as service constraints. In telecommunication systems, when a new service is added, new state transitions are created. In case of new service, the new state should be reached in the state transitions. On the other hand, some states of existing services should not be reached. These constraints can be considered as knowledge for detecting feature interactions. This paper also proposes a scenario for detecting feature interactions using elicited knowledge. This scenario was confirmed as effective.

There are two approaches for formal verification of sequential designs or finite state machines: language containment checking and symbolic model checking. To verify designs of practical size, in these two approaches, designs are represented symbolically, in practice, by ordered binary decision diagrams. In the conventional algorithm for language containment checking, finite automata given as specifications are also represented symbolically. This paper proposes a new method, called partially explicit method for checking language containment. By representing states of finite automata given as specifications explicitly, this method can remove redundant computations, and as a result, provide better performance than the conventional method which uses the product machines of designs and specifications. The experimental results show that this approach is effective in checking language containment symbolically.