BEGIN:VCALENDAR PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN CALSCALE:GREGORIAN X-WR-CALNAME:Calagator METHOD:PUBLISH VERSION:2.0 BEGIN:VTIMEZONE TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles BEGIN:STANDARD DTSTART:20111106T020000 RDATE:20111106T020000 TZOFFSETFROM:-0700 TZOFFSETTO:-0800 TZNAME:PST END:STANDARD END:VTIMEZONE BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20120106T012427Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120112T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120112T103000 DTSTAMP;VALUE=DATE-TIME:20120106T012427Z LAST-MODIFIED;VALUE=DATE-TIME:20120106T012427Z UID:http://calagator.org/events/1250461808 DESCRIPTION:Presented by Julien Schmaltz. \;\n \;\nCommunication fa brics constitute an important challenge for the design and verification of multicore architectures. To enable their formal analysis\, micro-arch itectural models have been proposed as an efficient abstraction capturin g the high-level structure of designs. Micro-architectural models also i nclude a representation of the protocols using the communication fabrics . This combination of different aspects in a single model is crucial for deadlock verification. Deadlocks emerge or are prevented in this combin ation: a system with a deadlock-free communication network combined with a deadlock-free protocol may have deadlocks or a system with a network with deadlocks combined with a deadlock-free protocol may be deadlock-fr ee. This combination also makes the verification problem more complicate d. We will present an algorithm for efficient deadlock verification in m icro-architectural models. We will discuss the limitations of this appro ach and point to future research direction. An important future applicat ion of our methodology is the verification of cache coherency at the lev el of micro-architectures.\n\nTags: galois\, formal methods\, hardware\, tech talk\, verification\n\nImported from: http://calagator.org/events/ 1250461808 URL:https://corp.galois.com/blog/2012/1/5/galois-tech-talk-33-next-week-o n-deadlock-verification-in-mi.html SUMMARY:Galois Tech Talk (3/3 next week!): On deadlock verification in mi cro-architectural models of communication fabrics. LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT END:VCALENDAR