December 13-15, 2010
Hyatt Regency Hotel, Austin, Texas, USA

December 12, 2010

6-8pm: MTV Welcome Drink and Early Registration.

Location Hyatt Marker 10 Bar
Meet the MTV organizers to pick-up your registration material early while enjoying a complimentary drink.

Day 1: December 13, 2010

7:30-7:50am: Registration and continental breakfast

7:50-8:00am: Welcome and Opening Remarks by the Workshop General Chair: Magdy Abadir (Freescale, USA)

8:00-9:40am: Debug Session

A.1 On the Resolution of Sequential Debugging

Görschwin Fey, André Sülflow, and Rolf Drechsler (University of Bremen, Germany)

A.2 An Automated Framework for Correction and Debug of PSL Assertions

Brian Keng*, Sean Safarpour (Vennsa Technologies, Canada), Andreas Veneris*, (*University of Toronto, Canada)

A.3 Post-silicon debugging with high level design descriptions and programmable controllers

Masahiro Fujita, Bijan Alizadeh, Hiroaki Yoshida, Takeshi Matsumoto (University of Tokyo, Japan)

A.4 Automation Techniques for Post-Silicon Debug of Timing Errors

Azadeh Davoodi (University of Wisconsin at Madison, USA)

9:40-10:30am: Architecture Validation

B.1 Using Software Architecture Patterns to Validate Performance of a Threaded Processor Architecture

Jim Holt and David Lindberg (Freescale, USA)

B.2 The impact a complete target environment simulation has on architecture validation: Case study of Speculative Execution Proposals

Jack Mason (Nova Southeastern University, USA)

10:30-10:45am Coffee Break

10:45-12:00pm: Validation Test

C.1 Fault Grading of Software-Based Self-Test procedures for Dependable Automotive Applications

Paolo Bernardi, Ernesto Sanchez, Michelangelo Grosso, *Oscar Ballan and *Giovanni Fontana (politecnico di torino, Italy and *STMicroelectronics, Italy)

C.2 Test Generation For Functional Verification of CMP Designs

Padmaraj Singh and *David Landis (Nvidia, *Carnegie Mellon University, USA)

C.3 A kernel based validation framework for functional test selection

Po-Hsien Chang and Li-C Wang (University of California at Santa Barbara, USA)

12:00-1:30pm Lunch break

1:30-3:15pm Panel I: Verification is a problem, but is debug the root cause?

Moderator: Sean Safarpour (Vennsa Technologies)
Harry Foster (Mentor Graphics)
Michael Stellfox (Cadence)
Alex Wakefield (Synopsys)
Bindesh Patel (Springsoft)

3:15-3:30pm Coffee Break

3:30-5:10 pm System Level

D.1 FPGA prototyping of the ARM Cortex A8 processor

Steve Ravet (ARM, USA)

D.2 Automatic Fault Localization for SystemC TLM Designs

Hoang M. Le, Daniel Grosse and Rolf Drechsler (University of Bremen, Germany)

D.3 Redesign and Verification of RTL IPs through RTL-to-TLM Abstraction and TLM Synthesis

Nicola Bombieri, Franco Fummi, Valerio Guarnieri, Graziano Pravadelli and Sara Vinco (University of Verona, Italy)

D.4 A Hardware/Software Co-design Framework using Abstract State Machines

Nathan D. P. Buchanan and Hiren D. Patel (University of Waterloo, Canada)

6:30pm MTV Workshop Dinner

Venue: Fogo De Chao, 309 E. 3rd St., Austin, TX 78701, Phone: (512) 472-0220

Description: A short (about 10 minutes) walk from Hyatt Fogo De Chao is located in downtown Austin. It features Brazilian cuisine with over 30 items including fresh cut vegetables, imported cheeses, cured meats and Brazilian side dishes. A wide variety of meat specialties expertly prepared by gaucho chefs and all you can eat gourmet salad and sides bar provides for a great experience amid stimulating discussions.

Transportation: Attendees can stroll to the restaurant or arrange for alternate ground transportation to the restaurant.

Day 2: December 14, 2010

7:30-8:00am Registration and continental breakfast

