检索结果-内蒙古大学图书馆

Mechanizing verification of arithmetic circuits: SRT division 17th

17th Conference on Foundations of Software Technology and Theoretical computer science, FSTTCS 1997

作者： Kapur, Deepak Subramaniam, M. Computer Science Department State University of New York AlbanyNY12222 United States Functional Verification Group Silicon Graphics Inc. Mountain ViewCA94040 United States

ISBN: (纸本)3540638768

The use of a rewrite-based theorem prover for verifying properties of arithmetic circuits is discussed. A prover such as Rewrite Rule Laboratory (RRL) can be used effectively for establishing numbertheoretic properties of adders, multipliers and dividers. Since verification of adders and multipliers has been discussed elsewhere in earlier papers, the focus in this paper is on a divider circuit. An SRT division circuit similar to the one used in the Intel Pentium processor is mechanically verified using RRL. The number-theoretic correctness of the division circuit is established from its equational specification. The proof is generated automatically, and follows easily using the inference procedures for contextual rewriting and a decision procedure for the quantifier-free theory of numbers (Presburger arithmetic) already implemented in RRL. Additional enhancements to rewrite-based provers such as RRL that would further facilitate verifying properties of circuits with structure similar to that of the SRT division circuit are discussed. © 1997, Springer Verlag.

关键词： Adders

来源：评论

学校读者我要写书评

暂无评论

Virtual hand interactions with 3D world 4

Virtual hand interactions with 3D world

引用

4th International Conference on Multi-Media Modeling, MMM 1997

作者： Moccozet, L. Huang, Z. Magnenat Thalmann, N. Thalmann, D. MIRALab-CUI University of Geneva 24 Rue Géńral Dufour Geneva 4CH 1211 Switzerland Computer Graphics Laboratory Swiss Federal Institute of Technology LausanneCH 1015 Switzerland Department of Information Systems and Computer Science National University of Singapore Singapore119260 Singapore

ISBN: (纸本)9810233515

Interactions between a virtual actor and its virtual environment involve many aspects. An important one is hands interactions. In a virtual scene depicting everyday life, the actor will need to grasp and hold objects, in such a way that both skeleton motion and body deformation have a realistic visual aspect. It will also need to interact with other virtual actors sharing the same virtual world, shaking hands when meeting for example. We present an efficient and realistic method combining automatic hand motion generation with hand deformation simulation. The resulting system is integrated in an interactive human simulation application. It adds the ability to simulate hand interactions between actors and their environment, in combination with traditional human animation techniques. The skeleton is animated by a heuristic motion control and multi-sensor based technique. The final free-form surface hand model is produced by a three-layer deformation model. The intermediate muscular layer is based on a geometric deformation tool, where deformations are coasidered as interpolating control points displacements. © Multimedia Modeling, MMM 1997 - Modeling Multimedia Information and Systems. All rights reserved.

关键词： Deformation

来源：评论

学校读者我要写书评

暂无评论

Geodesic Voronoi diagrams on parametric surfaces

Geodesic Voronoi diagrams on parametric surfaces

引用

computer graphics International

作者： R. Kunze F.-E. Wolter T. Rausch Welfen Laboratory-Division of Computer Graphics and Geometric Modelling Institute of Computer Science Department of Mathematics University of Hannover Hanover Germany

In this paper we extend the concept of Voronoi diagrams to parameterized surfaces where distance between two points is defined as infimum over the lengths of surface paths connecting these points. We present a method ... 详细信息

关键词： Joining processes Mesh generation Geophysics computing Laboratories computer graphics Solid modeling Mathematical model computer science Mathematics Data structures

来源：评论

学校读者我要写书评

暂无评论

Merging of galaxies with central black holes .2. Evolution of the black hole binary and the structure of the core

引用

ASTROPHYSICAL JOURNAL 1997年第1期478卷 58-65页

