The increasing complexity of hardware designs makes functional verification a challenge. The key issue of the state-of-the-art verification approaches is to obtain a “good” model for automated test generation or for...
详细信息
ISBN:
(纸本)9781479920976
The increasing complexity of hardware designs makes functional verification a challenge. The key issue of the state-of-the-art verification approaches is to obtain a “good” model for automated test generation or formal property checking. In this paper, we describe techniques for deriving EFSM-based models from HDL descriptions and briefly discuss applications of such models for verification. The distinctive feature of the suggested approach is that it automatically determines what registers of a design encode its state and use this information for model reconstruction.
Correctness checking of HDL-model behavior is an integral part of runtime verification of hardware. As a rule, it is based on comparing of HDL-model behavior and reference model behavior, developed in high-level progr...
详细信息
Correctness checking of HDL-model behavior is an integral part of runtime verification of hardware. As a rule, it is based on comparing of HDL-model behavior and reference model behavior, developed in high-level programming languages. Being verified, both models are stimulated with the same input sequence; their output traces are caught and matched. Due to the abstractness of the reference model, the matching is not a trivial task as event sequences can be different and some events of one trace may miss in the other one. A methodology of runtime trace matching for hardware models of different abstraction levels is suggested in this paper. The methodology has been successfully applied to a number of industrial projects of unit-level microprocessor verification.
The recently discovered '***' worm has drastically changed the perception that systems managing critical infrastructure are invulnerable to software security attacks. Here we present an architecture that enhan...
详细信息
The problem of search efficiency through large amount of text data is well-known problem in computer science. We would like to introduce a BST data structure that allows searches through a set of string values, and is...
详细信息
The problem of search efficiency through large amount of text data is well-known problem in computer science. We would like to introduce a BST data structure that allows searches through a set of string values, and is optimized for reading and writing large blocks of data. This paper describes the algorithms for insertion, deletion and search of variable-length strings in diskresident trie structures. This data structure is used for value indexes on XML data. We also compare our implementation with existing B+ tree implementation and show that our structure occupies several times less space with the same search efficiency.
The paper presents a twofold verification system that aimes to be an open platform for experimentation with various verification techniques as well as an industrial-ready domain specific verification tool for Linux de...
详细信息
The paper presents a model-based tool chain for system design and system integration of integrated modular avionics in civil aviation domain. It describes architecture of the tool chain, its current state, use cases s...
详细信息
ISBN:
(纸本)9789290922650
The paper presents a model-based tool chain for system design and system integration of integrated modular avionics in civil aviation domain. It describes architecture of the tool chain, its current state, use cases supported and future directions of development.
Cluster structure is one of the main features of social graphs. Many algorithms have been proposed in recent years that are capable of revealing fuzzy communities. But a lot of them tend to degrade in some special cas...
详细信息
Cluster structure is one of the main features of social graphs. Many algorithms have been proposed in recent years that are capable of revealing fuzzy communities. But a lot of them tend to degrade in some special cases, for example when nodes assigned to more than two groups. Taking into account that such highly overlapping membership is rather common for many social networks, it becomes obvious that there is a need for flexible techniques and detecting the scope of their effective applicability for various network configuration parameters. This article focuses on the resistance to cluster's growth intersection with emphasis on local fitness function's optimization. The testing of the modern fuzzy clustering methods and generalized classical approaches is performed. Depending on the scale of fuzziness the conclusion is provided about the applicability of certain algorithm classes with common methodology and their representatives.
This project is an attempt to combine the advantages of software flexibility and security of hardware firewalls. It aims at the implementation of these advantages in the hypervisor source code for the purpose of creat...
详细信息
ISBN:
(纸本)9789898565242
This project is an attempt to combine the advantages of software flexibility and security of hardware firewalls. It aims at the implementation of these advantages in the hypervisor source code for the purpose of creating user data confidentiality protection against its leakage from the personal computer through the network. The hypervisor implementation is based on the hardware virtualization extensions of both processors and motherboards. This constitutes a key feature, which enables hypervisor to combine the following advantages: the advantages of access to the OS environment and hardware protection against various intruders' methods of compromise, including those capable of exploiting OS kernel resources for performing the malicious actions.
The paper presents an AADL-based toolset for Integrated Modular Avionics (IMA) design and integration. It describes activities of IMA system designer and system integrator that are supported by the toolset as well as ...
详细信息
In this paper we explore the prospects of virtualization technologies being applied to high performance computing tasks. We use an extensive set of HPC benchmarks to evaluate virtualization overhead, including HPC Cha...
详细信息
ISBN:
(纸本)9781450317542
In this paper we explore the prospects of virtualization technologies being applied to high performance computing tasks. We use an extensive set of HPC benchmarks to evaluate virtualization overhead, including HPC Challenge, NAS Parallel Benchmarks and SPEC MPI2007. We assess KVM and Palacios hypervisors and, with proper tuning of hypervisor, we reduce the performance degradation from 10-60% to 1- 5% in many cases with processor cores count up to 240. At the same time, a few tests provide overhead ranging from 20% to 45% even with our enhancements. We describe the techniques necessary to achieve sufficient performance. These include host OS tuning to decrease noise level, using nested paging with large pages for efficient guest memory allocation, and proper NUMA architecture emulation when running virtual machines on NUMA hosts. Comparing KVM/QEMU and Palacios hypervisors, we conclude that in general the results with proper tuning are similar, with KVM providing more stable and predictable results while Palacios being much better on fine-grained tests at a large scale, but showing abnormal performance degradation on a few tests. Copyright 2012 ACM.
暂无评论