Blog

Blog

Simulation-Resistant Superbugs – A Central Theme of Discussion at DAC

Design bugs brought about by the megatrend use of parallelism to keep pace with performance and efficiency demands in the wake of Moore’s Law finally have a name: “Simulation-Resistant Superbugs.” The topic of combating these superbugs took center stage with Oski at DAC. Check out our previous blog titled “Simulation-Resistant ‘Superbugs’ Are Here. Time to Rethink …

Simulation-Resistant Superbugs – A Central Theme of Discussion at DACRead More »

Simulation-Resistant ‘Superbugs’ Are Here. Time to Rethink Your Verification Strategy.

Simulation-resistant superbugs are on the rise and wreaking havoc in an array of design domains including CPUs, GPUs, networking, wireless, functional safety, and machine learning. These functional superbugs are resistant to simulation because extreme corner cases are required to activate and detect them. They are a side-effect of designer innovations in parallelism and concurrency to …

Simulation-Resistant ‘Superbugs’ Are Here. Time to Rethink Your Verification Strategy.Read More »

The ABCs of Winning at the 2017 Hardware Model Checking Competition

Every year for the last nine years teams of researchers and software developers have come together to compete in the Hardware Model Checking Competition (HWMCC). This contest pits some of the brightest minds in design and verification against each other along with the solvers they have developed. Each team has worked tirelessly over the course …

The ABCs of Winning at the 2017 Hardware Model Checking CompetitionRead More »

ArterisIP

Implementation of an Architectural Formal Verification Methodology by ArterisIP

Chances are you’re probably reading this blog post on a mobile device with the utmost confidence that it is doing what you intend it to do.  As consumers, we place a lot of demands on not only our mobile gadgets but also the rest of our personal electronics.  We want them to perform all sorts …

Implementation of an Architectural Formal Verification Methodology by ArterisIPRead More »

ARM

What Can Be Learned from Arm’s Implementation of Formal Sign-off

At Oski, we’ve embedded ourselves in the world of Formal verification because we truly believe in the exhaustive nature of Formal to achieve significant confidence in design and verification sign-off.  So, it doesn’t surprise me that Arm’s initial experience with Formal compelled them to employ a much deeper Formal sign-off strategy with their latest design.  …

What Can Be Learned from Arm’s Implementation of Formal Sign-offRead More »

Recap: Decoding Formal Club, Spring 2017

What better way to celebrate the arrival of spring than another meeting of the Decoding Formal Club! The Decoding Formal Club is a forum for formal verification enthusiasts, pioneers, leaders and friends who work to promote the sharing of ideas, advancement of formal verification technology, and adoption of formal sign-off methodology within the industry. On …

Recap: Decoding Formal Club, Spring 2017Read More »

Part 3: Formal Verification Program Leader: Finishing Well and Learning from the Experience

In  this 3-part blog, I’ve been examining the emerging role of the Formal Verification (FV) Program Leader, an individual who plays a critical part in adoption of FV as part of an organization’s verification strategy, and its deployment on real projects.   The FV Program Leader’s importance and value stems not from him or her being …

Part 3: Formal Verification Program Leader: Finishing Well and Learning from the ExperienceRead More »

Oski Decoding Formal Club – A First-Timer’s Perspective

It’s undeniable: I am a newcomer to the formal verification scene. As one of the newest members of the Oski team, I didn’t know what to expect when I attended the Oski Decoding Formal Club meeting on October 11th. Oski hosted the event at the acclaimed Parcel 104 Restaurant in the Santa Clara Marriott hotel. …

Oski Decoding Formal Club – A First-Timer’s PerspectiveRead More »

Another Reason to Stay an Extra Day in Austin

If you are attending the Design Automation Conference (DAC) in Austin, Texas, June 5-9, and need a good reason to stay an extra day, look no further. Oski Technology is offering a one-day primer on advanced formal verification techniques at the DAC Decoding Formal one-day training, “Achieving Formal Sign-off”, on Thursday, June 9, from 10 a.m. until 5 p.m. at the …

Another Reason to Stay an Extra Day in AustinRead More »

Oski Technology Formal Coverage Methodology: implement checkers and constraints; run formal verification and collect coverage; are coverage goals met? add abstractions and add/fix constraints; are coverage goals met Y/N?; Design is formally verified

Part 2: Formal Verification Program Leader: The Critical Role of Planning and Measurement

As  in any engineering endeavor, formal verification involves engaging individuals in many different roles, often including formal managers and, given the technically deep and complex nature of FV, nearly always one or more formal experts. The manager of the formal verification effort on a project may have formal as his or her primary or sole …

Part 2: Formal Verification Program Leader: The Critical Role of Planning and MeasurementRead More »

Achieving Formal Sign-off: Key Learnings for Trainees and Experts

Formal sign-off is possible with today’s technology and methodology. But to get to formal sign-off takes an understanding of what is possible with formal verification, and an immersion in ongoing practice with formal methods and techniques. Moreover, early experiences with formal can determine later success with formal verification and sign-off. Even with a deep knowledge …