作者： Makino, J Department of Graphics and Computer Science College of Arts and Sciences University of Tokyo 3-8-1 Komaba Meguro-ku Tokyo 153 Japan

We investigated the evolution of the black hole binary formed by the merging of two galaxies, each containing a central massive black hole. Our main goal here is to determine if the black hole binary can merge through the hardening by dynamical friction and the gravitational wave radiation. We performed N-body simulations of the merging of two galaxies with a wide range of the total number of particles to investigate the effect of the number of particles on the evolution of the black hole binary, We found that the evolution timescale was independent of the number of particles in the galaxy N until the semimajor axis reached a critical value. After the semimajor axis became smaller than this critical value, the evolution timescale was longer for larger numbers of particles. Qualitatively, this behavior is understood naturally as the result of the ''loss cone'' effect. However, the dependence of the timescale on N is noticeably weaker than the theoretical prediction. In addition, the critical semimajor axis is smaller than the theoretical prediction. The timescale of evolution through gravitational radiation at this critical semimajor axis is longer than the Hubble time. We discuss the reason of this discrepancy and the implication of the present result on the structure of the elliptical galaxies and QSO activities.

关键词： black hole physics galaxies, active galaxies, interactions galaxies, nuclei methods, numerical

来源：评论

学校读者我要写书评

暂无评论

Building interactive animations using VRML and Java

Building interactive animations using VRML and Java

引用

Brazilian Symposium on computer graphics and Image Processing (SIBGRAPI)

作者： F.S. Tamiosso A.B. Raposo L.P. Magalhaes I.L.M. Ricarte Department of Computer Engineering and Industrial Automation State University of Campinas Sao Paulo Brazil Department-Computer Graphics Laboratory Computer Science University of Waterloo Waterloo ONT Canada

The paper exploits the combination of VRML (Virtual Reality Modeling Language) and Java for the construction of highly interactive animations, whose behaviour is defined in real time by a user's actions. The animations are modeled in VRML, which allows the definition of a Java program to process and generate events that determine the behaviour of scene elements. An application for the generation of Java graphical interfaces was developed, aiming to establish the communication between the user and the VRML environment, sending parameters to the program that controls the animation.

关键词： Animation Java Object oriented modeling Layout computer industry Automation computer science computer graphics Virtual reality Power generation

来源：评论

学校读者我要写书评

暂无评论

A practitioners' assessment of light reflection models

A practitioners' assessment of light reflection models

引用

Pacific Conference on computer graphics and Applications

作者： P. Shirley B. Smits H. Hu E. Lafortune Computer Science Department University of Utah Salt Lake UT USA Program of Computer Graphics Cornell University Ithaca NY USA

We discuss the theory and practical issues behind creating reflection models to show the difficulty of the problem. We survey the current approaches towards reflection models for computer graphics to show that even for simple surfaces, the important issues are far from settled. We briefly discuss future directions for research. Finally, we present a case study of a particular type of light reflection that captures some important aspects of appearance for a limited class of materials with subsurface reflection.

关键词： Optical reflection Optical polarization Rough surfaces Surface roughness computer science Cities and towns Image generation Layout computer graphics Optical scattering

来源：评论

学校读者我要写书评

暂无评论

Working with remote VRML scenes through low-bandwidth connections

Working with remote VRML scenes through low-bandwidth connec...

引用

Brazilian Symposium on computer graphics and Image Processing (SIBGRAPI)

作者： A.B. Raposo L.P. Magalhaes I.L.M. Ricarte School of Electrical and Computer Engineering FEEC Department of Computer Engineering and Industrial Automation State University of Campinas Sao Paulo Brazil Computer Science Department Computer Graphics Laboratory University of Waterloo Waterloo ONT Canada

We have developed a Web based application to accelerate the visualization of VRML scenes located in a remote server. This application enables the user to extract only the parts of a scene that are of actual interest. The extracted parts represent one or more sub trees of the hierarchical structure of the VRML scene, and only these parts will be rendered and visualized in the local computer. By reducing the complexity (size) of the remote scene, less data are transmitted from the remote server and the rendering process becomes faster in the local computer. The application is written in Java and is executed as an applet embedded in an HTML page.

