Logic simulation is a crucial verification task in processor design. Aiming at significant acceleration of system simulation we have parallelized IBM's cycle-based simulator TEXSIM. The resulting parallelTEXSIM has already been employed successfully in simulating S/390 architectures on IBM SP systems. Here we present parallelTEXSIM together with its model partitioning environment.

Discrete Event Simulation on GPUs employing parallel heap data structure is the focus of this thesis. Two traditional algorithms, one being conservative and other being optimistic, for parallel discrete event simulation have been implemented on GPUs using CUDA. The first algorithm is the safe-window algorithm (conservative). It has produced expected performance when compared to sequential simulation. The second algorithm, known as SyncSim, is an optimistic simulation algorithm previously designed to be space efficient and reduce rollbacks. This algorithm is re-implemented on GPU platform with necessary changes on the logic simulator and the parallel heap implementation. The performance of the parallel heap when working with a logic simulator has also been validated against the results indicated in previous research paper on parallel heap without the logic simulator.

Parallelization of logic simulation on register-transfer and gate level is a promising way to accelerate extremely time extensive system simulation processes for whole processor structures. In this report parallel simulation realized by means of the functional simulator parallel- TEXSIM based on the clock-cycle algorithm is considered. Within a corresponding simulation, several simulator instances co-operate over a loosely-coupled processor system, each instance simulating a part of a synchronous hardware design. Therefore, in preparation of parallel simulation, partitioning of hardware models is necessary, which is essentially determining e±ciency of the following simulation. A framework of formal concepts for an abstract description of parallel cycle simulation is developed. This provides the basis for partition valuation within partitioning algorithms. Starting from the definition of a Structural Hardware Model as special bipartite graph Sequential Cycle Simulation is introduced as sequence of actions. Following a cone-based partitioning approach a Parallel Structural Hardware Model is defined as set of Structural Hardware Models. Furthermore, a model of parallel computation called Communicating Processors is introduced which is closely related to the well known LogP Model. Together with the preceding concepts it represents the basis for determining Parallel Cycle Simulation as sequence of action sets.

The partitioning of complex processor models on the gate and register-transfer level for parallel functional simulation based on the clock-cycle algorithm is considered. We introduce a hierarchical partitioning scheme combining various partitioning algorithms in the frame of a competing strategy. Melting together the di®erent partitioning results within one level using superpositions we crossover to a mixture of experts one. This approach is improved applying genetic algorithms. We present two new partitioning algorithms (experts), the Backward-Cone-Concentration algorithm (n-BCC) and the Minimum-Overlap Cone-Cluster algorithm (MOCC), both of them taking cones as fundamental units for building partitions.

Parallelization of logic simulation on register-transfer and gate level is a promising way to accelerate extremely time-extensive system simulation processes during the design of whole processor structures. The background of this paper is given by the functional simulator parallelTEXSIM realizing simulation based on the clock-cycle algorithm over loosely-coupled parallel processor systems. In preparation for parallel cycle simulation, partitioning of hardware models is necessary, which essentially determines the efficiency of the following simulation. We introduce a new method of parameterized partition valuation for use within model partitioning algorithms. It is based on a formal definition of parallel cycle simulation involving a model of parallel computation called Communicating Processors. Parameters within the valuation function permit consideration of specific properties related to both the simulation target architecture and the hardware design to be simulated. Our partition valuation method allows performance estimation with respect to corresponding parallel simulation. This has been confirmed by tests concerning several models of real processors as, for instance, the PowerPC 604 with parallel simulation running on an IBM SP2.

The partitioning of complex processor models on the gate and register-transfer level for parallel functional simulation based on the clock-cycle algorithm is considered. We introduce a hierarchical partitioning scheme combining various partitioning algorithms in the frame of a competing strategy. Melting together different partitioning results within one level using superpositions we crossover to a mixture of experts one. This approach is improved applying genetic algorithms. In addition we present two new partitioning algorithms both of them taking cones as fundamental units for building partitions.

During the design and verification of the Hyperstone S5 flash memory controller, we developed a highly effective way to use the SystemVerilog direct programming interface (DPI) to integrate an instruction set simulator (ISS) and a software debugger in logic simulation. The processor simulation was performed by the ISS, while all other hardware components were simulated in the logic simulator. The ISS integration allowed us to filter many of the bus accesses out of the logic simulation, accelerating runtime drastically. The software debugger integration freed both hardware and software engineers to work in their chosen development environments. Other benefits of this approach include testing and integrating code earlier in the design cycle and more easily reproducing, in simulation, problems found in FPGA prototypes.

During the design and verification of the Hyperstone S5 flash memory controller, we developed a highly effective way to use the SystemVerilog direct programming interface (DPI) to integrate an instruction set simulator (ISS) and a software debugger in logic simulation. The processor simulation was performed by the ISS, while all other hardware components were simulated in the logic simulator. The ISS integration allowed us to filter many of the bus accesses out of the logic simulation, accelerating runtime drastically. The software debugger integration freed both hardware and software engineers to work in their chosen development environments. Other benefits of this approach include testing and integrating code earlier in the design cycle and more easily reproducing, in simulation, problems found in FPGA prototypes.

Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.