Achieving Formal Sign-off: Key Learnings for Trainees and ExpertsRead More »

Recap of the 2016 Oski Formal Puzzler – “Chessboard Challenge” (+ Video)

In December 2015, Oski challenged formal users to solve our Oski Formal Puzzler – the Chessboard Challenge, Berkeley Math Circle Monthly Contest 8, 2011, proposed and designed by Evan O’Dorney, three-time Putnam Fellow. Jesse Bingham from Intel submitted the winning entry, as was announced during a presentation at the recent meeting of the Decoding Formal Club in Santa Clara, …

Recap of the 2016 Oski Formal Puzzler – “Chessboard Challenge” (+ Video)Read More »

Part 1: Formal Verification Program Leader: An Emerging Role in Verification

Formal verification of hardware designs has been around for more than 25 years. Commercial tools, for example from AT&T Bell Labs and IBM, started appearing in the 1990s. It’s only recently that formal verification has been adopted into design and verification flows, due to a number of reasons. It’s harder to learn than simulation or emulation …

Part 1: Formal Verification Program Leader: An Emerging Role in VerificationRead More »

Oski Holiday Challenge: Fun Formal Puzzler Entries Due by Jan. 31!

“Jingle Bells”, “Silent Night”, “We Wish You a Merry Christmas”… It has been several weeks since my youngest daughter started practicing for her upcoming violin concert. I grew up in China and missed out on the fun of Christmas festivities and holiday music. Now that we live in the United States and have had the full …

Oski Holiday Challenge: Fun Formal Puzzler Entries Due by Jan. 31!Read More »

Formal 2025: It’s Back to the Future!

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” …

Formal 2025: It’s Back to the Future!Read More »

Close Win in Oski Deep Bounds 2015 Hardware Model Checking Competion for Norbert Manthey of TU, Dresden

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, …

Close Win in Oski Deep Bounds 2015 Hardware Model Checking Competion for Norbert Manthey of TU, DresdenRead More »

Formal Ensures Tight Working Relationships

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 …

Formal Ensures Tight Working RelationshipsRead More »

Decoding Formal @ DAC – Join Oski for Four Days of Formal Fun

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 …

Decoding Formal @ DAC – Join Oski for Four Days of Formal FunRead More »

Preparing for Another Challenge at DAC: Break the Testbench!

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 …

Preparing for Another Challenge at DAC: Break the Testbench!Read More »

“Shift Left” with Formal Technology

“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 …

“Shift Left” with Formal TechnologyRead More »

The Perils of Aiming Low: How Management Expectations Can Shape Formal Engineers’ Learning and Performance

I recently read a blog written by Dr. Noa Kageyama, performance psychologist and Juilliard alumnus and faculty member, titled “The Perils of Aiming Low: How Our Expectations Can Shape Our Students’ Learning & Performance.” Based on research findings from schools and sports, Dr. Kageyama concluded that high expectations from teachers and coaches correlate positively with …

The Perils of Aiming Low: How Management Expectations Can Shape Formal Engineers’ Learning and PerformanceRead More »

Making the Case to Executives for Formal Verification

Last year, after my presentation to a customer in Asia, the verification manager said, “You should give this talk to our senior executives, so they understand the benefits of formal.” It was said in a lighthearted manner, but in reality it rang true. Design and verification engineers and their managers understand the value of formal. …

Making the Case to Executives for Formal VerificationRead More »

New Year’s Resolution – Treading Deep into Formal

According to statistics published in 2014 by the University of Scranton in Pennsylvania in the Journal of Clinical Psychology, 45% Americans usually make New Year’s Resolutions. And people who explicitly make resolutions are 10 times more likely to attain their goals than people who don’t. The largest resolution category –– 47%, is related to self-improvement …

New Year’s Resolution – Treading Deep into FormalRead More »

2014 in Review: “There’s no going back now.”

2014 has been an exciting year for advances in technology, and another successful year for Oski Technology. Applying formal verification technology to the most challenging formal verification problems has been at the core of Oski’s business for nearly 10 years, and in 2014 we continued this journey with customers and partners from more than a …

2014 in Review: “There’s no going back now.”Read More »

“What if” All Design and Verification Engineers Used Formal?

What if all design and verification engineers used formal? What if formal tools become smart enough to do the abstractions? What if formal tools had infinite capacity? These and other questions were proposed by attendees on the event survey for this quarter’s Decoding Formal Club event on October 23, 2014 at the Computer History Museum …

“What if” All Design and Verification Engineers Used Formal?Read More »

Formal Verification, by Everyone and for Everyone

You might still be skeptical of the idea that formal verification can be used by everyone. After all, there is a deep-rooted perception in the industry that formal verification is for the elite few formal experts with Ph.Ds. This might have been true in the early days of formal technology. The formal tools’ capacity was limited and the …

Formal Verification, by Everyone and for EveryoneRead More »

Using Formal for Functional Coverage