关键词： Layout Java World Wide Web Application software Tactile sensors Acceleration Data visualization HTML graphics Animation

来源：评论

学校读者我要写书评

暂无评论

Image plane interaction techniques in 3D immersive environments 97

Image plane interaction techniques in 3D immersive environme...

引用

Proceedings of the 1997 symposium on Interactive 3D graphics

作者： Jeffrey S. Pierce Andrew S. Forsberg Matthew J. Conway Seung Hong Robert C. Zeleznik Mark R. Mine Department of Computer Science University of Virginia Charlottesville VA Brown University site of the NSF Science and Technology Center for Computer Graphics and Scientific Visualization Providence RI Department of Computer Science University of North Carolina Chapel Hill NC

来源：评论

学校读者我要写书评

暂无评论

An adaptive multi-resolution modeling technique based on viewing and animation parameters

An adaptive multi-resolution modeling technique based on vie...

引用

IEEE Annual International Symposium Virtual Reality

作者： R.W.H. Lau D.S.P. To M. Green Computer Graphics and Media Laboratory Department of Computing Hong Kong Polytechnic University Hong Kong China Department of Computer Science University of Alberta AB Canada

Because most existing multi resolution methods are slow, a common approach is to pregenerate a few key models of the object at different resolutions. During run time, the object's distance from the viewer determines which model to use for rendering. Although this approach is simple, it suffers from the sudden change in resolution as the object moves across the threshold distance. In addition, the model used to represent an object at a particular frame is not optimized for the given dynamic viewing and animation parameters. The quadtree type of methods for arranging the surface model may allow adaptive multi resolution modeling in a simple way and it reduces the sudden change of resolution from the object level to the node level. However, the square shape of the node, together with the four-time increment in size for representing surfaces, limits the types of surfaces that it can handle without creating excessive nodes. We present a real time adaptive multi resolution method for models of arbitrary topology.

关键词： Animation Page description languages Runtime Topology computer graphics Laboratories computer science Shape Rendering (computer graphics) Optimization methods

来源：评论

学校读者我要写书评

暂无评论

Timing-driven placement for regular architectures

引用

IEEE Transactions on computer-Aided Design of Integrated Circuits and Systems 1997年第6期16卷 597-608页

作者： A. Mathur C.L. Liu Silicon Graphics Inc. Mountain View CA USA Department of Computer Science University of Illinois Urbana-Champaign Urbana IL USA

We present a new iterative algorithm for timing-driven placement applicable to regular architectures such as field-programmable gate arrays (FPGAs). Our algorithm has two phases in each iteration: a compression phase and a relaxation phase. We employ a novel compression strategy based on the longest path tree of a cone for improving the timing performance of a given placement. Compression might cause a feasible placement to become infeasible. The concept of a slack neighborhood graph is introduced, and is used in the relaxation phase to transform an infeasible placement into a feasible one using a mincost maxflow formulation. The slack neighborhood graph approach used in the relaxation phase guarantees a bounded increase in delay during the relaxation phase. Our analytical results regarding the bounds on delay increase during relaxation are validated by the rapid convergence of our algorithm on benchmark circuits, We obtain placements that have 13% less critical path delay (on the average) than those generated by the Xilinx automatic place and route tool (apr) on technology-mapped MCNC benchmark circuits. The running time of our algorithm is significantly less than that of apr. Slack neighborhood graphs are of independent interest because they can also be used for timing-driven reconfiguration for yield enhancement and for handling incremental design changes efficiently.

关键词： Delay Timing Iterative algorithms Tree graphs Algorithm design and analysis Integrated circuit yield Very large scale integration Integrated circuit technology Integrated circuit interconnections Electronics industry

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：