Lingcore Laboratory

Portland, OR, United States

Lingcore Laboratory

Portland, OR, United States
SEARCH FILTERS
Time filter
Source Type

Liu F.,National Laboratory of Parallel Distributed Processing | Tan Q.,National Laboratory of Parallel Distributed Processing | Chen G.,Lingcore Laboratory | Song X.,Portland State University | And 2 more authors.
IET Computers and Digital Techniques | Year: 2010

As an important part of many processors's floating point unit, fused multiply-add unit performs a multiplication followed immediately by an addition. In IBM POWER6 microprocessor's fused multiply-add unit, a fast 128-bit floating-point end-around-carry (EAC) adder is proposed. Very few algorithmic details exist in today's literature about this adder. In this study, a complete designed EAC adder that can work independently as a regular adder is proposed. Details about the proposed EAC adder's arithmetic algorithms are described. In IBM's original EAC adder, the Kogge-Stone tree has been chosen for its high performance on ASIC technology. In this study, the authors present a comparative study on different parallel prefix trees which are used in the design of our new EAC adder targeting field programmable gate array (FPGA) technology. Our study highlights the main performance differences among 14 different architecture configurations focusing on the area requirements and the critical path delay. The experimental results show that there is one architecture configuration with the lower area requirement and the higher performance. © 2010 © The Institution of Engineering and Technology.


Wan H.,Tsinghua University | Chen G.,Lingcore Laboratory | Song X.,Portland State University | Gu M.,Tsinghua University
IET Software | Year: 2011

Programmable logic controllers (PLCs) are widely used in embedded systems. Timers play a pivotal role in PLC real-time applications. The formalisation of timers is of great importance. The study presents a formalisation of PLC timers in the theorem proving system Coq, in which the behaviours of timers are characterised by a set of axioms at an abstract level. The authors discuss how to model timers at a proper and sound abstract level. PLC programs with timers are modelled. As a case study, a quiz machine problem with a timer is investigated. This work demonstrates the complexity of formal timer modelling. © 2011 The Institution of Engineering and Technology.


Wan H.,Tsinghua University | Song X.,Portland State University | Chen G.,Lingcore Laboratory | Gu M.,Tsinghua University
Proceedings - International Conference on Quality Software | Year: 2010

Programmable logic controllers (PLCs) are widely used in computer-based industrial applications. Timers play a pivotal role in PLC real-time embedded system applications. The paper addresses the formal validation of PLC systems with timers in the theorem proving system Coq. The timer behavior is characterized formally. A refinement validation methodology is presented in terms of an abstract model and a concrete model. The refinement is calibrated by a mapping relation. The soundness of the methodology is shown in the proving system. An illustrative case study demonstrates the effectiveness of the approach. © 2010 IEEE.


Liu F.,National University of Defense Technology | Song X.,Portland State University | Tan Q.,National University of Defense Technology | Chen G.,Lingcore Laboratory
Computer Journal | Year: 2011

Arithmetic circuits play an important role in high-performance digital systems. The paper considers a generic architecture of hybrid prefix/carry-select arithmetic systems. A novel proof methodology is proposed to model and verify hybrid addition systems. Algebraic structures and first-order recursive equations are harnessed in proof derivations. Case studies on several typical classes of hybrid prefix/carry-select adders and special cases with pseudo-carries such as Ling's carry demonstrate the effectiveness of the proposed approach. © 2010 The Author Published by Oxford University Press on behalf of The British Computer Society. All rights reserved.


Liu F.,National University of Defense Technology | Song X.,Portland State University | Tan Q.,National University of Defense Technology | Chen G.,Lingcore Laboratory
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems | Year: 2010

End-around-carry (EAC) adder is extensively used in microprocessor's floating-point units. This paper presents an algebraic characterization of an EAC adder's algorithm. A novel symbolic analysis approach is presented to prove the EAC adder's correctness. Algebraic structures and first-order recursive equations are harnessed in proof derivations. A hybrid prefix/EAC architecture is considered. © 2006 IEEE.


Chen G.,Lingcore Laboratory | Liu F.,National Laboratory of Parallel Distributed Processing
IEEE Transactions on Computers | Year: 2010

Adder circuits have been extensively studied. Their formal properties are well known, but the proofs are either incomplete or difficult to find. This short contribution intends to integrate all formal proofs related to adders in a single place and to add the details when necessary. The presentation is accessible to general VLSI designer. Another goal of this study is to put together relevant materials for the preparation of further formal studies in computer arithmetic. The presentation is made as concise as possible. © 2006 IEEE.


Liu F.,National Laboratory of Parallel Distributed Processing | Tan Q.,National Laboratory of Parallel Distributed Processing | Chen G.,Lingcore Laboratory
Mathematical and Computer Modelling | Year: 2010

The paper presents an algebraic analysis for the correctness of prefix-based adders. In contrast to using higher-order functions and rewriting systems previously, we harness first-order recursive equations for correctness proof. A new carry operator is defined in terms of a semi-group with the set of binary bits. Both sequential and parallel addition algorithms are formalized and analyzed. The formal analysis on some special prefix adder circuits demonstrates the effectiveness of our algebraic approach. This study lays an underpinning for further understanding on computer arithmetic systems. © 2010 Elsevier Ltd.


Liu F.,National Laboratory of Parallel Distributed Processing | Tan Q.,National Laboratory of Parallel Distributed Processing | Song X.,Portland State University | Chen G.,Lingcore Laboratory
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Year: 2010

In this paper, we present a general architecture of hybrid prefix/carry-select adder. Based on this architecture, we formalize the hybrid adder's algorithm using the first-order recursive equations and develop a proof framework to prove its correctness. Since several previous adders in the literature are special cases of this general architecture, our methodology can be used to prove the correctness of different hybrid prefix/carry-select adders. The formal proof for a special hybrid prefix/carry-select adder shows the effectiveness of the algebraic structures built in this paper. © Springer-Verlag Berlin Heidelberg 2010.


Chen G.,Lingcore Laboratory
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems | Year: 2010

This paper describes a new advancement in theorem proving based formal verification: a formalization of a parameterized parallel prefix adder developed in the proof assistant Coq. © 2010 IEEE.

Loading Lingcore Laboratory collaborators
Loading Lingcore Laboratory collaborators