Browsing by Author "Han, Jungang"

Now showing 1 - 2 of 2
  • Thumbnail Image
    ItemOpen Access
    THE IMPLEMENTATION AND VERIFICATION OF A CONDITIONAL SUM ADDER
    (1988-07-01) Han, Jungang; Stone, Glen
    In this paper we first formulate the Conditional Sum Addition (CSA) algorithm, then design an area-time efficient Conditional Sum Adder in CMOS. We also design a Binary Look-ahead Carry adder and a fast ripple carry adder in the same technology for the comparison of their performances. Finally we formally prove that the CMOS implementation of the CSA adder is correct (i.e. the implementation meets the specification of the intended behavior) by using Mike Gordon's Higher Order Logic (HOL) system.
  • Thumbnail Image
    ItemOpen Access
    IMPLEMENTING TEMPORAL LOGIC IN HOL AND APPLICATIONS
    (1988-07-01) Han, Jungang
    Higher-Order Logic (HOL) system has been proved to be very powerful for hardware verification. Many of the largest proofs completed to date have been constructed using HOL system. It seems to be that the HOL system is more suitable for dealing with static object though we can define functions with parameter of time for handling dynamic objects in HOL system. On the other hand, Temporal logic which includes time in its semantics has the potential of handling timing problems. In order to mechanize the deducing process of temporal logic and explore the possibilities of applying temporal logic to hardware verification, we have tried to implement the linear timing temporal logic on the top level of HOL system by expressing the temporal logic concepts in high-order logic and proving the axioms and inference rules of a formal temporal logic system. This paper describes the ideas and results of this work, and gives some examples of applying temporal logic to hardware specification and verification. We have proved that there exists a static hazard in the combinational circuit considered under certain conditions, and the hazard is eliminated in the improved circuit. We have also specified and verified the properties of a S-R latch by the combined power of temporal logic and HOL system.