Streamline is widely used in flow field visualization. Information-theoretic streamline distribution method performs well on demonstrating feature regions but only considers the direction component of vector. Our algorithm places streamlines based on information entropy calculated by both vector direction and vector magnitude, to cover more information of the flow field. By considering vector magnitude, the initial streamlines derived from entropy and supplementary streamlines derived from conditional entropy can convey the steepness of speed variation. An advanced streamline pruning method is also applied to improve the efficiency of our algorithm. Results prove that the streamlines produced by our algorithm can reflect the vector magnitude variation of a flow field without losing sight of the salient features.

This paper focused on the safety verification of the multithreaded programs for mobile crowdsourcing networks. A novel algorithm was proposed to find a way to apply IC3, which is typically the fastest algorithm for SAT‐based finite state model checking, in a very clever manner to solve the safety problem of multithreaded programs. By computing a series of overapproximation reachability, the safety properties can be verified by the SAT‐based model checking algorithms. The results show that the new algorithm outperforms all the recently published works, especially on memory consumption (an advantage that comes from IC3).

With the increasing size of flow field, a challenge in streamline visualization arises that the memory of calculation node cannot accommodate the entire required data. To solve this problem, out-of-core technique divides the flow field into blocks and read block on demand of computing. Data prefetching is a frequent out-of core method to reduce the affection of the gap between I/O and calculation speed, while the performance is coherent with prefetching hit rate. In this paper, we focus on how to improve the prefetching hit rate to increase the data prefetching efficiency by changing the style of flow field partitioning, and present a novel feature-based dynamic block partition method that divides data to blocks of different sizes. The key of our method is first to compute the feature attributes of the field, and then determine the partitioning points by specific operations to divide feature regions more finely. It is easy to apply our approach to replace block partition part of all state-of-the-art prefetching algorithms. Experimental results show that the major quality measurement of our partitioning strategy for prefetching is much better than the traditional methods, with an increase of about 10%in both prefetch hit rate and effective rate.

Finite Time Lyapunov Exponent (FTLE) is widely used in Lagrangian Coherent Structure extraction and research on unsteady flow field. FTLE is computationally expensive due to the flow map calculation on dense samples in the field. In order to improve the computation efficiency, we investigate the most time-consuming flow map and propose UIA, a Uniform Integrated Advection algorithm based on piecewise linear hypothesis. FTLE coverts multiple spatiotemporal interpolations and multi-step time advection into single matrix multiplication so as to dramatically reduce computation and be applied to any type of grids. We also design an UIA based FTLE algorithm on GUP and MIC to further reduce computation time, and present corresponding performance optimization strategies. The correctness and accuracy of algorithm are also experimentally verified by applying the algorithm to an analytical 3-dimensional field. The speedup ratio of the proposed algorithm ranges from 6 to 143 compared with FTLE execution time based on traditional RK4 flow map, which demonstrates that UIA has significantly improve the efficiency of FTLE computation and visualization.

Missing features often occurs in both streamline placement and streamline selection. To solve this problem, a feature-based approach to streamline selection that can guarantee the preservation of the integrity of flow field features is presented in this paper. The streamline feature type is defined based on the relationship between streamlines and flow field features. Given a large number of randomly or uniformly seeded streamlines, the proposed approach judges the feature type for each streamline by considering its geometric characteristics and amount of the information. All streamlines are then clustered according to their feature types and positions. Streamlines are selected from those feature streamline clusters. In addition, a streamline similarity measure based on the dynamic time warping algorithm and the mean of closest point distances is presented to avoid selecting redundant streamlines. The developed algorithm is applied to multiple data sets and compared with a recent streamline selection algorithm. Results show that the developed algorithm can reflect the key features of a flow field more effectively and greatly improve the readability of streamline visualizations.

Application mapping algorithm for reconfigurable architecture is one of the major research direction in reconfigurable computing. In this paper, we analyze the data memory bank conflict problem of the ACRPs (Application Customized Reconfigurable Pipelines) when exploiting the data parallelism and a conflict-free iteration-data mapping algorithm based on the operation mapping results is proposed to conquer the bank conflict problem. The experiments showed that ACRP can exploit the CFU, pipeline- and data-level parallelism efficiently. More specifically, the iteration-data mapping algorithm avoids the bank conflicts while exploiting the data parallelism to increase the throughput.

