Hybrid Fault Simulation for Synchronous Sequential Circuits
- Bernd Becker; Martin Keim; Rolf Krieger
We present a fault simulator for synchronous sequential circuits that combines the efficiency of three-valued logic simulation with the exactness of a symbolic approach. The simulator is hybrid in the sense that three different modes of operation - three-valued, symbolic and mixed - are supported. We demonstrate how an automatic switching between the modes depending on the computational resources and the properties of the circuit under test can be realized, thus trading off time/space for accuracy of the computation. Furthermore, besides the usual Single Observation Time Test Strategy (SOT) for the evaluation of the fault coverage, the simulator supports evaluation...
Timing of Multi-Gigahertz Rapid Single Flux Quantum Digital Circuits
- Kris Gaj; Eby G. Friedman; Marc; Marc J. Feldman
. Rapid Single Flux Quantum (RSFQ) logic is a digital circuit technology based on superconductors that has emerged as a possible alternative to advanced semiconductor technologies for large scale ultra-high speed, very low power digital applications. Timing of RSFQ circuits at frequencies of tens to hundreds of gigahertz is a challenging and still unresolved problem. Despite the many fundamental differences between RSFQ and semiconductor logic at the device and at the circuit level, timing of large scale digital circuits in both technologies is principally governed by the same rules and constraints. Therefore, RSFQ offers a new perspective on the timing...
Clavis: A Temporal Reasoning System for Classification of Audiovisual Sequences
- Jean Carrive; Francois Pachet; Remi Ronfard
In the context of video indexing, we present the Clavis system in which typical video sequences of television programs are represented by templates. Templates are terminological constraint networks in which video segments coming from automatic analysis tools are represented in a description logic formalism. Templates allow to express complex classes of video sequences with temporal constraints associated to a regular expression operator. Recognizing occurrences of a template in a video program is a plan recognition problem for which efficient methods have been implemented in a constraint satisfaction problem framework. The paper describes the system and illustrates its use with several...
Constraint Propagation on Multiple Domains
- Antonio J. Fernández; Antonio J. Fern'andez; Patricia M. Hill
In previous work we have presented a simple generic framework to solve constraints on any domain (finite or infinite) which has a lattice structure. The approach is based on the use of a single constraint similar to the indexicals used by constraint logic programming (CLP) over finite domains and on a particular definition of an interval lattice built from any computation domain. In this paper we...
Efficient Büchi Automata from LTL Formulae
- Fabio Somenzi; Roderick Bloem
We present an algorithm to generate small Büchi automata for LTL formulae. We describe a heuristic approach consisting of three phases: rewriting of the formula, an optimized translation procedure, and simplification of the resulting automaton. We present a translation procedure that is optimal within a certain class of translation procedures. The simplification algorithm can be used for Buchi automata in general. It reduces the number of states and transitions, as well as the number and size of the accepting sets---possibly reducing the strength of the resulting automaton. This leads to more efficient model checking of lineartime logic formulae. We compare...
Placement and Routing Tools for the Triptych FPGA
- Carl Ebeling; Larry McMurchie; Scott Hauck; Steven Burns
Field-programmable gate arrays (FPGAs) are becoming an increasingly important implementation medium for digital logic. One of the most important keys to using FPGAs effectively is a complete, automated software system for mapping onto the FPGA architecture. Unfortunately, many of the tools necessary require different techniques than traditional circuit implementation options, and these techniques are often developed specifically for only a single FPGA architecture. In this paper we describe automatic mapping tools for Triptych, an FPGA architecture with improved logic density and performance over commercial FPGAs. These tools include a simulated-annealing placement algorithm that handles the routability issues of fine-grained FPGAs,...
- Lawrence S. Moss
We present a generalization of modal logic to logical systems which are interpreted on coalgebras of functors on sets. The leading idea is that infinitary modal logic contains characterizing formulas. That is, every model-world pair is characterized up to bisimulation by an infinitary formula. The point of our generalization is to understand this on a deeper level. We do this by studying a frangment of infinitary modal logic which contains the characterizing formulas and is closed under infinitary conjunction and an operation called 4. This fragment generalizes to a wide range of coalgebraic logics. We then apply the characterization result...
Equivalence Checking of Combinational Circuits using Boolean Expression Diagrams
- Henrik Hulgaard; Poul Frederick Williams; Henrik Reif Andersen
The combinational logic-level equivalence problem is to determine whether two given combinational circuits implement the same Boolean function. This problem arises in a number of CAD applications, for example when checking the correctness of incremental design changes (performed either manually or by a design automation tool). This paper introduces a data structure called Boolean Expression Diagrams (BEDs) and two algorithms for transforming a BED into a Reduced Ordered Binary Decision Diagram (OBDD). BEDs are capable of representing any Boolean circuit in linear space and can exploit structural similarities between the two circuits that are compared. These properties make BEDs suitable...
A Comparison of PVS and Isabelle/HOL
- David Griffioen; Marieke Huisman
. There is an overwhelming number of different proof tools available and it is hard to find the right one for a particular application. Manuals usually concentrate on the strong points of a proof tool, but to make a good choice, one should also know (1) which are the weak points and (2) whether the proof tool is suited for the application in hand. This paper gives an initial impetus to a consumers' report on proof tools. The powerful higher-order logic proof tools PVS and Isabelle are compared with respect to several aspects: logic, specification language, prover, soundness, proof manager,...
Needed Narrowing in Prolog
- Sergio Antoy
We describe the implementation of needed narrowing deployed in a compiler of a functional-logic language and present a few related concepts and results. Our implementation is obtained by translating rewrite rules into Prolog source code and optionally applying a set of optimizations to this code. We benchmark the effectiveness of each individual optimization. We show that our implementation is more efficient than all other previously proposed similar implementations. We measure both execution times, as is customarily done, and memory allocation that turns out to be a significant factor. We solve equations using a semi-strict equality relation that generalizes classic strict...
Compiling Multi-Paradigm Declarative Programs into Prolog
- Sergio Antoy; Michael Hanus
This paper describes a high-level implementation of the concurrent constraint functional logic language Curry. The implementation, directed by the lazy pattern matching strategy of Curry, is obtained by transforming Curry programs into Prolog programs. Contrary to previous transformations of functional logic programs into Prolog, our implementation includes new mechanisms for both efficiently performing concurrent evaluation steps and sharing common subterms. The practical results show that our implementation is superior to previously proposed similar implementations of functional logic languages in Prolog and is competitive w.r.t. lower-level implementations of Curry in other target languages. An noteworthy advantage of our implementation is the...
Delay Uncertainty Due To On-Chip Simultaneous Switching Noise In High Performance Cmos Integrated Circuits
- Kevin T. Tang; Eby G. Friedman
On-chip parasitic inductance inherent to the power supply rails has become significant in high speed digital circuits. Therefore, current surges result in voltage fluctuations within the power distribution networks, creating delay uncertainty. On-chip simultaneous switching noise should therefore be considered when estimating the propagation delay of a CMOS logic gate in high speed synchronous CMOS integrated circuits. Analytical expressions characterizing the on-chip simultaneous switching noise voltage and the output voltage waveform of a CMOS logic gate driving both a capacitive and a resistive-capacitive load are presented in this paper. The waveform of the output voltage signal based on the analytical...
Reprogrammable Hardware for Educational Purposes
- Michael Gschwind
This paper presents a novel idea in teaching computer architecture by using programmable hardware. Current teaching models for computer architecture today are either mostly theory-only or implementation oriented. Theory-based architecture courses lack the feedback to show students the effects of their decisions. Implementation-oriented instruction emphasizes the implementation aspects, that is, very low-level implementation strategies, over CPU architecture and forces the usage of very limited CPU designs to reduce complexity. High cost and long manufacturing times are other problems associated with this approach. We propose to use field programmable gate arrays (FPGAs) to allow fast implementation of chip designs. This allows...
NS32FX161-15NS32FX161-20NS32FX164-20 NS32FX164-25NS32FV16-20NS32FV16-25 Advanced ImagingCommunication Signal Processors
- General Description The
this document applies to the NS32FV16 and the NS32FX161 as well# The NS32FX164 can perform all the computations and control functions required for a stand-alone Fax system# a PC add-in Fax#Voice#Data Modem card or a Laser#Fax system # It also meets the performance requirements to implement 14400# 9600 and 7200 bps modems complying with CCITT V#17# V#29 and V#27 standards# The NS32FV16 supports V#29 and V#27 standards as well as voice# The NS32FX161 supports V#29 and V#27 standards# The NS32FX164 provides a 16 Mbyte Linear external address space and a 16-bit external data bus# The CPU core# which is the...
Proof Systems for Structured Specifications and Their Refinements
- Michel Bidoit; Mara Victoria Cengarle; Rolf Hennicker
Reasoning about specifications is one of the fundamental activities in the process of formal program development. This ranges from proving the consequences of a specification, during the prototyping or testing phase for a requirements speci cation, to proving the correctness of refinements (or implementations) of specifications. The main proof techniques for algebraic specifications have their origin in equational Horn logic and term rewriting. These proof methods have been well studied in the case of nonstructured speci cations (see Chapters 9 and 10). For large systems of specifications built using the structuring operators of speci cation languages, relatively few proof techniques...
ATIP99.057 1999 Symposium on VLSI Technology
- No Lo Gy
: Process technology for silicon CMOS and memory (mainly DRAM, but also Flash and FeRAM) for 0.05- to 0.2-micron generations were presented at the 1999 VLSI Technology Symposium held June 1999 in Kyoto Japan, and is discussed in this report with focus on Logic and merged Logic/DRAM technologies. KEYWORDS: Conferences, Semiconductors COUNTRY: Japan REPORT CONTENTS 1. INTRODUCTION 1.1 Executive Summary 2. GATE INSULATOR (OXIDE, NITRIDE, HIGH-K) 2.1 Leakage 2.2 Reliability 2.3 High-K Isolators 2.4 Integration 3. METAL GATE 4. MOSFET DESIGN 4.1 Spacer 4.2 Source and Drain Junctions 4.3 Channel Engineering 4.4 Buried Channel PMOSFET 5. DRAM AND LOGIC PROCESS...
A Study of Provability in Defeasible Logic
- M. J. Maher; G. Antoniou; D. Billington
Defeasible logic is a logic-programming based nonmonotonic reasoning formalism which has an efficient implementation. It makes use of facts, strict rules, defeasible rules, defeaters, and a superiority relation. We clarify the proof theory of defeasible logic through an analysis of the conclusions it can draw. Using it, we show that defeaters do not add to the expressiveness of defeasible logic, among other results. The analysis also supports the restriction of defeasible logic to admit only acyclic superiority relations.
Security Protocol for IEEE 802.11 Wireless Local Area Network
- Se Hyun Park; Aura Ganz; Zvi Ganz
As Wireless Local Area Networks #WLANs# are rapidly deployed to expand the #eld of wireless products, the provision of authentication and privacy of the information transfer will be mandatory. These functions need to takeinto account the inherent limitations of the WLAN medium such as limited bandwidth, noisy wireless channel and limited computational power. Moreover, some of the IEEE 802.11 WLAN characteristics such as the use of a point coordinator and the polling based Point Coordination Function #PCF# have also to be considered in this design. In this paper, weintroduce a security protocol for the IEEE 802.11 PCF that provides privacy...
A Representation of the Zoo World in the Language of the Causal Calculator
- Joohyung Lee; Vladimir Lifschitz; Hudson Turner
The Zoo World is an action domain proposed by Erik Sandewall as part of his Logic Modelling Workshop. We show how to represent this domain in the input language of the Causal Calculator.
A Distributed System for Solving Equational Constraints Based on Lazy Narrowing Calculi
- Mircea Marin; Tetsuo Ida; Wolfgang Schreiner
In this paper we describe the architecture and implementation of a system that aims at extending in a consistent way a functional logic programming language with solving techniques of various constraint solving systems. The system is called CFLP (Constrained Functional Logic Programming language), and consists of a lazy functional logic interpreter extended in two directions: the possibility to specify constraints, and the possibility to specify AND- and OR-parallelism. For solving the constraints, a distributed constraint solving system was implemented.