8:00-9:15am: Formal Verification

E.1 Schedulability Analysis for Multi-Core Global Scheduling under Cache Warm-Up Overheads based on Model Checking

Wei Sheng, Yanyan Gao, Li Xi and Xuehai Zhou (University of Science and Technology, China)

E.2 An Embedded Reachability Analyzer And Invariant Checker (ERAIC)

Ouiza Dahmoune and Robert de B. Johnston (INRS-EMT, Canada)

E.3 Bounded Model Checking of Incomplete Networks of Timed Automata

Christian Miller, Karina Gitina, Christoph Scholl and Bernd Becker (Albert-Ludwigs-Universitaet Freiburg, Germany)

9:15-10:05am: Coverage

F.1 Relational Database Schema for the UltraSparc Functional Coverage Flow

James Roberts, Ray Voith and Michael Burns (Oracle, USA)

F.2 Hi-Fi or One Small Music Library? Exploring the Implementation and Analysis Cost Trade-Offs of Coverage Model Design

Paul Graykowski and Andrew Piziali (Synopsys, USA)

10:05-10:20am Coffee Break

10:20-12:00pm: SoC VerificationG.1 An Efficient Event Generation Method for Testing a SOC with Multiple Processing Elements and Associated Peripherals

Devraj Kallappa Bakchowde and Nanda Kishore A S (Nokia Siemens Networks India Pvt. Ltd, India)

G.2 An enhanced Strategy for Functional Stress Pattern Generation for System-on-Chip Reliability Characterization

Mauricio de carvalho, Paolo Bernardi, Ernesto Sanchez and Matteo Sonza Reorda (Politecnico di Torino, Italy)

G.3 System validation using IP-XACT standards

Rajesh Chirumamilla (ARM, India)

G.4 Using Graphics Processing Units for Logic Simulation of Electronic Desings

Alper Sen, Baris Aksanli, Murat Bozkurt (Bogazici University,Turkey)

12:00-1:30pm Lunch break

1:30-3:15pm Panel II: SystemVerilog Verification Methodology: Challenges and Solutions

Moderator: Bhanu Kapoor (Mimasic)
Sharon Rosenberg (Cadence)
Janick Bergeron (Synopsys)
Alan Hunter (ARM)

3:15-3:30pm Coffee Break

3:30-4:45pm Invited Industry Session on Formal Methods for Power & Performance

H.1 Pranav Ashar, CTO, RealIntent

H.2Yuan Lu, CTO, NextOp Software

H.3 Rajeev Ranjan, CTO, Jasper Design Automation

4:45pm Closing Remarks – Magdy Abadir (Freescale)

Day 3: December 15, 2010

Tutorials Day

(Free with MTV registration)

Venue: Freescale Semiconductor Inc

7700 W Parmer Lane, Building A Auditorium, Austin, TX 78729

8:00-11am: Tutorial : Experiences in Validating Power-Managed Processors and Wireless SoCs

Bhanu Kapoor (Mimasic), Alan Hunter (ARM), Amit Kumar (CSR), and Prapanna Tiwari (Synopsys)

In this tutorial, we focus on the power management architecture verification experiences of Wireless SoCs and specifically focus on the tasks for validating a power managed ARM Cortex A-8 core and a power-managed GPS SoC.

The power management verification strategy was put in place with following goals in mind:

  • Ensuring the intent of power-aware design is implemented per its architecture definition
  • Correct sequencing of control signals during the switching and scaling of power supplies
  • Correct input and output functionality of each power domain during the power cycles
    • Coverage of all power states and all legal transitions between these power states
    • Some of the specific verification issues encountered and to be discussed here include the following:
  • Ensuring that each of the domains are clamped correctly in all valid power states of the chip
  • Ensuring level-shifters and level shifting clamps are correctly placed and validated for presence of different voltages and clock frequencies associated with the power domains
  • Issues with voltages on level-shifters corrupting signals across domains
  • Delay dependent issue with isolation resulting from voltage ramp times
  • Un-initialized registers & memory contents on each power cycle corrupting downstream logic

We will review all of the key power management techniques and associated verification issues and then follow it up with the case studies of a processing core and a GPS chip.