In this paper, we present a novel feature extraction approach called FLDA for unsteady flow fields based on Latent Dirichlet allocation (LDA) model. Analogous to topic modeling in text analysis, in our approach, pathlines and features in a given flow field are defined as documents and words respectively. Flow topics are then extracted based on Latent Dirichlet allocation. Different from other feature extraction methods, our approach clusters pathlines with probabilistic assignment, and aggregates features to meaningful topics at the same time. We build a prototype system to support exploration of unsteady flow field with our proposed LDA-based method. Interactive techniques are also developed to explore the extracted topics and to gain insight from the data. We conduct case studies to demonstrate the effectiveness of our proposed approach.

Soft errors have become a critical challenge as a result of technology scaling. However, to evaluate the influence of soft errors in flip-flop (FF) on the failure of circuit is a hard verification problem. Here, we proposed a novel flip-flop soft error failure rate analysis methodology using sequential equivalence checking (SEC) and taking the application behaviors into consideration, which combines the advantage of formal techniques based approaches in completeness and the advantage of application behaviors in accuracy in differentiating vulnerability of FFs. As a result, all the FFs in a circuit are sorted by their failure rates and designers can use this information to perform optimal hardening of selected sequential components against soft errors. Experimental results on an implementation of a SpaceWire end node and the set of the largest ISCAS'89 benchmark sequential circuits demonstrate the efficiency of our approach. Case study on an instruction decoder of a practical 32 bits microprocessor shows the applicable of our methodology.

The always increasing complexity of digital system makes designers start the design from more abstract System Level Modeling (SLM). However, the SLM arouses a new challenge for verification engineer to guarantee the functional equivalence between SLM specifications and Transaction Level Modeling (TLM) or other lower level implementations. This paper proposes a novel method for equivalence checking between SLM and TLM based on coverage directed simulation. In the proposed method, firstly quality measurements based on both code and functional coverage are used to generate simulation stimuli for SLM. Then the generated stimuli are used to simulate the SLM and TLM designs concurrently. Finally, equivalence checking is carried out based on the simulation results of the selected observing variables. With the proposed method, we can check the equivalence between SLM and TLM designs more efficiently with less simulation cost. The promising experimental results show the efficiency of our method.

Functional verification is the most difficult and time-consuming step in VLSI design flow, owing to the complexity and scale of chips rapidly increasing. The key problem of VLSI functional verification is improving the efficiency and coverage. For the important component-Cache in the microprocessors, an FPGA-based pseudo-random functional verification method is proposed in this paper. The test bench of this method is synthesizable, and the field programmable gate array (FPGA) emulation process is integrated to improve the efficiency of verification. The functional verification coverage is increased by automatically generating the constraints directed pseudo-random test stimuli. The method is applied in the real chips, and is compared with the pseudo-random software simulation method. The results show that our method is faster by about three orders of magnitude, and find more bugs in the designs.

With the on-chip resources largely increased, modern architectures are much different from traditional ones. The relation between temporal computing and spatial computing is getting more and more intricate. In this paper, we first analyzed and compared the abstract computing models of modern architectures. Then, a runtime reconfigurable architecture called programmable dataflow computing architecture (ProDFA) is proposed. The architecture of ProDFA is sumarized, then the process of how applications are mapped and execute are simply introduced. As a case study, a specific reconfigurable structure for symmetric ciphers is implemented. Performance of several typical symmetric ciphers are evaluated. The experimental results show high performance and efficiency of ProDFA.

Complementary synthesis can automatically synthesize the decoder circuit of an encoder. However, its user needs to manually specify an assertion on some configuration pins to prevent the encoder from reaching the nonworking states. To avoid this tedious task, this paper propose an automatic approach to infer this assertion, by iteratively discovering and removing cases without decoders. To discover all decoders that may exist simultaneously under this assertion, a second algorithm based on functional dependency is proposed to decompose , the Boolean relation that uniquely determines the encoder's input, into all possible decoders. To help the user select the correct decoder, a third algorithm is proposed to infer each decoder's precondition formula, which represents those cases that lead to this decoder's existence. Experimental results on several complex encoders indicate that our algorithm can always infer assertions and generate decoders for them. Moreover, when multiple decoders exist simultaneously, the user can easily select the correct one by inspecting their precondition formulas.

