Pippa Slayton is Marketing and Business Development Manager at Oski Technology. She has 8+ years experience in the high-tech industry and drives marketing campaigns, marketing strategy, product launches, social media, and community building and event program management for Oski’s formal … More »
November 13th, 2015 by Pippa Slayton
The recent Decoding Formal Club meeting hosted by Oski Technology on October 21, 2015 at the Computer History Museum in Mountain View celebrated the club’s 2nd anniversary with a “back to the future” twist.
While many of the predictions in the movie “Back to Future Part II” did not come true on October 21, 2015, the day of “the future” to which Marty McFly and Doc Brown time travel in a flying silver DeLorean sports car, that didn’t deter us from inviting attendees from Apple, ARM, Arteris, Broadcom, Ericsson, Google, Imagination, Microsoft, NVIDIA, Palo Alto Networks, Qualcomm and others to make some timely predictions for formal verification in 2025. The group was comprised of formal experts with years of experience, as well as engineers who are new to formal verification, so the predictions for 2025 were daring, but quite possible.
Close Win in Oski Deep Bounds 2015 Hardware Model Checking Competition for Norbert Manthey of TU, Dresden
October 29th, 2015 by Pippa Slayton
This year’s Oski Deep Bound Track Hardware Model Checking Competition (HWMCC) was a thrillingly close contest that came down to just one benchmark design of more than 100 benchmarks. The winner was announced at the Hardware Model Checking Competition Report session of the annual Formal Methods in Computer-Aided Design (FMCAD) Conference, held in Austin, Texas, on September 30, 2015. Winner Norbert Manthey of the Institute of Artificial Intelligence and a graduate of TU Dresden, Germany, took the prized first place from runners up Alberto Griggio, and Marco Roveri, researchers at Fondazione Bruno Kessler, and graduates of the University of Trento, Italy.
September 24th, 2015 by Pippa Slayton
On the radio yesterday, we heard that the song “Happy Birthday To You”, one of the most widely sung tunes in the world, was ruled by federal judge George H. King to finally be in the public domain!
This welcome news seems to come at the right time, as Oski Technology plans to celebrate the second anniversary of the Decoding Formal Club at our quarterly meeting on October 21 at Computer History Museum, in Mountain View.
Since it was founded in October 2013, the Decoding Formal Club has drawn the attention of engineers, designers and verification managers. In a relatively short time we have covered much ground, and become a forum where formal knowledge and experience can be shared among the growing community of formal enthusiasts. In turn, Oski’s featured presentations have covered many aspects of formal sign-off methodology: Bounded Proof, Abstraction Models, Formal Test Planning, End-to-End Checkers and Constraint Management.
September 9th, 2015 by Dr. Jin Zhang
Gabe Moretti of Chip Design used several points from Jin’s blog post below, in his recent article titled, “Design and Verification Need a Closer Relationship.” The article can be found at: http://bit.ly/1fGyXW2
Today, verification engineers have a whole arsenal in their tool kit in order to combat hidden bugs in the design. Different verification techniques render different working relationship with the designers.
Formal verification is a white-box verification technique, which means formal engineers need to have a good understanding about the internals of the design in order to do effective formal verification. Therefore, formal engineers and RTL designers naturally have a much tighter working relationship than other disciplines.
First, a sound verification methodology should allow equal contribution from all effective techniques, which includes leveraging the exhaustiveness of formal to sign-off on design blocks that are harder to verify with simulation. The block partition between formal and simulation should be clean to simplify the effort on both ends. To achieve that, formal engineers should participate in the architectural planning and exploration stage of design development in order to help influence decisions regarding design partition and block interface. A well-partitioned design with a clean interface will make the decision on where to apply formal, as well as the actual formal verification tasks, much easier.
August 12th, 2015 by Dr. Jin Zhang
EDA’s verification market segment is not the only place where something’s named for the Cal (University of California, Berkeley) mascot Oski. A Blue and Gold Fleet boat named Oski sails out of Pier 39 in San Francisco and takes visitors around the Bay and Alcatraz.
When I saw the Oski pulling away from the pier, I couldn’t help but draw an analogy between Oski Technology’s mission and the choppy waters the boat was heading into on that sunny day. Sunny days and choppy waters are something verification engineers can face on a daily basis. Verification tasks are so challenging in today’s for system-on-chip (SoC) designs that verification alone takes more than 60% of the project cycle. What’s more, simulation alone for SoC designs will leave large holes for bugs to sneak through, all the way to silicon. The challenge of verification actually is more daunting than the choppy waters of San Francisco Bay.
June 19th, 2015 by Dr. Jin Zhang
The story of Louis Zamperini, as told by Laura Hillenbrand in “Unbroken: A World War II Story of Survival, Resilience, and Redemption”, is a great testimony of the strength of human spirit. Going through unimaginable catastrophes, including drifting 47 days on the open sea with leaping sharks, thirst, starvation, and machine gun attack from a bomber plane, as well as enduring 3 years under severe and brutal conditions as a POW in Japan, Zamperini emerged unbroken with grace, humanity and love.
This is such an inspiring story that when I thought about writing about Oski DAC 2015 “Break the Testbench” Challenge results, the word “unbroken” came to mind. While this is no comparison in its scale to the story of Zamperini, the word “unbroken” succinctly summarizes the challenge result.
June 6th, 2015 by Dr. Jin Zhang
Oski Decoding Formal Events are usually hosted at the Computer History Museum in Mountain View and have attracted lots of formal enthusiasts in the bay area. Deep formal talks from Oski, lectures given by formal experts from different companies, good networking, cool gifts and museum tours have become the signature of these events that formal engineers look forward to, every quarter.
To reach out to formal enthusiasts around the world and create a bigger event than usual, the 2015 Q2 Decoding Formal event will be hosted at DAC. Our theme is proving completeness of End-to-End Formal for Sign-off.
May 18th, 2015 by Dr. Jin Zhang
You may remember the Oski Technology Live Verification Challenge in 2012, where during the 72 hours of DAC, Oski verification engineer Chirag Agarwal formally verified a well-simulated design from NVIDIA, sight unseen, live and on camera, and found 4 corner case bugs. The challenge results exceeded everyone’s expectations, and inspired other companies to do more with formal in their verification flow. See the Live Oski Verification Challenge, and a blog recap and six-minute video, here.
May 1st, 2015 by Dr. Jin Zhang
My daughter has been learning violin for the last 5 years with a wonderful Suzuki teacher. She emphasizes proper posture, beautiful tone and a good work ethic. This has built a solid foundation for my daughter to venture into learning other instruments. Last fall my daughter started playing flute for her school band, and viola at Young String Ensemble, the youngest division of Portland Youth Philharmonic, founded in 1929 as the first youth orchestra in the United States.
To help her prepare for the upcoming audition for the more advanced Portland Youth Conservatory Orchestra, we decided she would take some viola lessons with the Oregon Symphony Principal Violist. We were totally blown away after just one lesson.
April 1st, 2015 by Dr. Jin Zhang
“Shift Left” has become a hot phrase after Aart’s keynote speech at DVCon2015 where he talked about how shifting left in schedule resulted from 10x productivity gain in design, IP, verification and software can spur on 100x opportunities in applications across all fields. He suggested many of these technological advances have the potential of changing what mankind is all about.
Static and formal techniques were mentioned as one of the mechanisms that increase productivity and contribute to shift left in the verification schedule. There are several reasons why formal technology is a key driver for the left shift.