The Community for Technology Leaders
Sixth ACM and IEEE International Conference on Formal Methods and Models for Co-design, MEMOCODE '08 (2008)
Anaheim, CA
June 5, 2008 to June 7, 2008
ISBN: 978-1-4244-2417-7
TABLE OF CONTENTS

[Commentary] (PDF)

pp. v

Table of contents (PDF)

pp. iii-iv

Programming Multicores with Kahn Process Networks; a Smart Choice? (PDF)

Bart Kienhuis , Leiden Institute of Advanced Computer Science (LIACS)
pp. 3-4

Arithmetic Circuits Verification without Looking for Internal Equivalences (PDF)

O. Sarbishei , Department of Electrical Engineering, Sharif University of Technology, Tehran, Iran, sarbishei@ee.sharif.edu
B. Alizadeh , Department of Electrical Engineering, Sharif University of Technology, Tehran, Iran, b_alizadeh@sharif.edu
Masahiro Fujita , VLSI Design and Education Center (VDEC), University of Tokyo, Tokyo, Japan, fujita@ee.t.u-tokyo.ac.jp
pp. 7-16

From Data to Events: Checking Properties on the Control of a System (PDF)

Christophe Jacquet , SUPELEC, 3 rue Joliot-Curie, 91192 Gif-sur-Yvette Cedex, FRANCE, Christophe.Jacquet@supelec.fr
Frederic Boulanger , SUPELEC, 3 rue Joliot-Curie, 91192 Gif-sur-Yvette Cedex, FRANCE, Frederic.Boulanger@supelec.fr
Dominique Marcadet , SUPELEC, 3 rue Joliot-Curie, 91192 Gif-sur-Yvette Cedex, FRANCE, Dominique.Marcadet@supelec.fr
pp. 17-26

Vacuity Analysis by Fault Simulation (PDF)

Luigi di Guglielmo , Dipartimento di Informatica ¿ Università di Verona, Strada le Grazie 15, 37134 Verona, Italy, luigi.diguglielmo@univr.it
Franco Fummi , Dipartimento di Informatica ¿ Università di Verona, Strada le Grazie 15, 37134 Verona, Italy, franco.fummi@univr.it
Graziano Pravadelli , Dipartimento di Informatica ¿ Università di Verona, Strada le Grazie 15, 37134 Verona, Italy, graziano.pravadelli@univr.it
pp. 27-36

Rule-Based Approaches for Equivalence Checking of SpecC Programs (PDF)

Subash Shankar , City University of New York (CUNY), New York City, NY, subash.shankar@hunter.cuny.edu
Masahiro Fujita , University of Tokyo, Tokyo, Japan, fujita@ee.t.u-tokyo.ac.jp
pp. 39-48

Static Deadlock Detection for the SHIM Concurrent Language (PDF)

Nalini Vasudevan , Department of Computer Science, Columbia University, New York, USA, naliniv@cs.columbia.edu
Stephen A. Edwards , Department of Computer Science, Columbia University, New York, USA, sedwards@cs.columbia.edu
pp. 49-58

A Comparison of Two SystemC/TLM Semantics for Formal Verification (PDF)

Claude Helmstetter , INRIA - LIAMA, Beijing 100080, China, claude@liama.ia.ac.cn
Olivier Ponsini , INRIA, 38334 Saint-Ismier Cedex, France, olivier.ponsini@inria.fr
pp. 59-68

Latency-Insensitive Hardware/Software Interfaces (PDF)

Greg Hoover , University of California, Santa Barbara and Washington University, ghoover@ece.ucsb.edu
Forrest Brewer , University of California, Santa Barbara and Washington University, forrest@ece.ucsb.edu
Chris Gill , University of California, Santa Barbara and Washington University, cdgill@cse.wustl.edu
pp. 71-72

Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems (PDF)