Existing techniques for animation of object fracture have a basic assumption that the object materials are homogeneous while most materials in real world are heterogeneous. To solve this problem, we introduce a novel method called MCA to simulate the fracture of heterogeneous materials. The method of movable cellular automata (MCA) is based on the discrete concept and provides advantages both of classical cellular automaton and discrete element methods. First, the object is represented as discrete sphere particles, named movable cellular automata, and then the MCA method is used to simulate the material and physical properties as well as to determine when and where the fracture occurs. To meet the real-time requirement, the MCA simulation is performed on GPU with CUDA in order to accelerate the complex calculation of automata's physical properties. After simulation, the results are directly sent to the vertex buffer object (VBO) for rendering to avoid the costly communication between CPU and GPU. The experimental results show the feasibility and effectiveness of the proposed method.

Due to its high performance/cost ratio, a single PC equipped with multi-GPU is an attractive platform for large scale scene rendering and visualization. In this paper, we present a compositeless parallel rendering algorithm on shared memory multi-GPU system. Our algorithm is based on hybrid sort-first and sort-last render mode. By utilizing the DMA asynchronous transfer in modern video cards, we implement asynchronous image read back and implicit image compositing. Using the compositeless algorithm, we totally remove image compositing stage in parallel rendering contrasting with the traditional parallel rendering methods. The theoretical analysis and experiments demonstrate that our algorithm is practical and scalable for large scale scene rendering and high-resolution display.

With the on-chip resources largely increased, the computing paradigm of modern architectures are much different from traditional ones. The relation between temporal computing and spatial computing is getting more and more intricate. In this paper, a coarse-grained reconfigurable architecture is proposed named as programmable dataflow computing architecture: ProDFA. With both fine-grained control ability and long-term control logic, ProDFA implements coarse-grained reconfigurability and fine-grained controllability, which brought both flexible programmability and high efficiency. A case study on block ciphers is done. A specific reconfigurable structure for block ciphers is designed and several mainstream block ciphers are mapped and evaluated. The experimental results show the high efficiency of the specific reconfigurable structure.

Complementary synthesis automatically synthesizes the decoder circuit of an encoder. It determines the existence of the decoder by checking whether the encoder's input can be uniquely determined by its output. However, this algorithm will not halt if the decoder does not exist. To solve this problem, a novel halting algorithm is proposed. For every path of the encoder, this algorithm first checks whether the encoder's input can be uniquely determined by its output. If yes, the decoder exists; otherwise, this algorithm checks if this path contains loops, which can be further unfolded to prove the non-existence of the decoder for all those longer paths. To illustrate its usefulness and efficiency, this algorithm has been run on several complex encoders, including PCI-E and Ethernet. Experimental results indicate that this algorithm always halts properly by distinguishing correct encoders from incorrect ones, and it is more than three times faster than previous ones.

With technology scaling, radiation-induced soft error has been a major concern even for mainstream enterprise applications. Since various hardening solutions impose significant costs in performance, area and power consumption, full soft error protection can hardly satisfy the multiple design goals simultaneously. Recent studies have noted that the circuits have partial intrinsic immunity to soft errors. And the interest in using the circuit's intrinsic immunity to improve the tradeoffs between reliability and various overhead from hardening is growing. However, most existing approaches cannot use it well. In this paper, the aim is to explore the principal source of the circuits' immunity to guide fault tolerance to make better use of it. We categorized the components in a circuit into three classes: components with full immunity, with partial immunity and without immunity. By experimental and theoretical analysis, it is proved that the circuit's intrinsic immunity mainly stems from the components with partial immunity.

One of the most difficult jobs in designing communication and multimedia chips is to design and verify the complex complementary circuit pair (E,E-1), in which circuit E transforms information into a format suitable for transmission and storage, and its complementary circuitE-1recovers this information. In order to facilitate this job, we proposed a novel two-step approach to synthesize the complementary circuitE-1fromEautomatically. First, a SAT solver was used to check whether the input sequence ofEcan be uniquely determined by its output sequence. Second, the complementary circuitE-1was built by characterizing its Boolean function, with an efficient all-solution SAT solver based on discovering XOR gates and extracting unsatisfiable cores. To illustrate its usefulness and efficiency, we ran our algorithm on several complex encoders from industrial projects, including PCIE and 10 G Ethernet, and successfully built correct complementary circuits for them.

One of the most difficult jobs in designing communication and multimedia chips, is to design and verify complex complementary circuit pair (E, E-1), in which circuit E transforms information into a format that is suitable for transmission and storage, while E's complementary circuit E-1 recovers this information.

