Recent advancement in hardware design urge during a transaction based model as a new intermediate design level. Supporters for the Transaction Level Modeling (TLM) trend claim its efficiency in terms of rapid prototyping and fast simulation incomparison to the classical RTL-based approach. Intuitively, from a verification point of view, faster simulation induces better coverage results. This is driven by two factors: coverage measurement and simulation guidance. In this paper, we propose to use an abstract model of the design, written in the Abstract State Machines Language(AsmL), in order to provide an adequate way for measuring the functional coverage. Then, we use this metric indefining the fitness function of a genetic algorithm proposed to improve the simulation efficiency. Finally, we compare our coverage and simulation results to:(1) random simulation at TLM; and (2) the Specman tool of Verisityat RTL.

The importance of re-usable intellectual properties (IPs) cores is increasing due to the growing complexity of today's system-on-chip and the need for rapid prototyping. In this paper, we provide a design for verification approach of a PCI-X bus model, which is the fastest and latest extension of PCI technologies. We use two different modeling levels, namely UML and AsmL. We integrate the verification within the design phases where we use model checking and model based testing, respectively at the AsmL and SystemC levels. This case study presents an illustration of the integration of formal methods and simulations for the purpose of providing better verification results of SystemC IPs

Transaction-level modeling allows exploring several SoC design architectures, leading to better performance and easier verification of the final product. In this paper, we present an approach to design and verify SystemC models at the transaction level. We integrate the verification as part of the design flow where we first model both the design and the properties (written in Property Specification language) in Unifed Modeling Language (UML); then, we translate them into an intermediate format modeled with AsmL [language based on Abstract State Machines (ASM)]. The AsmL model is used to generate a finite state machine of the design, including the properties. Checking the correctness of the properties is performed on the fly while generating the state machine. Finally, we translate the verified design to SystemC and map the properties to a set of assertions (as monitors in C#) that can be reused to validate the design at lower levels by simulation. For existing SystemC designs, we propose to translate the code back to AsmL in order to apply the same verification approach. At the SystemC level, we also present a genetic algorithm to enhance the assertions coverage. We will ensure the soundness of our approach by proving the correctness of the SystemC-to-AsmL and AsmL-to-SystemC transformations. We illustrate our approach on two case studies including the PCI bus standard and a master/slave generic architecture from the SystemC library.

Transaction level modeling allows several SoC design architectures to be explored, leading to better performance and easier verification of the final product. We present an approach to design and verify SystemC models at the transaction level. We integrate the verification as part of the design-flow. In this approach, we first model both the design and the properties (written in PSL - Property Specification Language) in UML. Then, we translate them into an intermediate format modeled by abstract state machines (ASM). The ASM model is used to generate an FSM of the design including the properties. Checking the correctness of the properties is performed on-the-fly while generating the state machine. Finally, we translate the verified design to SystemC and map the properties to a set of assertions (as monitors in C#) that can be re-used to validate the design at lower levels through simulation. We illustrate our approach on two case studies, the PCI bus standard and a generic master/slave architecture from the SystemC library.

In this paper, we present a technique to design and verify the look-aside (LA-1) interface standard used in network processors. Our design flow includes several refinements starting from an informal UML specification until getting to an RTL modeled in Verilog. We integrate the verification of the LA-interface in the design flow by considering two intermediate levels: (1) abstract state machines (ASM); and (2) SystemC. The first one serves the verification by model checking of a set of PSL properties, while the second includes a set of assertions to be verified by simulation. To evaluate the performance of our approach, we used the rule-base model checker to verify the same properties; and the OVL library to verify the same assertions.

In this paper we describe a methodology for the formal verification of a DSP chip using the HOL theorem prover. We used an iterative method to specify both the behavioral and structural descriptions of the processor. Our methodology consists of first simplifying the representations of the DSP units. We then prove for each unit that its hardware description implies its behavioral specification. Using the simplified (abstracted) description of the units we have been able to greatly reduce the cost of deducing the behavior of the processor instruction set from the hardware implementation of the processor units. The proposed methodology creates a new representation of the processor at each iteration such that its complexity can be handled by the theorem prover. This allowed us to make a proof of the full instruction set of this processor.

In hybrid coding technique, the sampled data are divided into blocks ofN \times Msamples. Next, each block is transformed to generate a one-dimensional transform of each line in the block. The transform coefficients are then processed by a block of DPCM encoders which uncorrelate the data in the second dimension and qnantize the uncorrelated samples using appropriate quantizers. In this study an adaptive hybrid coding technique is proposed based on using a single quantizer (A/D converter) to quantize the transform coefficients and using a variable-rate algorithm for coding the quantized coefficients. The accuracy of the A/D converter (number of bits per sample) determines the fidelity of the system. The buffercontrol algorithm controls the accuracy of the A/D converter for each block resulting in a fixed-rate encoder system. Experimental results have shown a stable buffer condition and reconstructed images with a higher fidelity than nonadaptive hybrid systems.

The Space Shuttle initially will be using a field-sequential color television system but it is possible that an NTSC color TV system may be used for future missions. In addition to downlink color TV transmission via analog FM links, the Shuttle will use a high resolution slow-scan monochrome system for uplink transmission of text and graphics information. This paper discusses the characteristics of the Shuttle video systems, and evaluates digitization and/or bandwidth compression techniques for the various links. The more attractive techniques for the downlink video are based on a two-dimensional DPCM encoder that utilizes temporal and spectral as well as the spatial correlation of the color TV imagery. An appropriate technique for distortion-free coding of the uplink system utilizes two-dimensional HCK codes.

Computational aspects of Wiener filtering of discrete Markov sequences are studied. It is shown that using lower triangular transformation, an extremely efficient suboptimal Wiener filter can be designed. The performance of the suboptimal filter for a first-, second-, and third-order Markov sequence is evaluated and is compared to the performance of the Wiener filter for these sequences.

The following is a survey of the technical literature on adaptive coding of imagery. Section 1 briefly discusses the general problem of image data compression. The optimum image data compression system, from a theoretical viewpoint, is presented in Section 1.1. The theoretical and the implementational problems of the optimum system are discussed and the assumptions that are made to overcome these problems are outlined. One important assumption is the stationarity which is not true for most imagery. In adaptive systems the parameters are varied according to changes in signal statistics optimizing the system performance for nonstationary signals. In this article the adaptive systems are divided to four categories. Section 2 is a survey of adaptive transform coding systems. Section 3 discusses adaptive predictive coding systems. Sections 4 and 5 discuss adaptive cluster coding and adaptive entropy technique, respectively.

Two hybrid coding systems utilizing a cascade of a unitary transformation and differential pulse code modulators (DPCM) systems are proposed. Both systems encode the transformed data by a bank of DPCM systems. The first system uses a one-dimensional transform of the data where the second one employs two-dimensional transformations. Theoretical results for Markov data and experimental results for a typical picture are presented for Hadamard, Fourier, cosine, slant, and the KarhunenLoeve transformations. The visual effects of channel error and also the impact of noisy channel on the performance of the hybrid system, measured in terms of the signal-to-noise ratio of the encoder, is examined and the performance of this system is compared to the performances of the two-dimensional DPCM and the standard two-dimensional transform encoders.

We consider a transform coding system that uses a lower-triangular transformation to uncorrelate the data. Based on this transformation we propose a generalized differential pulse code modulation (DPCM) system and show that at high bit rates it performs almost as well as coding by the method of principal components (Karhunen-Loeve transformation). This study connects the transform coding system to the DPCM encoder by showing that the proposed system simplifies to a standard DPCM encoder for Markov data.

A number of schemes for implementing a fast multiplier are presented and compared on the basis of speed, complexity, and cost. A parallel multiplier designed using the carry-save scheme and constructed from 74 series integrated circuits is described. This multiplier multiplies 10-bit by 12-bit binary numbers with a worst- case multiplication time of 520 ns. The cost of the integrated circuits was less than $ 500.

Still pictures can be modeled as realizations of a two-dimensional random field. Similarly, pictures that unfold with time across an aperture can be modeled as realizations of three-dimensional fields. Correlated sources can be found by looking at different regions of the spectrum or at different areas of a picture. Under the assumption that the sources are Gaussian a method is presented for finding the rate distortion function for all such sources, under a mean-square-error criterion, in terms of their power spectral densities. In particular, the rate distortion functions for a pair of correlated processes and for a two-dimensional random field are derived.