Radu Mateescu , INRIA / VASY project-team, Faculté des Sciences Mirande, bât. LE2I, F-21000 Dijon, France, Radu.Mateescu@inria.fr
Emilie Oudot , INRIA / VASY project-team, Faculté des Sciences Mirande, bât. LE2I, F-21000 Dijon, France, Emilie.Oudot@inria.fr
pp. 73-74

Assertion-Based Design with Horus (PDF)

Yann Oddos , Laboratoire TIMA,INPG/UJF/CNRS, 46 avenue F.Viallet, 38031 Grenoble cedex, France., E-mail: yann.oddos@imag.fr
Katell Morin-Allory , Laboratoire TIMA,INPG/UJF/CNRS, 46 avenue F.Viallet, 38031 Grenoble cedex, France., E-mail: katell.morin-allory@imag.fr
Dominique Borrione , Laboratoire TIMA,INPG/UJF/CNRS, 46 avenue F.Viallet, 38031 Grenoble cedex, France., E-mail: dominique.borrione@imag.fr
pp. 75-76

A System Verilog Rewriting System for RTL Abstraction with Pentium Case Study (PDF)

Steve Haynal , Strategic CAD Labs, Intel Corporation, 2501 NW 229th, Ave, Hillsboro, OR 97124, steve.haynal@intel.com
Timothy Kam , Strategic CAD Labs, Intel Corporation, 2501 NW 229th, Ave, Hillsboro, OR 97124, timothy.kam@intel.com
Michael Kishinevsky , Strategic CAD Labs, Intel Corporation, 2501 NW 229th, Ave, Hillsboro, OR 97124, michael.kishinevsky@intel.com
Emily Shriver , Strategic CAD Labs, Intel Corporation, 2501 NW 229th, Ave, Hillsboro, OR 97124, emily.shriver@intel.com
Xinning Wang , Strategic CAD Labs, Intel Corporation, 2501 NW 229th, Ave, Hillsboro, OR 97124, xinning.wang@intel.com
pp. 79-88

Directed-Logical Testing for Functional Verification of Microprocessors (PDF)

Michael Katelman , Department of Computer Science, University of Illinois at Urbana-Champaign, U.S.A., katelman@uiuc.edu
Jose Meseguer , Department of Computer Science, University of Illinois at Urbana-Champaign, U.S.A., meseguer@uiuc.edu
Santiago Escobar , Departmento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Spain, sescobar@dsic.upv.es
pp. 89-100

Estimating the Performance of Cache Replacement Policies (PDF)

Daniel Grund , Saarland University, grund@cs.uni-sb.de
Jan Reineke , Saarland University, reineke@cs.uni-sb.de
pp. 101-112

Infinite State Model Checking with Arithmetic Constraints (PDF)

Tevfik Bultan , University of California, Santa Barbara
pp. 115-116

Classification of General Data Flow Actors into Known Models of Computation (PDF)

Christian Zebelein , Hardware/Software Co-Design, University Erlangen-Nuremberg, Erlangen, Germany, E-mail: christian.zebelein@cs.fau.de
Joachim Falk , Hardware/Software Co-Design, University Erlangen-Nuremberg, Erlangen, Germany, E-mail: falk@cs.fau.de
Christian Haubelt , Hardware/Software Co-Design, University Erlangen-Nuremberg, Erlangen, Germany, E-mail: haubelt@cs.fau.de
Jurgen Teich , Hardware/Software Co-Design, University Erlangen-Nuremberg, Erlangen, Germany, E-mail: teich@cs.fau.de
pp. 119-128

On the Deterministic Multi-threaded Software Synthesis from Polychronous Specifications (PDF)

Bijoy A. Jose , FERMAT Lab, Virginia Polytechnic Institute and State University, Blacksburg, VA, USA, bijoy@vt.edu
Sandeep K. Shukla , FERMAT Lab, Virginia Polytechnic Institute and State University, Blacksburg, VA, USA, shukla@vt.edu
Hiren D. Patel , Ptolemy Group, University of California, Berkeley, Berkeley, CA, USA, hiren@eecs.berkeley.edu
Jean-Pierre Talpin , ESPRESSO Project, IRISA/INRIA, Rennes, France, jean-pierre.talpin@irisa.fr
pp. 129-138