Decision trees have been widely used for online learning classification. Many approaches usually need large data stream to finish decision trees induction, as show notable limitations (even fail) with small data stream. In fact, there exist many real instances with small data stream. In the paper, we propose a novel incremental extremely random forest algorithm, dealing with online learning classification with small streaming data. In our method, arriving examples are stored at the leaf nodes and used to determine when to split the leaf nodes combined with Gini index, so the trees can be expanded efficiently with a few examples. Our algorithm has been applied to solve both online learning and video object tracking problems, and the results on UCI datasets and challenging video sequences demonstrate its effectiveness and robustness.

This paper describes a heterogeneous multicore SoC named EVMP-SoC, which is composed of a RISC host processor and two minor-different SIMD synergistic processor that are specially optimized for embedded visual media applications. By using on chip memory and the multi-channel memory access unit, this chip achieved several different level of parallelism, such as single-instructionstream-multiple-datastream (SIMD) data-level parallelism (DLP), multicore thread-level parallelism (TLP) and memory tile pipeline parallelism. We used an affine transformation framework called PLuTo on code optimization for EVMPSoC and explored multiple level parallelism on this chip. We found that lacking of processor performance model, the general polyhedral affine transformation framework could not generate efficient parallel code for heterogeneous architectures. Tile scheduling and pipelining techniques are adopted to make a full use of process cores and memory bandwidth. The experiment results showed that tile schedule and pipeline is effective. This chip gained a very good accelerate ratio after all the parallel optimizations. Finally, the chip was proved to be high efficiency and availability through a case study (a typical application of three dimensional reconstruction from multi images).

Consistency and responsiveness are two important factors in providing the sense of reality in Distributed Virtual Environment (DVE). However, it is not easy to optimize both aspects because of the trade-off between these two factors. As a result, most existing consistency maintenance methods ignored the responsiveness requirements, or just assumed a simple responsiveness requirement model which cannot meet the real need of DVE systems. In this paper, we first present a new responsiveness requirement model. The model can describe requirement satisfaction situation of each node. Base on this model, we propose a responsiveness requirement based consistency method. The method can adjust the utilization of time resource according to the requirements of different nodes and improve the overall responsiveness performance by at least 20%. Therefore, it provides a good support to increase the applicability of DVE systems.

The flexibility, performance and cost effectiveness of reconfigurable architectures have lead to its widespread use for embedded applications. Coarse-grained reconfigurable system design is very complex for multi-fields experts to collaborate on application algorithm design, hardware/software co-design and system decision. However, existing reconfigurable system design methods and environments can only support hardware/software co-design, ignoring the collaboration between multi-field experts. This paper presents a collaborative partition approach of coarse-grained reconfigurable system design using evolutionary ant colony optimization. We create a distributed collaborative design environment for system decision engineers, software designers, hardware designers and application algorithm developers. The method not only utilizes the advantages of ant colony optimization for searching global optimal solutions, but also provides a framework for multi-field experts to work collaboratively. Experimental results show that the method improves the quality and speed of hardware/software partition for coarse-grained reconfigurable system design.

To cope with increasingly complexity and time-to- market pressure, system-on-chip system modeling is introduced to describe system behavior at the highest abstract level. System modeling helps to separate and cooperate between the steps of system level design. This paper puts forward the application-driven system-on- chip system model extraction approach. The approach extracts application features including control/dataflow, computation/storage and critical tasks features, based on which system models are automatically generated. This approach greatly improves efficiency and correctness of system modeling because it needs not manual work. Moreover, the approach fully excavates and utilizes application features to benefit system level design.

Functional verification is widely recognized as the bottleneck of the hardware design cycle. The coverage-driven verification approach makes coverage the core engine that drives the whole verification flow, which enables reaching high quality verification in a timely manner. In this paper, we present a coverage driven test generation methodology and a set of tools. We present a novel method for automatic generating simulation vectors from HDL descriptions based on path coverage and constraint solving. We present a novel approach to generate functional vectors based on assertions for RTL design verification. Our approach combines program-slicing based design extraction, word-level SAT and dynamic searching techniques. We also present a coverage analysis method based on VCD file, which only replaying the simulation of the control statements in the HDL description. Experimental results show the efficiency of our methodology.

