嵌入式协处理器中除法和平方根计算的整合设计

在浮点处理元中串行实现除法和平方根计算虽然速度慢,但设计简单规则,占用资源少,有利于嵌入式的应用。结合嵌入式协处理器LSC87的研制,给出了串行实现除法和平方根计算的基4SRT算法,介绍了确定SRT选择常数过程中不确定区域的验证方法;给出了除法与平方根计算可共用的基4SRT查询表设计;同时讨论了迭代冗余结果向非冗余二进制的转换。本协处理器设计量大限度 地利用了通用数据路径来完成SRT算法的实现,节约了设计资源,并缩短了迭代时间。     

Uppaal到PVS的时间自动机翻译器

Uppaal是一种对实时系统模型进行建模和验证的工具,PVS（Prototype Verification System）是开发和分析形式化规格说明的原型证明系统。介绍了Uppaal2PVS翻译器的设计与实现,给出了一种将用Uppaal生成的时间自动机规格说明翻译成PVS文件的方法,从而将模型检查问题转换成了定理证明问题,解决了潜在的状态空间爆炸问题。最后给出了一个实例。     

Translation of IEC 61131-3 Function Block Diagrams to PVS for Formal Verification with Real-Time Nuclear Application

The trip computers for the two reactor shutdown systems of the Ontario Power Generation (OPG) Darlington Nuclear Power Generating Station are being refurbished due to hardware obsolescence. For one of the systems, the general purpose computer originally used is being replaced by a programmable logic controller (PLC). The trip computer application software has been rewritten using function block diagrams (FBDs), a commonly used PLC programming language defined in the IEC 61131-3 standard. The replacement project’s quality assurance program requires that formal verification be performed to compare the FBDs against a formal software requirements specification written using tabular expressions (TEs). The PVS theorem proving tool is used in formal verification. Custom tools developed for OPG are used to translate TEs and FBDs into PVS code. In this paper, we present a method to rigorously translate the graphical FBD language to a mathematical model in PVS using an abstract syntax to represent the FBD constructs. We use an example from the replacement project to demonstrate the use of the model to translate a FBD module into a PVS specification. We then extend that example to demonstrate the method’s applicability to a Simulink-based design.     

定理证明辅助工具PVS剖析

ＰＶ查斯坦福机构开发的强大的规约。验证系统,它的适用领域广泛,在概要介绍ＰＶＳ的构成。功能后,着重分析了ＰＶＳ的规约语言,验证系统的特点,以及使得ＰＶＳ灵活,强大的设计决策和内在机制。     

Polynomial function intervals for floating-point software verification

The focus of our work is the verification of tight functional properties of numerical programs, such as showing that a floating-point implementation of Riemann integration computes a close approximation of the exact integral. Programmers and engineers writing such programs will benefit from verification tools that support an expressive specification language and that are highly automated. Our work provides a new method for verification of numerical software, supporting a substantially more expressive language for specifications than other publicly available automated tools. The additional expressivity in the specification language is provided by two constructs. First, the specification can feature inclusions between interval arithmetic expressions. Second, the integral operator from classical analysis can be used in the specifications, where the integration bounds can be arbitrary expressions over real variables. To support our claim of expressivity, we outline the verification of four example programs, including the integration example mentioned earlier. A key component of our method is an algorithm for proving numerical theorems. This algorithm is based on automatic polynomial approximation of non-linear real and real-interval functions defined by expressions. The PolyPaver tool is our implementation of the algorithm and its source code is publicly available. In this paper we report on experiments using PolyPaver that indicate that the additional expressivity does not come at a performance cost when comparing with other publicly available state-of-the-art provers. We also include a scalability study that explores the limits of PolyPaver in proving tight functional specifications of progressively larger randomly generated programs.     

Verification and synthesis of addition programs under the rules of correctness of statements

Deductive verification and synthesis of binary addition programs are carried out on the base of the rules of proving the correctness for statements of the predicate programming language P. The paper presents key fragments of verification and synthesis of the programs for the Ripple carry, Carry look-ahead and Ling adders. The correctness conditions of the programs were translated into the specification language of the PVS verification system. The proof is found to be a tedious procedure as compared with the ordinary programming. However, for program synthesis, the development of theories and proofs on PVS are easier and faster than for program verification.     

Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods

Formal specification combined with mechanical verification is a promising approach for achieving the extremely high levels of assurance required of safety-critical digital systems. However, many questions remain regarding their use in practice: Can these techniques scale up to industrial systems, where are they likely to be useful, and how should industry go about incorporating them into practice? This paper discusses a project undertaken to answer some of these questions, the formal verification of the microcode in the AAMP5 microprocessor. This project consisted of formally specifying in the PVS language a Rockwell proprietary microprocessor at both the instruction-set and register-transfer levels and using the PVS theorem prover to show the microcode correctly implemented the instruction-level specification for a representative subset of instructions. Notable aspects of this project include the use of a formal specification language by practicing hardware and software engineers, the integration of traditional inspections with formal specifications, and the use of a mechanical theorem prover to verify a portion of a commercial, pipelined microprocessor that was not explicitly designed for formal verification.     

