The Community for Technology Leaders
Formal Methods and Models for Co-Design, ACM/IEEE International Conference on (2006)
Napa, CA, USA
July 27, 2006 to July 30, 2006
ISBN: 1-4244-0421-5
TABLE OF CONTENTS
Papers

Copyright (Abstract)

pp. ii

Table of Contents (Abstract)

pp. v-viii

Keynote Talk I (Abstract)

pp. 1-2

Component-based hardware/software co-verification (Abstract)

null Xiaoyu Song , Dept. of Comput. Sci., Portland State Univ., OR, USA
null Guowu Yang , Dept. of Comput. Sci., Portland State Univ., OR, USA
null Fei Xie , Dept. of Comput. Sci., Portland State Univ., OR, USA
pp. 27-36

A rule-based model of computation for SystemC: integrating SystemC and Bluespec for co-design (Abstract)

H.D. Patel , Bradley Dept. of Electr.&Comput. Eng., Virginia Tech., Blacksburg, VA, USA
S.K. Shukla , Bradley Dept. of Electr.&Comput. Eng., Virginia Tech., Blacksburg, VA, USA
pp. 39-48

Low-power hardware synthesis from TRS-based specifications (Abstract)

G. Singh , FERMAT Lab, Virginia Tech, Blacksburg, VA, USA
S.K. Shukla , FERMAT Lab, Virginia Tech, Blacksburg, VA, USA
pp. 49-58

802.11a transmitter: a case study in microarchitectural exploration (Abstract)

M. Pellauer , Comput. Sci.&Artificial Intelligence Lab, Massachusetts Inst. of Technol., Cambridge, MA, USA
N. Dave , Comput. Sci.&Artificial Intelligence Lab, Massachusetts Inst. of Technol., Cambridge, MA, USA
S. Gerding , Comput. Sci.&Artificial Intelligence Lab, Massachusetts Inst. of Technol., Cambridge, MA, USA
null Arvind , Comput. Sci.&Artificial Intelligence Lab, Massachusetts Inst. of Technol., Cambridge, MA, USA
pp. 59-68

Automatic decomposition for sequential equivalence checking of system level and RTL descriptions (Abstract)

J.A. Abraham , Comput. Eng. Res. Center, Texas Univ., Austin, TX, USA
S. Vasudevan , Comput. Eng. Res. Center, Texas Univ., Austin, TX, USA
pp. 71-80

A verified development of hardware using CSP/spl par/B (Abstract)

A.A. McEwan , Dept. of Comput., Surrey Univ., Guildford, UK
S. Schneider , Dept. of Comput., Surrey Univ., Guildford, UK
pp. 81-82

Keynote Talk II (Abstract)

pp. 87-88

Scalable program analysis using Boolean satisfiability (Abstract)

A. Aiken , Stanford Univ., CA, USA
pp. 89-90

Execution semantics and formalisms for multi-abstraction TLM assertions (Abstract)

W. Ecker , Infineon Technol. AG, Neubiberg, Germany
pp. 93-102

A methodology for abstracting RTL designs into TL descriptions (Abstract)

N. Bombieri , Dipt. di Informatica, Univ. di Verona, Italy
G. Pravadelli , Dipt. di Informatica, Univ. di Verona, Italy
F. Fummi , Dipt. di Informatica, Univ. di Verona, Italy
pp. 103-112

Using Reo for formal specification and verification of system designs (Abstract)

M. Sirjani , Dept. of Electr.&Comput. Eng., Tehran Univ., Iran
N. Razavi , Dept. of Electr.&Comput. Eng., Tehran Univ., Iran
pp. 113-122

Programming models and languages for SoC-implemented architectures (Abstract)

R. Gupta , California Univ., San Diego, CA, USA
pp. 125-126

Session V: Time and Clocks (Abstract)

pp. 127-128

Specifying and proving properties of timed I/O automata in the TIOA toolkit (Abstract)