We introduce a novel architecture template modeling for mapping applications on coarse-grained reconfigurable SoC. System level design issues become critical with increasingly complex integrated circuits and time-to-market pressure continues relentlessly. Design reuse and early design decision for computation and communication are a "must". Our technique is based on a transaction level architecture template modeling methodology in which computation/communication co-design is performed with the architecture described in an abstract manner. Besides, we use eACOGA algorithm for hw/sw partition. eACOGA uses genetic algorithm to evolve the parameters of ant colony optimization, and makes use of such advantages as positive feedback and efficient convergence to search for optimal partition solutions. Experiments show our approach improves the quality and efficiency of hw/sw partition for reconfigurable SoC, and architecture template enhances system reuse of existing SoC design and achieves exploration speedup well.

Image and video compression is a typical data-intensive and computation-intensive application. As general processors are inefficient and power consumptive in processing such tasks, more and more novel architectures appeared. This paper first gave an overview about the media compression standards, and then introduced several novel architecture processors, such as VIRAM, DTVA, Imagine, Cell, RAW and TRIPS. Some of these processors used PIM technology, and some are based on stream processing, the others are multicore and polymorph architecture. Finally compared and analyzed the design parameters of these processors, such as the performance and power consumptions. According to the media compression features which have constraints on architectural design, we concluded some useful suggestions for media compression processor architecture designers, that include execution model, memory hierarchies, performance and dissipation, etc.

We designs and implements a system-on-chip SW/HW co-verification environment SoC-Gen, which collaborates formal verification and simulation techniques for SoC co-verification. This paper first give an overview of SoC-Gen, and then focus on the simulation based verification environment: SoC-CBSHVE, which based on componential design and integration methodology The environment adopts automatic software, hardware and simulation wrappers. Simulator adopts asynchronous parallel algorithm and bus-based communication mechanism. Five data buses support verification components simulation communication. Standard message format and unify simulation interfaces easy SoC components design and verification. Experimental results show that SoC-CBSHVE enables easy debugging, rich portability, and high verification speed, at a low cost for system-on-chip system-level software and hardware co-verification.

The flexibility, performance and cost effectiveness of reconfigurable architectures have lead to its widespread use for embedded applications. Reconfigurable SoC (system-on-a-chip) design is very complex for multi-fields experts to collaborate on application algorithm design, hardware/software co-design and system decision. However, existing reconfigurable SoC design methods and environments can only support hardware/software co-design, ignoring the collaboration between multi-field experts. This paper presents a distributed collaborative partition method of reconfigurable system design using ant colony optimization. We create a distributed collaborative design environment for multi-field experts. The communication protocol, maintenance of consistency and parallel control are discussed. The method not only utilizes the advantages of ant colony optimization for searching the global best optimized solutions, but also provides a framework for multi-field experts to work collaboratively. Experimental results show that our method effectively improves the quality and efficiency of hardware/software partition for reconfigurable system design.

For omni-directional imaging based cooperative robot vision system, panorama unrolling is an important problem. We present an eight direction symmetry reuse algorithm for this problem, principles of this algorithm are: 1) Treat the original image to be unrolled as a series of co-centric circles, and uniformly partition them into eight parts of symmetrical sector regions. 2) According to symmetry principle in spatial geometry, we construct the symmetrical transform relations pixel coordinates among these regions. So, we need compute only one region of pixel coordinate for panorama unrolling, by use of complex ray-trace coordinate mapping, while the other seven parts of regions can be determined by symmetrically reusing results from the first region, which reduces seven-eighths computational burden for ray-tracing method. Experiments indicate that, under the same precision, our algorithm improves 3.28 times of unrolling speed compared with ray-trace unrolling method. In omnidirectional video with look-up table method, the idea of eight direction symmetry reuse can also be used to reduce the look-up table size to only one-eighth of the original table.

This paper proposes a flexible, efficient and configurable motion estimation architecture. The core of this architecture is a motion estimation engine NPSPE (Nine Points Search Pattern Engine), which can support the latest efficient block-based motion estimation algorithms used by MPEG-4/H.264 encoding, such as PMVFAST and EPZS. This architecture has been designed and synthesized in SMIC 0.18um technology. The result shows it consumes only 17.5K gates, but its computing efficiency is about 15 times higher than the well-known low power FS engine including 16 PEs while its PSNR is similar to FS.