Formal Verification of the <Emphasis Type="Italic">VAMP</Emphasis> Floating Point Unit

We report on the formal verification of the floating point unit used in the VAMP processor. The dual-precision FPU is IEEE compliant and supports denormals and exceptions in hardware. The supported operations are addition, subtraction, multiplication, division, comparison, and conversions.We have formalized the IEEE standard 754. The formalization is supplemented by a rich theory of rounding, which includes notations and theorems facilitating the verification of the actual hardware. The theory of rounding enables the separation of the hardware into smaller modules which can be verified individually. Each module is verified on the gate level against a formal specification. The combination of these formal specifications, together with the theorems from the theory of rounding, yield the overall correctness of the FPU, i.e., theorems stating that the gate-level hardware complies with the high-level formalization of the IEEE standard. The verification is done completely in the theorem prover PVS.We further report on the implementation and test of the verified FPU on a Xilinx FPGA.     

Hierarchical program specification and verification — a many-sorted logical approach

Summary The notion of abstractions in programming is characterized by the distinction between specification and implementation. As far as the specification structures are concerned, hierarchical program development with abstraction mechanisms is naturally regarded as a process of theory extensions in a many-sorted logic. To support such program development, a language called t is proposed with which one can structuredly build up theories and write their program implementation. There, the implementation is regarded as another level of theory extension, and the relation between the specification and the implementation of an abstraction is characterized in terms of a homomorphism between the two theories. On this formalism, a mechanizable proof method is introduced for validation of implementations of both data and procedural abstraction. Finally, a new data type concept is introduced to generalize the so-called type-parametrization mechanism. A justification of this concept within the first order logic is provided as well as its applications to program structuring and verification.     

Theorem prover approach to semistructured data design

The wide adoption of semistructured data has created a growing need for effective ways to ensure the correctness of its organization. One effective way to achieve this goal is through formal specification and automated verification. This paper presents a theorem proving approach towards verifying that a particular design or organization of semistructured data is correct. We formally specify the semantics of the Object Relationship Attribute data model for Semistructured Data (ORA-SS) modeling notation and its correctness criteria for semistructured data normalization using the Prototype Verification System (PVS). The result is that effective verification on semistructured data models and their normalization can be carried out using the PVS theorem prover.     

NRS FPU中浮点乘、除运算的合并设计

ＮＲＳ ＦＰＵ是西北工业大学航空微电子中心研制的具有自主版权的协处理器,文中面向嵌入式应用描述了ＮＲＳ ＦＰＵ通用路径下浮点乘、除的合并设计。主要讨论了迭代计数器、除索引奇存器与乘数寄存器的合用、ＢＯＯＴＨ译码逻辑与除法的查找表结合、以及数据缩放与移位部件的共用。并结合具体实现,对浮点除算法中实现较复杂的商位产生算法进行了改进。与其它几种常见的处理器比较显示,ＮＲＳ ＦＰＵ规模小,速度高,是嵌入式     

Functional dependencies of C functions via weakest pre-conditions

We present functional dependencies, a convenient, formal, but high-level, specification format for a piece of procedural software (function). Functional dependencies specify the set of memory locations, which may be modified by the function, and for each modified location, the set of memory locations that influence its final value. Verifying that a function respects pre-defined functional dependencies can be tricky: the embedded world uses C and Ada, which have arrays and pointers. Existing systems we know of that manipulate functional dependencies, Caveat and SPARK, are restricted to pointer-free subsets of these languages. This article deals with the functional dependencies in a programming language with full aliasing. We show how to use a weakest pre-condition calculus to generate a verification condition for pre-existing functional dependencies requirements. This verification condition can then be checked using automated theorem provers or proof assistants. With our approach, it is possible to verify the specification as it was written beforehand. We assume little about the implementation of the verification condition generator itself. Our study takes place inside the C analysis framework Frama-C, where an experimental implementation of the technique described here has been implemented on top of the WP plug-in in the development version of the tool.     

基于正弦数据压缩算法的DDS研究及FPGA实现

