At this first Decoding Formal Club meeting of 2015, we will tread deep into formal, cover constraint management for formal sign-off, debate liveness vs. safety, and discuss the evolution of formal verification at ARM. Speakers include Jonathan Michelson from NVIDA, Ross Weber from ARM, Oski CEO, Vigyan Singhal and special guest and TED-Talk presenter, Cliff Stoll, who will talk about his blown glass Klein bottles.
Jonathan Michelson from NVIDA will cover the long-standing debate over liveness vs. safety and describe two real post-silicon design bugs undetected by simulation. Ross Weber will take us on a dive into the formal verification activities on a new CPU project. Topics to include planning, property development, designer usage, initial value abstractions, deep bug hunting, and formal verification coverage metrics/tools. Vigyan Singhal from Oski Technology will talk about constraint management, over-constraints, under-constraints, dead-ends and vacuous proofs as they relate to formal sign-off.
Cliff Stoll, scientist, educator, TED Talk presenter, will be joining us as a special guest speaker. For 15 years, Acme Klein Bottle has provided nonorientable manifolds to math folk. Like much of mathematics, it’s marginally profitable, but endlessly entertaining. Thousands of online computer models of Klein bottles grace the internet, but physical models are rarely built. Using a torch and hot glass, we supply the finite but unbounded demand or one-sided, R3 immersed, zero-volume, borosilicate Riemannian manifolds. So how do you make a Klein Bottle? Attend our last session of the day with TED Talk presenter Cliff Stoll, and find out!
11:30 AM Welcome, Lunch and Networking
12:30 PM Constraint Management for Formal Sign-off
Vigyan Singhal, CEO, Oski Technology
1:30 PM Coffee Break
1:40 PM Liveness vs. Safety – A Practical Viewpoint
Jonathan Michelson, Principal Engineer, NVIDIA
2:25 PM “What if “Table Topics and Networking
2:45 PM Formal Verification and a New CPU Project at ARM
Ross Weber, Formal Verification Engineer, ARM
3:30 PM Low Dimensional Topology for Fun and Profit
Cliff Stoll, TED-Talk presenter, Newfield Wireless and Acme Klein Bottles
4:00 PM Wrap-Up and Prize Drawing
4:15 PM Computer History Museum Tour (Self-Guided)
* * * Registration is now closed for this event. * * *
Jonathan Michelson has more than 18 years of experience verifying complex designs via both formal verification and coverage driven, directed random simulation. He is a co-author of “The Art of Verification with SystemVerilog Assertions,” “The Art of Verification with Vera”, and many publicly published papers and presentations. He co-designed a verification language and methodology at Silicon Graphics; architected, designed, and verified complex systems at Cisco; and is currently verifying low power, high performance processors at nVidia. He received his bachelor’s and master’s degrees in electrical engineering and computer science from the Massachusetts Institute of Technology.i.
Ross Weber is a formal verification engineer in the ARM Austin CPU design team. Ross worked at Jasper, and before that for 10 years at Unisys as a designer in the system cache design team, for about five of those years using Incisive Formal Verifier (IFV).
Cliff Stoll graduated from Buffalo Public School #61 with a blue star for good attendance. Later, he did postdocs at Kitt Peak Observatory, 紫金山天文台, Space Telescope Institute, Lawrence Berkeley Labs, and Harvard-Smithsonian Center for Astrophysics. In his spare time, he squeezes lumps of bituminous coal into diamonds. View Cliff’s TED Talk, “The Call to Learn.”
Vigyan Singhal is President and CEO of Oski Technology. He has worked in the semiconductor and EDA industries for more than 20 years, and founded two venture-funded start-ups – Jasper (acquired by Cadence) and Elastix (acquired by eSilicon). Vigyan began his career with Cadence Berkeley Labs as a Research Scientist. He has authored more than 70 publications, 3 of which won best paper awards. Vigyan has a PhD in EECS from the University of California at Berkeley where he was a Regents Scholar, and has a BTech in Computer Science from IIT Kanpur where he graduated at the top of his class.
This event is sponsored by Synposys.