A novel specification driven and constraints solving based method to automatically generate test programs from simple to complex ones for advanced microprocessors is presented in this paper. Our microprocessor architectural automatic test program generator (MA2TG) can produce not only random test programs but also a sequence of instructions for a specific constraint by specifying a user constraints file. The proposed methodology makes three important contributions. First, it simplifies the microprocessor architecture modeling and eases adoption of architecture modification via architecture description language (ADL) specification. Second, it generates test programs for specific constraints utilizing the power of state-to-art constraints solving techniques. Finally, the number of test program for microprocessor verification and the verification time are dramatically reduced. We applied this method on DLX processor to illustrate the usefulness of our approach.

It is a hotly research topic to eliminate irrelevant variables from counterexample, to make it easier to be understood. BFL algorithm is the most effective Counterexample minimization algorithm compared to all other approaches, but its run time overhead is very large due to one call to SAT solver per candidate variable to be eliminated. So we propose a faster counterexample minimization algorithm based on refutation analysis and incremental SAT. First, for every UNSAT instance of BFL, we perform refutation analysis to extract the set of variables that lead to UNSAT, all variables not belong to this set can be eliminated simultaneously. In this way, we can eliminate many variables with only one call to SAT solver. At the same time, we employ incremental SAT approach to share learned clauses between similar instances of BFL, to prevent overlapped state space from being searched repeatedly. Theoretic analysis and experiment result shows that, our approach can be 1 to 2 orders of magnitude faster than BFL, and still retain the minimization ability of BFL.

Ant System Algorithm has the advantages of positive feedback and efficient convergence in optimal searching, but it lacks initial pheromone, which greatly limits this algorithm's searching speed. Oriented to Platform-Based Design of System-on-a-Chip, we present a hardware/software bi-partitioning algorithm based on Ant System, Algorithm with Initial Pheromone. The main ideas are: a). Reuse the partitioning result of reference design provided by Platform-Based Design method as current design's initial partitioning, which is then converted into the initial pheromone needed by Ant System Algorithm. b). Search for the optimal partitioning scheme with the Ant System Algorithm based on the initial pheromone. Our algorithm adopts system level reusing feature of Platform-Based Design method to prevent the disadvantages of Ant System Algorithm. Experiments show our algorithm improves the efficiency of Ant System Algorithm by an average of forty percent.

A Hierarchical Platform-Based Design (Hi-PBD) method is put forward for SoC system design. This method divides SoC system design flow into three levels (i.e. system model level, virtual components level and real components level) to achieve separation of function from structure and separation of computation from communication. HI-PBD defines two mapping processes (i.e. design planning and virtual-real synthesis) to go through all the three design levels. Hi-PBD supports reuse of both the three level design templates and the two mapping results, which increased reusing efficiency greatly. Besides, Hi-PBD boosts up design flexibility by means of supporting revision at all the three level and ensures the final design target satisfies performance requirements through a novel performance constraints transmission strategy. Experiments indicate Hi-PBD method improves SoC high level design efficiency by 30%-40%, and this method achieves platform template reuse ratio by 75%-90%.

With fast development of graphics hardware, the current algorithms on rendering of landscape and seascape, which are focused on precise view-frustum culling and complicated decision of level of detail (LOD), lead the CPU to be the bottleneck of system. This paper presents a new framework based on some new data structures and new rendering algorithms for navigation and rendering of very large-scale landscape and seascape. Firstly, we construct a new terrain data model, which consists of terrain tile pyramid and terrain summary pyramid. Secondly, in order to stitch the terrain tile boundaries seamlessly, the index template is introduced, and an algorithm of LOD based on "remarkability" is described in detail. Finally, Perlin noise is used to simulate the ocean surface and a framework of navigation of very large-scale scene is completed. Experimental results show that this system can satisfy the requirements of real-time navigation of large-scale landscape and seascape.

We present a multi-resolution mesh model of the ocean surface based on a straightforward terrain LOD scheme, tiled quad-tree, with that the region of ocean surface can be extended limitlessly and readily adapted for GPU acceleration. We have introduced the concept of wrapped fractal surface (WFS) for generating height field map of the ocean. Through WFS self-mapping, we can create a series of WFS and obtain the height field map at discrete times without repeating tiles. By interpolating the height map at regular intervals we can build an ocean surface continuously and dynamically. This paper also studied shallow ocean waves concerned about affects of seaboard and underwater terrain. Experimental results showed that our approach was effective and would satisfy the requirements of a realistic real-time navigation for large-scale seascape.