针对直接数字频率合成器（DDS）芯片因存储空间开销大导致功耗增加,可靠性降低的问题 ,设计了一种将改进sunderland算法与QE-ROM技术相结合的一种用于直接数字频率合成器（DDS）的紧凑型16位精度正弦查找表(ROM);对所设计的正弦查表算法进行了系统级仿真与硬件描述语言（Verilog HDL)实现,并最终在FPGA上进行了整体算法功能与性能的验证;基于AD5360芯片制作了一款多通道16位输出数模转换器(DAC),并搭载降压稳压芯片LM317和LM337实现了一款可以将220V工频转换为DAC所需的±9V和3.75V的供电电源。测试结果显示,设计的正弦查找表算法在达到16位精度的同时,只占据8576bit的存储空间。所使用的正弦数据优化算法相比较传统的DDS正弦波形发生器资源节省99.2%,实现了122：1的压缩比,有效降低了DDS的芯片面积和功耗;     

Proof assistance for real-time systems using an interactive theorem prover

This paper discusses the adaptation of the PVS theorem prover for performing analysis of real-time systems written in the ASTRAL formal specification language. Several issues arose during the encoding of ASTRAL that are relevant to the encoding of many real-time specification languages such as encoding formulas as types, handling partial functions, dealing with noninterleaved concurrency, and defining irregular operators. These issues and possible solutions are presented as well as how they were handled in the ASTRAL encoding. A translator was written that translates any ASTRAL specification into its corresponding PVS encoding. After performing the proofs of several systems using their translations, PVS strategies were developed to automate the proofs of certain types of properties. In particular, strategies are presented for fully automating the proofs of certain classes of untimed properties. In addition, strategies were developed for partially automating the derivation of timed executions using transition steps. The encoding was used as the basis for a fully automated transition sequence generator tool, which has a wide variety of applications.     

Formal requirements analysis of an avionics control system

The authors report on a formal requirements analysis experiment involving an avionics control system. They describe a method for specifying and verifying real-time systems with PVS. The experiment involves the formalization of the functional and safety requirements of the avionics system as well as its multilevel verification. First level verification demonstrates the consistency of the specifications whilst the second level shows that certain system safety properties are satisfied by the specification. They critically analyze methodological issues of large scale verification and propose some practical ways of structuring verification activities for optimizing the benefits     

Optimum RNS sign detection algorithm using MRC-II with special moduli set

In this paper, we present a generic sign detection algorithm based on mixed radix conversion algorithm, MRC-II [M. Akkal, P. Siy, A new mixed radix conversion algorithm MRC-II, Journal of System Architecture (2006)] and also we present an optimum algorithm for sign detection based on a special moduli set where m_n is even. The described algorithm requires only one comparison for sign detection. A new moduli set will also be presented which simplifies MRC-II conversion algorithm by eliminating the need for table lookup normally used in MRC hardware implementation. The algorithm does not require ROM table like other algorithms. For a moduli set of four moduli that satisfies the special moduli set conditions, 0 tables are needed to do the conversion, while Szabo and Tanaka MRC algorithm [N.S. Szabo, R.I. Tanaka, Residue Arithmetic and Its Application to Computer Technology, McGraw-Hill, New York, 1967] requires 6 tables with a total table size of 4608 bits; and Huang MRC algorithm [C.H. Huang, A fully ParallelMixed-radix conversion algorithm for residue number applications, IEEE Transactions on Computers c-32 (4) (1983)] requires 10 tables with a total table size of 3840 bits.     

Model-Based Verification and Validation of Properties

One of the key issues in software development, like in all engineering problems, is to ensure that the product delivered meets its specification. Verification and validation are well-established techniques for ensuring the quality of a product within the overall software development lifecycle. With models being expressed in the Unified Modeling Language, the application of verification and validation is complicated. Firstly, concerning verification, a UML model is typically not the input language of a verification tool. Secondly, with regards to validation, a UML model is also not directly executable.In this paper, we show how verification and validation can be achieved for UML models. Within our approach, graph transformation techniques are applied for automated translation of UML models into a language understood by a verification tool or directly into an implementation. By the use of such semantic-preserving transformations, both verification and validation can be lifted up to the model level, allowing for a seamless integration of verification and validation into a UML-based development process.     

Combining formal verification and conformance testing for validating reactive systems

This paper presents a combination of verification and conformance testing techniques to support the formal validation of reactive systems. The idea is to use symbolic test selection techniques to extract subgraphs (components) from a specification, and to perform the verification on the components rather than on the whole specification. Under reasonable sufficient conditions, this constitutes a sound compositional verification technique, in the sense that a property verified on the components also holds on the whole specification. This may considerably reduce the global verification effort. Moreover, once verified, a component forms the basis of an adequate test case, i.e. when executed on an implementation, it will not issue false positive or negative verdicts with respect to the verified properties. The approach has been implemented using the STG test selection tool and the PVS theorem prover. It is demonstrated here on a smart‐card application: the Common Electronic Purse System. Copyright © 2003 John Wiley & Sons, Ltd.