"In my research work, I have been applying formal techniques to RTL at the micro-architecture level," stated Prof. Melham. "I am pleased to be joining the Jasper TAB to advance the technology pipeline for applying formal technologies throughout the whole design and verification cycle, from architecture to silicon. I see Jasper taking the lead in formal technology applications at the architecture level, helping chip companies alleviate the most troubling downstream design and verification challenges."
Prof. Melham received his Ph.D. in 1990 from the University of Cambridge for his foundational research in formal hardware verification and mechanized reasoning, and was a co-developer of the original HOL theorem prover for higher order logic at Cambridge. In 1993, he joined the Computing Science Department at Glasgow University. He was appointed to a Professorship of Computing Science at Glasgow in 1998, before moving to Oxford in 2002. He was elected a Fellow of the Royal Society of Edinburgh in 2002.
"Having been involved with formal verification research and development for 25 years, I am excited about joining Jasper's TAB to participate in the ongoing development and growing proliferation of formal verification across a wide variety of horizontal industry segments,” stated Moshe Vardi. “With the rising importance of high-level models in design, formal verification is becoming critical to the industry. I expect Jasper to play a major role in this market."
Prior to joining Rice University, Prof. Vardi was at the IBM Almaden Research Center, where he managed the Mathematics and Related Computer Science Department. Vardi is the recipient of three IBM Outstanding Innovation Awards, and a co-winner of the 2000 Gödel Prize, the 2005 ACM Paris Kanellakis Award for Theory and Practice, and the LICS 2006 Test-of-Time Award. He holds honorary doctorates from the University of Saarland, Germany, and the University of Orleans, France, and received his Ph.D. from the Hebrew University of Jerusalem in 1981.
"We are delighted to welcome Moshe and Tom to our technical advisory board, and pleased to be working with two of the industry’s most respected formal verification visionaries," said Ziyad Hanna, chief architect and vice president of research at Jasper Design Automation. “These two gentlemen have contributed greatly to formal verification research and development, and will help Jasper advance its formal technology leadership."
About Jasper’s Technical Advisory Board
Jasper’s Technical Advisory Board (TAB) is made up of verification luminaries from the academic and commercial worlds. The TAB’s purpose is to advise Jasper’s management team on research trends in formal verification and formal technology exploration and expansion. The TAB also provides valued guidance on Jasper’s technical product development, and educates students and the market on trends in formal verification.
In addition to Tom Melham and Moshe Vardi, the TAB currently includes Brian Bailey, renowned verification industry veteran; Alan Hu, associate head of the Department of Computer Science at the University of British Columbia; Sharad Malik, professor in the Department of Electrical Engineering, Princeton University; and Satoshi Goto, professor at the Graduate School of Information, Production and Systems, Waseda University, Kitakyushu, Japan.
About Jasper Design Automation
Jasper Design Automation’s production-proven formal verification solutions are used by logic designers, verification engineers and silicon bring-up teams to design, explore and debug RTL, to ensure correctness of block-level functionality and for rapid post-silicon validation and debug. JasperGold® Verification System delivers complete “deep formal” systematic verification, ensuring correctness of critical design features without any testbench development. JasperGold Express, a “light formal” solution, complements simulation by accelerating bug-hunting and coverage attainment. For expert help with large scale formal verification deployment, RTL exploration or post-silicon debug, please visit http://www.jasper-da.com.
Jasper Design Automation, the Jasper Design Automation logo,
JasperGold, Formal Testplanner, GamePlan, Proof Accelerators, Lossless
Abstractions, Formal Scoreboard, and Design Tunneling are trademarks or
registered trademarks of Jasper Design Automation, Inc. All other names
mentioned are trademarks, registered trademarks, or service marks of
their respective companies.