Selected Abstracts
A novel formal verification approach for RTL hardware IP cores
Ridha Djemal, Mohamed Ayoub Dhouib, Samuel Dellacherie, Rached Tourki
Faculté des Sciences de Monastir, Avenue de l’Environnement 5000 Monastir, Tunisia
Telnet, Centre Urbain Nord 1082 Tunis, Tunisia
TNI-Valiosys, 4 avenue de Cambridge 14200 Herouville St. Clair, France
Abstract: We present a promising formal verification methodology based on the inductive approach using the imPROVE-HDL tool. This methodology is dedicated for RTL IPs or IP-based digital/logic hardware designs to prove the correctness of their temporal properties related to the control-dominated architecture model. Each temporal property can be checked through the IP interface where all properties have to be proved or disproved. We developed a new methodology to generate the appropriate environment of the IP interface according to the design context (master, slave, arbiter and decoder) before starting the verification of all properties one by one. When all temporal properties are verified, we generate some test sequences that contain a complex scenario to check the compatibility between all properties. We implemented our methodology to generate the appropriate environment and applied the inductive approach to verify various properties of two real IP designs using the imPROVE-HDL tool developed by TNI-Valiosys. The first design is an RTL IP-based digital hardware dedicated for real time video processing, where the second one performs an AHB to AHB Bridge. On these designs, we successfully proved few properties and discovered a design violation.
Keywords: Formal verification; Property checking; IP-based digital/logic hardware design verification; SAT: Boolean satisfiability approach; AMBA: advanced micro-controller bus architecture; AHB: advanced high performance bus.
A Blind Watermarking Algorithm Implementation for Digital Images and Video
Sourour Karmani, Ridha Djemal and Rached Tourki
Faculté des Sciences de Monastir, Avenue de l’Environnement 5000 Monastir, Tunisia
Abstract : With the growth of new image technologies, copyright protection becomes an important issue to preserve digital images and video properties. In this paper, we propose an improved implementation of a blind object watermarking scheme for images and video streams. To make the watermark robust and perceptual invisible, we have used a two dimensional wavelet transform as a transformation domain for both image and watermark. We have also used an optimized quantization and replacement strategies within the insertion process. Hardware architecture is designed and tested in order to evaluate the performance of our proposed watermarking algorithm. This architecture has been implemented on the Altera Stratix II prototyping board.
Keywords: Watermarking, 2D-DWT, insertion process, RTL implementation and FPGA.
High performance architecture of integrated protocols for encoded video application
H. Guesmi,*, R. Djemal, B. Boualleguea,b, J.-P. Diguetb, R. Tourkia
a Laboratoire d’Electronique et de Microélectroniques, Physic Department of Monastir ,
Avenue de l’Environnement, 5019 Monastir, Tunisia
b Laboratoire LESTER, Rue Saint Maudé 56321 Lorient Cedex, France
Abstract: Despite the evolution of high-speed communication network to accommodate an increasingly number of applications with diverse service requirements, there still exist a number of barriers related to the deployment of the encoded video over the ATM network. In fact, additional works have to be devoted to improve protocol architecture and to guarantee the QoS. In this paper, we first analyze the main parameters affecting the visual quality of real video pictures. Then, we define specific services to be implemented at the network interface level. We also discuss the proposed integrated protocols architecture for real time application such as video coding illustrating the function to support the challenges of managing real time services over high speed network. In fact, data cells are exposed to delays and losses, which affect the quality of the video signal. Therefore, we have to perform the adequate processing in order to keep the quality of service on an acceptable level. In this article, we propose the design of an interface between the MPEG-2 standard and the ATM network in order to improve the video visual quality. Our approach tries to overcome the difficulty imposed by traditional random cell discarding due to the bursty aspect of the traffic and the variable bit rate (VBR) transmission, nature of compressed video. The performance evaluation shows the effectiveness of the proposed interface architecture with the set of mechanisms in improving the robustness of the video delivery system.
Keywords: Asynchronous transfer mode; Motion picture expert group; Quality of service
Protocol architecture for MPEG-2 video over a high speed network
Bouallegue, B. Djemal, R. Guesmi, H. Diguet, J.P. Philippe, J.-L. Tourki, R.
Phys. Dept., Sci. Fac. of Monastir, Tunisia;
Real-time communication services related to encoded video transmission over a high-speed network such as ATM need a new integrated protocol architecture to meet the required quality. Data cells are exposed to delays and losses, which affect the video signal quality, and so adequate processing is needed in order to keep the quality of service as an acceptable level. The authors propose the design of a new adaptation of MPEG-2 video in ATM networks in order to improve the video visual quality. The approach, based on a new MPEG-2 protocol architecture, tries to overcome the difficulty imposed by traditional random cell discarding due to the bursty aspect of the traffic and the variable bit rate transmission nature of encoded video. The importance of including a dynamic bandwidth reallocation and appropriate interleaving technique for bursty encoded video traffic being carried in an ATM network is shown, by comparing the degradation quality of an MPEG-2 sequence with and without the proposed techniques. The results show that the proposed interface is effective in solving the cell-loss problem and thus enhances the QoS for MPEG-2 video transmission in ATM networks.
Rapid prototyping of an ATM programmable associative Operator
Ridha Djemal a,b,*, Guy Mazaré b, Rached Tourki a
a Laboratoire d'Electronique de Micro-électronique of Monastir,
Avenue de l'Environnement, 5019 Monastir, Tunisia
b Laboratoire Logiciels Systèmes Réseaux, Grenoble -IT (INPG),
* Centre National de la Recherche Scientifique (CNRS),
BP. 72, 38402 Saint Martin d'Hères, France
Abstract : In this paper, we describe a semi-automatic method for designing a programmable architecture related to high speed communication protocols. A case study of associative based architecture of high speed communication system is presented with a validation environment. The environment provides an interesting estimation using XILINX prototyping board including memories (content addressable memory, CAM, RAM, DPRAM). In our approach, we try to perform a rapid prototyping of such architecture and allow the designer to interact easily in order to customize the architecture according to application requirements. This method of validation provides important benefits in hardware prototyping: better validation environment and reduced time to give a real estimation for a large variety of applications.
Keywords: Asynchronous transfer mode (ATM); Content addressable memory (CAM); Quality of service (QoS); Interactive aided design utility (IADU).