M. Archer , Center for High Assurance Comput. Syst., Naval Res. Lab., Washington, DC, USA
pp. 129-138

Reliable design with multiple clock domains (Abstract)

J. Stoy , Bluespec Inc., Waltham, MA, USA
E. Czeck , Bluespec Inc., Waltham, MA, USA
R. Nanavati , Bluespec Inc., Waltham, MA, USA
pp. 139-148

The SystemJ approach to system-level design (Abstract)

F. Gruian , Dept. of Comput. Sci., Lund Inst. of Technol., Sweden
pp. 149-158

Keynote Talk III (Abstract)

pp. 159-160

Integrating design and verification - from simple idea to practical system (Abstract)

C. Seger , Strategic CAD Labs, Intel Corp., Santa Clara, CA, USA
pp. 161-162

Efficient code generation from synchronous programs (Abstract)

E. Vecchie , Dept. of Comput. Sci., Kaiserslautern Univ., Germany
J. Brandt , Dept. of Comput. Sci., Kaiserslautern Univ., Germany
K. Schneider , Dept. of Comput. Sci., Kaiserslautern Univ., Germany
pp. 165-174

Latency-insensitive design and central repetitive scheduling (Abstract)

R. de Simone , INRIA, Sophia-Antipolis, France
J. Boucaron , INRIA, Sophia-Antipolis, France
J.-V. Millo , INRIA, Sophia-Antipolis, France
pp. 175-183

A scenario-aware data flow model for combined long-run average and worst-case performance analysis (Abstract)

S. Stuijk , Dept. of Electr. Eng., Eindhoven Univ. of Technol., Netherlands
S.V. Gheorghita , Dept. of Electr. Eng., Eindhoven Univ. of Technol., Netherlands
M.C.W. Geilen , Dept. of Electr. Eng., Eindhoven Univ. of Technol., Netherlands
J.P.M. Voeten , Dept. of Electr. Eng., Eindhoven Univ. of Technol., Netherlands
T. Basten , Dept. of Electr. Eng., Eindhoven Univ. of Technol., Netherlands
B.D. Theelen , Dept. of Electr. Eng., Eindhoven Univ. of Technol., Netherlands
pp. 185-194

Formal methods for checking realizability of coalitions in 3-party systems (Abstract)

P. Dasgupta , Dept. of Comput. Sci.&Eng., Indian Inst. of Technol., Kharagpur, India
P.P. Chakrabarti , Dept. of Comput. Sci.&Eng., Indian Inst. of Technol., Kharagpur, India
A. Banerjee , Dept. of Comput. Sci.&Eng., Indian Inst. of Technol., Kharagpur, India
pp. 198

A semantic-driven synthesis flow for platform-based design (Abstract)

null Qi Zhu , Dept. of Electr. Eng.&Comput. Sci.,, California Univ., Berkeley, CA, USA
A. Davare , Dept. of Electr. Eng.&Comput. Sci.,, California Univ., Berkeley, CA, USA
A. Sangiovanni-Vincentelli , Dept. of Electr. Eng.&Comput. Sci.,, California Univ., Berkeley, CA, USA
pp. 199

Assertion checking of control dominated systems with nonlinear solvers (Abstract)

P. Sanchez , Dep. TEISA, Cantabria Univ., Spain
I. Ugarte , Dep. TEISA, Cantabria Univ., Spain
pp. 200

Compositional interaction specifications for SystemC (Abstract)

I.H. Krueger , California Univ., San Diego, CA, USA
F. Doucet , California Univ., San Diego, CA, USA
R. Gupta , California Univ., San Diego, CA, USA
pp. 201

R-SHIM: deterministic concurrency with recursion and shared variables (Abstract)

S.A. Edwards , Dept. of Comput. Sci., Columbia Univ., New York, NY, USA
O. Tardieu , Dept. of Comput. Sci., Columbia Univ., New York, NY, USA
pp. 202

Author Index (Abstract)

pp. 203-204
97 ms
(Ver )