Organisers:
Ian Harris, University of Californa Irvine, US
Mathias Soeken, Universität Bremen, DE

The life of a computing system arguably begins with architects developing architectural models, and tuning various design parameters for target performance and power consumption. The result of this process is the definition of the high-level architectural specification of the system, which defines the functional requirements for the system design. This specification is used as a guide for most downstream activities, e.g., decompose system functionality, implement various design blocks, perform code reviews, design pre-silicon and post-silicon validation test-benches, define assertions, etc. Unfortunately, architectural specifications are rarely developed with the rigor, discipline, and formality warranted for something used so extensively throughout the system life cycle. System functionality is typically described informally with prose mixed with charts, diagrams, and tables. Furthermore, these descriptions are spread across a large number of different documents, each document several hundreds of pages long and covering different aspects of the design (e.g., functionality, power, security, communication, etc.). Unsurprisingly, these documents contain inconsistencies, ambiguities, even errors. These are often discovered late in the implementation or validation phases or on field, leading to late design churns, complex patches, point-fixes, and de-featuring. The situation is exacerbated in recent years with fast increasing design complexity on the one hand and decreasing time-to-market on the other.

In this talk, we look at the industrial practice in defining design specification, the complexities in making them rigorous, and the impacts of specification ambiguity to design, validation, and production. Specific examples from industrial case studies will be used for demonstration. We look at recent efforts from different affected stake-holders (i.e., architects, designers, implementers, and validators) to converge on requirement descriptions. In spite of these efforts, a significant gap remains between the state of the practice and what is needed to define unambiguous specifications for trustworthy system designs, and we explore the critical research needs in this area.

Bio: Sandip Ray a Research Scientist at Intel's Strategic CAD Labs in Hillsboro, OR, USA. His research focuses on developing correct, dependable, and trustworthy computing systems through a synergy of specification, synthesis, verification, and validation techniques. At Intel, he leads research on development of a trustworthy and robust validation infrastructure for next-generation industrial SoC designs. Before joining Intel, Dr. Ray worked as a Research worked as a Research Scientist at the University of Texas at Austin, where he developed analysis frameworks for diverse computing systems ranging from synthesized hardware designs to software routines including binary and assembly programs. His work found application in major semiconductor companies, including AMD, Freescale, IBM, Intel, Galois, and Rockwell Collins. Dr. Ray is the author of three books (two upcoming), as well as more than 40 peer-reviewed research papers published in international journals and conferences. He has served on the technical program committee of more than 30 international meetings and conferences, and as general and program chair for ACL2 2009 and FMCAD 2013. He serves as an Associate Editor for IEEE Transactions on Multi-scale Computing Systems, and has served as guest Associate Editor for ACM TODAES and Springer JETTA. Dr. Ray has a Ph.D. from the University of Texas at Austin, and is a senior member of IEEE.

Algebraic Geometry is the study of the (geometry of) solutions to a system of polynomial equations. Modern algebraic geometry does not explicitly solve the system of equations to enumerate the solutions, but rather reasons about the solutions using abstract/computational algebra. Particularly, the theory and technology of Groebner bases provide a powerful set of tools to solve these polynomial decision problems. In this talk, I will describe how techniques from algebraic geometry and symbolic computation can be used to derive canonical (word-level) abstractions of the functions implemented by hardware designs.

Hardware designs and their functions often exhibit some structure or symmetry in the implementations. To improve our understanding of hardware designs, the functionality, symmetry and the structure of the circuits needs to be analyzed together. Can algebraic geometry help us achieve that? I will present Groebner bases techniques and applications that show glimpses of such a capability --- hopefully, this will motivate the DUHDe community to investigate the use of algebraic geometry to better understand hardware designs.

Bio: Priyank Kalla received the B.E. degree in electronics engineering from Birla Vishvakarma Mahavidyalaya, Sardar Patel University, Vallabh Vidyanagar, India, in 1993, and the M.S. and Ph.D. degrees from the University of Massachusetts, Amherst, in 1998 and 2002.

Since 2002, he has been first an Assistant Professor and now an Associate Professor with the Electrical and Computer Engineering Department at the University of Utah in Salt Lake City.

Dr. Kalla's research interests are in fundamental CAD techniques for the synthesis, optimization, and verification of digital VLSI circuits and systems.

Dr. Kalla was a recipient of the NSF CAREER award in 2006.