Using Wired for Design Exploration (2009)
Emil Axelsson, Koen Claessen, Mary Sheeran
Lava has been used successfully in structural circuit description and layout generation for FPGAs [2]. It has been demonstrated that Lava is suitable for describing so-called “clever ” or...
Exposed Datapath for Efficient Computing (2008)
Magnus Björk, Magnus Själander, Lars Svensson, Martin Thuresson, John Hughes, Jonas Karlsson, ...
Abstract — We introduce FlexCore, which is the first exemplar of a processor based on the FlexSoC processor paradigm. The FlexCore utilizes an exposed datapath for increased performance. Manually...
FlexSoC: Combining Flexibility and Efficiency in SoC Designs (2008)
John Hughes, Per Larsson-edefors, Mary Sheeran, Per Stenström, Lars “j. Svensson
The FlexSoC project aims at developing a design framework that makes it possible to combine the computational speed and energy-efficiency of specialized hardware accelerators with the flexibility of...
Hardware Description and Verication Lava Exam, due midnight May 21, 2004 (2007)
The purpose of this take-home exam is to give you further practice in writing Lava denitions of recursive circuits. You will also gain experience of doing analysis of non-functional properties (like...
The Design and Veri cation of a Sorter Core (2007)
Koen Claessen, Mary Sheeran, Satnam Singh
Abstract. The design and veri cation of a high speed sorter core is presented. We present several techniques and tools used to verify the functionality of the sorter. The sorter is a periodic sorter...
Wired - a Language for Describing Non-Functional (2007)
Properties Of Digital, Emil Axelsson, Koen Claessen, Mary Sheeran
Increasingly, designers need to estimate non-functional properties such as area, power consumption and timing, even when working at a high level of abstraction, early in the design. In deep...
Designing Correct Circuits. (2006)
Edited Mary Sheeran, Tom Melham, Mary Sheeran, Tom Melham
This volume contains material provided by the speakers to accompany their presentations at
Wired: Wire-aware circuit design (2005)
Emil Axelsson, Koen Claessen, Mary Sheeran
Abstract. Routing wires are dominant performance stoppers in deep sub-micron technologies, and there is an urgent need to take them into account already at higher levels of abstraction. However, the...
Symbolic model checking based on induction (2004)
Niklas Sörensson, Niklas Sörensson, Niklas Eén, Niklas Sörensson, Koen Claessen, Niklas Sörensson, ...
Applications and extensions of algorithms for SAT solving. First order theorem proving and finite model finding. SAT based Model Checking. Software Development Paradox A finite model finder for first...
A Satellite Event of the ETAPS 2004 group of conferences Participants ’ Proceedings (2004)
Edited Tom Melham, Mary Sheeran, Tom Melham, Mary Sheeran, Scott Hazelhurst (witwatersrand, Axel Jantsch (kth, ...
This volume contains material provided by the speakers to accompany their presentations at
Generating fast multipliers using clever circuits (2004)
Abstract. New insights into the general structure of partial product reduction trees are combined with the notion of clever circuits to give a novel method of writing simple but flexible and highly...
Finding Regularity: Describing and Analysing Circuits That Are Not Quite Regular (2003)
We demonstrate some simple but powerful methods that ease the problem of describing and generating circuits that exhibit a degree of regularity, but are not as beautifully regular as the text-book...
A Tutorial on Lava: A Hardware Description and Verification System (2000)
Contents 1 Introduction 4 2 Getting Started 6 2.1 Your First Circuit . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2 The Lava Interpreter . . . . . . . . . . . . . . . . . . . . . . . . . 7...
The Final Proceedings for European Joint Conferences on Theory and Practice of Software (ETAPS), 6 April 2002 - 14 April 2002 This is a computer and information science conference. Topics include...
A tutorial on Stalmarck's proof procedure for propositional logic (1998)
Mary Sheeran, Gunnar Stalmarck
logic
A tutorial on the use of propositional logic and Stålmarck's method in system verification (1998)
. We explain the use of propositional logic, and in particular of Stalmarck's method of propositional proof, in modelling and verifying finite-state reactive systems. Part I: Propositional logic...
A tutorial on Stålmarck's proof procedure for propositional logic (1998)
Mary Sheeran, Mary Sheeran, Gunnar Stålmarck, Gunnar Stalmarck
. We explain Stalmarck's proof procedure for classical propositional logic. The method is implemented in a commercial tool that has been used successfully in real industrial verification...
Lava: Hardware Design in Haskell (1998)
Per Bjesse, Koen Claessen, Mary Sheeran, Satnam Singh
Lava is a tool to assist circuit designers in specifying, designing, verifying and implementing hardware. It is a collection of Haskell modules. The system design exploits functional programming...
How to prove properties of recursively defined circuits using Stalmarck's method (1998)
Mary Sheeran, Arne Borälv, Chalmers Tekniska Hogskola
. We present a technique for proving properties of recursively defined circuits using Stalmarck's method. We consider instances of circuits defined according to a particular inductive scheme and...
Per Bjesse 730921-6252 CTH Supervisor: (1997)
Mary Sheeran, Chalmers Tekniska
Specification of signal processing programs in a pure functional language and compilation to distributed architectures
New HDL research challenges posed by dynamically reprogrammable hardware (1996)
Jonathan Hogg, Satnam Singh, Mary Sheeran
Dynamically re�programmable hardware �e.g. Field Programmable Gate Arrays or FPGAs � change many of our basic assumptions of what hardware is. Nor� mal hardware design focuses on the...
We showhow to describe and analyse multistage interconnection networks in a relational framework. We give simple elegant descriptions of butterfly networks, using only two functions for building...
We show how to describe and analyse multistage interconnection networks in a relational framework. We give simple elegant descriptions of butterfly networks, using only two functions for building...
A Certain Loss of Identity (1992)
Geraint Jones, Mary Sheeran, Chalmers Tekniska Hogskola
For pragmatic reasons it is useful to exclude the identity relation from the `implementable subset' of Ruby. However there are many expressions in the relational calculus whose natural meaning...
Designing Arithmetic Circuits by Refinement in Ruby (1992)
. This paper presents in some detail the systematic derivation of a static bit-level parallel algorithm to implement multiplication of integers, that is to say one which might be implemented as an...
Geraint Jones, Geraint Jones, Mary Sheeran, Mary Sheeran, Mary Sheeran
Collecting butterflies This monograph contains three papers about butterfly circuits. Circuits of this form turn up in many signal processing applications, and networks of the same shape are found in...
Deriving bit-serial circuits in Ruby (1991)
The action of bit-serial arithmetic circuits is often explained in purely pictorial terms. In contrast, this paper describes an attempt to deal with the systematic development of bit-serial...
Relations and Refinement in Circuit Design (1991)
A language of relations and combining forms is presented in which to describe both the behaviour of circuits and the specifications which they must meet. We illustrate a design method that starts by...
Computer-Based Tools For Regular Array Design (1989)
Wayne Luk, Geraint Jones, Mary Sheeran
. We present an overview of a prototype system based on a functional language for developing regular array circuits. The features of a simulator, floorplanner and expression transformer are discussed...
Timeless Truths about Sequential Circuits (1988)
We suggest the use of a declarative programming language to design and describe circuits, concentrating on the use of higher-order functions to structure and simplify designs. In order to describe...
Designing FPGA Circuits in Lava
This paper explores the potential of the lazy functional programming language Haskell for the specification, synthesis and