Virtual prototyping AADL architectures in a polychronous model of computation (PDF)

Yue Ma , INRIA, Unité de Recherche Rennes-Bretagne-Atlantique, Campus de Beaulieu, 35042 Rennes Cedex, France
Jean-Pierre Talpin , INRIA, Unité de Recherche Rennes-Bretagne-Atlantique, Campus de Beaulieu, 35042 Rennes Cedex, France
Thierry Gautier , INRIA, Unité de Recherche Rennes-Bretagne-Atlantique, Campus de Beaulieu, 35042 Rennes Cedex, France
pp. 139-148

MEMOCODE 2008 Co-Design Contest (PDF)

Patrick Schaumont , ECE Dept Virginia Tech, schaum@vt.edu
Krste Asanovic , EECS Dept UC Berkeley, krste@eecs.berkeley.edu
James C. Hoe , ECE Dept Carnegie Mellon University, jhoe@ece.cmu.edu
pp. 151-154

High-throughput Pipelined Mergesort (PDF)

Kermin Fleming , MIT - CSAIL, Cambridge, MA, kfleming@csail.mit.edu
Myron King , MIT - CSAIL, Cambridge, MA, mdk@csail.mit.edu
Man Cheuk Ng , MIT - CSAIL, Cambridge, MA, mcn02@csail.mit.edu
Asif Khan , MIT - CSAIL, Cambridge, MA, aik@csail.mit.edu
Muralidaran Vijayaraghavan , MIT - CSAIL, Cambridge, MA, vmurali@csail.mit.edu
pp. 155-158

Hardware Accelerated Crypto Merge Sort: MEMOCODE 2008 Design Contest (PDF)

VJ Sananda , AMD, Austin North Design Center, 9500 Arboretum Blvd, Austin TX 787, E-mail: vj.sananda@amd.com
pp. 159-162

H.264 Decoder: A Case Study in Multiple Design Points (PDF)

Kermin Fleming , MIT - CSAIL, Cambridge, MA, kfleming@csail.mit.edu
Chun-Chieh Lin , MIT - CSAIL, Cambridge, MA, ragnarok@csail.mit.edu
Nirav Dave , MIT - CSAIL, Cambridge, MA, ndave@csail.mit.edu
Arvind , MIT - CSAIL, Cambridge, MA, arvind@csail.mit.edu
Gopal Raghavan , Nokia Research Center - Cambridge, Cambridge, MA, gopal.raghavan@nokia.com
Jamey Hicks , Nokia Research Center - Cambridge, Cambridge, MA, jamey.hicks@nokia.com
pp. 165-174

Correctness of a Fault-Tolerant Real-Time Scheduler and its Hardware Implementation (PDF)

Eyad Alkassar , Saarland University,, Dept. of Computer Science, 66123 Saarbrücken, Germany, eyad@wjpserver.cs.uni-sb.de
Peter Bohm , University of Oxford, Computing Laboratory, Oxford, OX1 3QD, England, petb@comlab.ox.ac.uk
Steffen Knapp , Saarland University, Dept. of Computer Science, 66123 Saarbrücken, Germany, sknapp@wjpserver.cs.uni-sb.de
pp. 175-186

Specification and Verification of LambdaRAM- A Wide-area Distributed Cache for High Performance Computing (PDF)

Venkatram Vishwanath , Dept. of Computer Science, University of Illinois at Chicago, venkat@evl.uic.edu
Lenore D. Zuck , Dept. of Computer Science, University of Illinois at Chicago, lenore@cs.uic.edu
Jason Leigh , Dept. of Computer Science, University of Illinois at Chicago, spiff@uic.edu
pp. 187-198

Author index (PDF)

pp. A-1
94 ms
(Ver 3.3 (11022016))