Abstract: We present a hardware-software co-design and verification framework targeting computer elements including System-on-Chips (SoC) as well as printed circuit boards (PCB) designs by trying to completely separate their computation and communication parts. The basic idea is to formally verify and synthesize communication parts independently from computation parts so that any changes of protocols in interfaces/communications do not affect the correctness of the computation parts. We define interface protocols in terms of automaton which are formally verified through model checking type tools.  Then the actual hardware and software elements for the target computer systems can be automatically generated from them. Software can be automatically compiled into the target processors codes. As for hardware, high level synthesis followed by logic synthesis is applied to generate gate-level implementations. During scheduling phases of software and hardware synthesis processes, input-output (I/O) timings for the target design are fixed. When communication protocol changes, the timings of such I/O must be rescheduled so as to satisfy the new protocol definition. We define common interface mechanisms between computation and communication parts which make their independent development possible. Using that common interface, computation parts are seamlessly unified with their automatically generated communication parts.  As an example application of our design methodology, we discuss about automatic generation of VLSI on-chip bus protocol converters. In IP based designs of VLSI, designers try to reuse existing IPs as much as possible. Since currently available IPs use various communication protocols, protocol conversion is one of the most important topics in IP-based designs.

We propose a method for automatic protocol transducer synthesis which is applicable to the state-of-the-art complicated protocols. The key idea here is again to separate the data transfer circuits from protocol definitions as much as possible, which makes it possible to develop protocol transducer synthesis techniques based on a divide and conquer approach. We demonstrate our method by synthesizing transducers which translate among the real and complicated protocols with advanced features such as non-blocking transactions and out-of-order transactions.

Masahiro Fujita received his Ph.D. from the University of Tokyo in 1985. He is a professor in VLSI Design and Education Center (VDEC) at the University of Tokyo. Prior to joining the University of Tokyo in 2000, he was director of CAD for VLSI in Fujitsu Laboratories of America for 6 years. He has done innovative works in the areas of digital design verification, synthesis, and testing. He has co-authored 7 books, and has over 100 publications. He has been given several research awards from Japanese scientific societies. His current research interests include synthesis and verification in higher level design stages, hardware/software co-designs and also digital/analog co-designs. Appointments: dcm@cs.cmu.edu