Embedded system is the application specific computing system that embedded in other application, to perform some special information processing functionalities. Embedded system is composed of software part (including embedded system software and application software) and hardware part (including embedded processors, memory, ASICs, IO circuit et al). In order to ensure design quality and efficiency of embedded system, it not only requires the designers to do hardware/software co-design, but also requires experts from different domains to cooperate. Existing embedded system design methods and environments mainly support hardware/software co-design, but they can't support the cooperation among experts from different domains. In this paper, we present a distributed cooperative design method for embedded system and developed the corresponding design environment, main features are: We employ mobile agent and Web service technology to establish the distributed cooperative design environment. This distributed network environment can support experts from different domains perform embedded system virtual prototyping modeling and simulation, hardware/software partitioning and performance evaluation cooperatively, this environment also supports traditional embedded system hardware/software co-design and design reusing method. Application experiment on the embedded system design of satellite navigation and positioning device indicate that, our distributed cooperative design method and design environment of embedded system improves the design quality and efficiency greatly.

A hot research topic is the elimination of irrelevant variables from a counterexample, to make it more easily understood. The BFL (brute force lifting) algorithm is the most effective counterexample minimization algorithm compared to all other approaches. But its time overhead is very large due to one call to the SAT (satisfiability) solver for each candidate variable to be eliminated. The key to reducing time overhead is to eliminate multiple variables simultaneously. Therefore, we propose a faster counterexample minimization algorithm based on refutation analysis. We perform refutation analysis on those UNSAT instances of BFL, to extract the set of variables that lead to UNSAT. All variables not belonging to this set can be eliminated simultaneously as irrelevant variables. Thus we can eliminate multiple variables with only one call to the SAT solver. Theoretical analysis and experimental results show that our algorithm can be 2 to 3 orders of magnitude faster than the existing BFL algorithm, and with only minor loss in counterexample minimization ability.

This paper presents a novel method for automatic functional vectors generation from RT-level HDL descriptions based on path coverage and constraint solving. Compared with existing method, the advantage of this method includes: 1) it avoids generating redundant constraints, which will accelerate the test generation process, 2) it solves the problem of how to propagate the internal values to the primary inputs with decision models, 3) it can handle various HDL description styles, and various styles of designs. Experimental results conduct on several practical designs show that our method can efficiently improve the functional vectors generation process. The prototype system has been applied to verify RTL description of a real 32-bits microprocessor core and complex bugs remained hidden in the RTL descriptions are detected.

A novel specification driven and constraints solving based method to automatically generate test programs from simple to complex ones for advanced microprocessors is presented in this paper. Our microprocessor architectural automatic test program generator (MA/sup 2/TG) can produce not only random test programs but also a sequence of instructions for a specific constraint by specifying a user constraints file. The proposed methodology makes three important contributions. First, it simplifies the microprocessor architecture modeling and eases adoption of architecture modification via architecture description language (ADL) specification. Second, it generates test programs for specific constraints utilizing the power of state-to-art constraints solving techniques. Finally, the number of test program for microprocessor verification and the verification time are dramatically reduced. We applied this method on DLX processor to illustrate the usefulness of our approach.

We present a novel approach to generate functional vectors based on assertions for RTL design verification. Our approach combines program-slicing based design extraction, word-level SAT and dynamic searching techniques. Through design extraction, vectors generation need only concern about the design parts related to the given assertion, thus large practical designs can be handled. Constraints Logic Programming (CLP) naturally models mixed bit-level and word-level constraints, and word-level SAT techniques solve the mixed constraints in a unified framework, which gain perfect performance. Initial states derived from dynamic simulation can dramatically accelerate the searching process of functional vectors generation. A prototype system has been built, and the experimental results on some public benchmarks and industrial circuits demonstrate the efficiency of our approach and its applicability to large practical designs.

For RTL verification, we have to separate the control and datapath parts contained in the whole design, and apply different verification techniques for different parts. This paper presents a new circuit extraction method using program slicing technique, and develops an elegant theoretical basis based on program slicing for circuit extraction from Verilog description. The technique can obtain a chaining slice for given signals of interest. Compared with related researches, the main advantages of our method include: it is fine grain; it has no HDL coding style limitation; it is precise and is capable of dealing with various Verilog constructions. The technique has been integrated with a commercial simulation environment and incorporated into a design process. The experimental results on practical designs show the significant benefits of the proposed approach.