Brian Bailey’s recent article on “Fixing Functional Coverage” in Semiconductor Engineering (http://semiengineering.com/fixing-functional-coverage/) polled experts from different companies about the challenges of catching all the bugs, utilizing assertions and expanding coverage to the entire system. This blog elaborates on the four points we made in Brian’s article about how formal can help with functional coverage. Hitting …

Using Formal for Functional CoverageRead More »

Sponsoring Technical Advancement in Formal Verification

The Hardware Model Checking Competition (HWMCC) was conceived at CAV (Computer-Aided Verification) 2006 and first launched at CAV 2007. The goals were to encourage technical advancement of model checking algorithms and thereby their deployment in the industry to promote formal adoption for hardware design verification. Throughout the years, several competition tracks have been added – …

Sponsoring Technical Advancement in Formal VerificationRead More »

Debate over Formal Sign-off vs. Bug-hunting

Formal technologies have been used in many different ways in the industry including automatic formal, formal apps and so on. One of ways of using formal technology is use it for formal sign-off. Oski has developed a Formal Sign-off methodology that covers complete design functionality to ensure 100% correct design behavior according to design spec. …

Debate over Formal Sign-off vs. Bug-huntingRead More »

How Long Does It Take to Formally Verify This Design?

This year at DAC, we asked attendees to participate in a guessing game – make an educated guess about how long it takes to formally verify a design based on the given design description and statistics. Here is a recap of the information provided to participants: Design Description Reorder IP packets that can arrive out …

How Long Does It Take to Formally Verify This Design?Read More »

Win:1-Week Formal Test Planning Session with Oski Technology

Enter to Win: 1-Week Formal Test Planning Session with Oski Technology Formal test planning is the first step to ensuring successful End-to-End formal verification and formal sign-off. There are 3 stages in the process of formal test planning – identifying the right design blocks for formal verification (the where question); estimating the formal verification effort …

Win:1-Week Formal Test Planning Session with Oski TechnologyRead More »

Building Up the Formal Community

In our visits to many of our customers in the past year, we received a few common requests from companies both large and small: Can you help us find formal expertise to hire? Can you train our engineers to become formal experts? Can you help us build an internal formal team – fast?

Oski Receives DVCon “Honorable Mention” for Best Paper Bounded Proofs

DVCon 2014 was a successful show for Oski Technology. Not only were we proud to receive an “Honorable Mention” for (2nd) Best Paper at DVCon “Sign-off with Bounded Formal Verification Proofs”, we had the opportunity to have many meaningful conversations with existing customers and others new to formal verification and eager to learn more about …

Oski Receives DVCon “Honorable Mention” for Best Paper Bounded ProofsRead More »

Countdown to DVCon 2014

The countdown to DVCon 2014 has begun! With more exhibitors and attendees than ever before, new programs and technical sessions, longer exhibit hours, DVCon 2014 is shaping up to be another outstanding event for the industry. At Oski Technology, we are excited to offer many opportunities to connect with verification experts in the industry at …

Countdown to DVCon 2014Read More »

Verification Management from a Formal Perspective

Recently, Gabe Moretti, contributing editor to Chip Design, wrote a lengthy article for Systems Design Engineering addressing an important topic, “Verification Management.” It included comments from Atrenta, Breker Verification Systems, Jasper Design Automation, Mentor Graphics, OneSpin Solutions, Oski Technology and Sonics on a series of questions from Gabe on how to manage today’s complex and …

Verification Management from a Formal PerspectiveRead More »

The Abstraction Model – Is It More, Is It Less?

Oski Technology provides formal verification services to leading semiconductor companies to verify complex design blocks that are difficult to verify using simulation. In our projects, we often write Abstraction Models to overcome formal complexity barriers that would otherwise render formal verification results inconclusive. For example, for the open-source Sun OpenSparc T1 design, verifying a data …

The Abstraction Model – Is It More, Is It Less?Read More »

Oski Innovation Enables Formal Sign-Off ™ in 2013

A busy year is drawing to a close for Oski Technology. Reflecting back on this year we are proud of what we have accomplished for our valued customers. Oski Formal Sign-Off ™ Methodology, incorporating End-to-End checkers, Abstraction Models and formal coverage – this is the boldest application of formal technology for RTL functional verification. Gone …

Oski Innovation Enables Formal Sign-Off ™ in 2013Read More »

Promoting Formal Education: Oski Shares Experiences at FMCAD 2013

Although Oski Technology is first and foremost a formal verification service company, making effective use of formal tools and promoting education around the power of formal technology has always been at the core of our business. Since Oski was founded in 2005, we have engaged in many activities to help increase the adoption of formal …

Promoting Formal Education: Oski Shares Experiences at FMCAD 2013Read More »

Oski’s Two New Secure Chambers Support Asia Growth

Oski Technology, founded by Vigyan Singhal, pioneer and practitioner in formal verification, has earned great respect and reputation in the Silicon Valley for helping customers tape out mission-critical projects using formal technology. Leveraging the power of End-to-End formal verification and Abstraction Models, Oski works with its customers to adopt formal sign-off methodology so that formal …

Oski’s Two New Secure Chambers Support Asia GrowthRead More »