Upcoming Events

August 22-24

Oski is a proud sponsor of Hot Chips 2021.

Register here.

Design Automation Conference 2021

San Francisco, CA

December 5-9, 2021

Designer Track Presentation – Presented by Oski and Intel

Architectural Formal Sign-Off of Compression System Data Coherency

Past Events

Tuesday, March 2, 2021 15:00 PST

Oski is glad to be back at DVCon U.S. this year and to be presenting a formal verification methodology paper with NVIDIA. Join us in the “Advanced Methodologies 2” session on Tuesday, March 2, for Saurabh Chaurdia’s talk on “Detecting Circular Dependencies in Forward Progress Checkers” and discover a way to detect deadlock conditions which could otherwise be missed due to decomposition of proofs. Register here.

Technical Session Details

Paper ID 7101 Detecting Circular Dependencies in Forward Progress Checkers

Saurabh Chaurdia, Arun Khurana, Naveen Kumar, Aditya Chaurasiya – Oski Technology

Yogesh Mahajan, Prasenjit Biswas – NVIDIA

Abstract: Forward progress checkers are often implemented with embedded stall conditions, which are conceptually equivalent to implicit constraints. These constraints cannot be verified using traditional methods, such as assume-guarantee, and hence they introduce the risk of missing deadlock bugs due to circularity in the proofs. In this paper, we present a method for detecting circular dependencies in this style of forward progress checker and share results of applying this method to the blocks of a GPU system design.

January 28, 2021, 10:00 – 11:00 AM PST

Oski Decoding Formal Club Online

Sponsored by:

Qualcomm Case Study Presentation followed by Q&A Session

Proving Absence of Deadlock in High-Performance Cache Sub-Systems

Mobile SoC designs include an increasingly large number of cores and IPs which access shared memory caches. To alleviate traffic congestion from many clients, advanced cache design architectures have evolved which use a hybrid of arbiters, switches, and crossbars to optimize for throughput. Higher performance can be achieved through the widespread use of parallelism.

However, this leads to the risk of deadlock building up in the system as some ordering sequences must be preserved in data processing. Thus, designs must also incorporate deadlock avoidance schemes to counter this risk.

Proving the effectiveness of these schemes is a challenge for traditional verification methods due to the limited coverage achieved. Join us for this talk to discover how Level 4 formal verification with Abstraction Models found previously unknown deadlock bugs and delivered sign-off on the absence of deadlock in the fixed design.

Presented by: Vaibhavi Solanki, Qualcomm and Nishant Yadav, Oski Technology

New to Decoding Formal? The Decoding Formal Club is a forum for formal enthusiasts, pioneers, leaders and colleagues who work to promote the sharing of ideas, advancement of formal technology, and adoption of formal sign-off within the industry.

Wednesday October 28, 2020 15:30 – 16:00 CET

Oski Technology is glad to be back at DVCon Europe this year and to be presenting a case study with u-blox. Verification of deadlocks is one of the biggest challenges faced by many IC design teams across the industry. To learn how formal sign-off methodology solves this challenge, join Emrah Armagan and Roger Sabbagh for their talk on “Discovering Deadlocks in a Memory Controller IP”.

Technical Session Details

Paper 2.4 Discovering Deadlocks in a Memory Controller IP

Jef Verdonck, Emrah Armagan, Khaled Nsaibia, Slava Bulach – u-blox AG

Pranay Gupta, Anshul Jain, Chirag Agarwal, Roger Sabbagh – Oski Technology, Inc

Abstract: The risk of deadlocks is one of the areas that is not well addressed by dynamic testing. Simulation does not provide the tools to target deadlocks directly, so finding deadlock scenarios generally happens by chance. On the other hand, formal verification is particularly well suited to verifying a wide range of forward progress properties of designs, such as absence of deadlock, live-lock, and starvation. In this paper, we present a formal verification methodology that has been shown to predictably discover deadlock in RTL designs. The methodology is applicable in the early phases of IP development and design integration. We share results from the application of the method on an industrial memory controller IP


#AskOski Live – A Decoding Formal Club online event

Register Today

When: Thursday, September 24 2020, 10am-11am PDT

Got questions about formal sign-off? Submit them to #AskOski to have them answered live!

You’re invited to a live discussion session with Oski’s founder, Vigyan Singhal, where he will share his answers to some of the most often heard questions, such as:

What is formal sign-off and why is it needed?

Which type of designs are the best fit for formal sign-off?

Isn’t complexity a barrier to using formal for sign-off?

Attendance is limited, so submit your questions and register today.

Sponsored by:

Speaker: Vigyan Singhal, Oski Founder

Vigyan Singhal is the founder and chairman of Oski Technology. He has worked in the semiconductor and EDA industries for more than 25 years. Previously he founded Jasper Design Automation, later acquired by Cadence. Vigyan has been applying formal verification on industrial designs since verifying simulation-resistant pieces of the PowerPC 601 at Motorola, post-silicon, in 1993. Later, Vigyan was at Cadence, where he built their first-general formal verification tool. He has authored more than 70 publications and holds 14 patents in IC design and verification. Vigyan has a PhD in EECS from the University of California at Berkeley and a BTech in Computer Science from IIT Kanpur where he graduated at the top of his class.

August 16-18

Oski is a proud sponsor of Hot Chips 2020.
Oski has been involved in the development of two-thirds of the devices being showcased by major North American semiconductor companies at the symposium. Register here.

Verification Track Presentation
Using Formal Sign-Off to Deliver Bug-Free IP

Presenters:
Jay Minocha – Provino Technologies
Roger Sabbagh – Oski Technology

In this talk, Jay and Roger will explain the challenge of exhaustively verifying feature rich and highly configurable SoC interconnect IP. Taking the examples of the AXI interface controllers, they will cover the process of applying Level 4 formal sign-off methodology. They will also share examples of simulation-resistant bugs which were eradicated from the design, thereby considerably reducing the risk for design IP users.

Design Automation Conference 2020

A Virtual Experience

July 20-24

Designer Track Invited Session – Organized by Oski

Who’s Got the Ball? Pragmatic Approaches to Formal Sign-Off of Deadlocks

Wednesday July 22, 3:30pm – 5:00pm

70.1  Proving Absence of Deadlock in High-Performance Cache Sub-Systems

70.2  Covering the Last Mile in SOC Level Deadlock Verification

70.3  Starvation Avoidance Verification in Bus Interconnect Fabrics

DVCon United States

March 2-5, 2020
DoubleTree Hotel
San Jose, California
Booth #202

Schedule a DVCon US Meeting

Conference Paper Presentation

Session 1.3: Finding the Last Bug in a CNN DMA Unit

Tuesday, March 3, 10:00 – 10:30 – Session: Formal Verification I

 

Decoding Formal Club Meeting

Register Today!

When – Tuesday, December 3rd 2019, 11:30 am – 5:00 pm

Where – Conference Room C, 181 Metro Plaza, Suite 279, San Jose, CA 95110 (New)

DVCon Europe

Oct 29-30, 2019
Holiday Inn Munich City Centre, Munich, Germany
Booth 603

Schedule a DVCon EU Meeting

Conference Paper Presentation

Session 8.3: Covering the Last Mile in SoC Deadlock Verification

Wednesday, October 30, 14:15 – 14:45 – SoC Verification, Forum 7

Design Automation Conference 2019

Jun 3-5, 2019
Las Vegas Convention Ctr.
Booth 824

Schedule a DAC Meeting

Oski DAC Booth Theater Presentations. Register today!

Every attendee is automatically entered into a draw for this foldable drone with HD camera.

Reserve your seat

Formal Sign-off Meets Real-World Tapeout Schedules

How formal verification was used to accelerate the verification process and meet the challenging tapeout deadline for the Surface Write Unit of a GPU.

Monday – 1 pm

Tuesday – 2:30 pm

Wednesday – 4pm

Reserve your seat

Metrics-Driven Formal Sign-Off of PCIe PCS

A metrics-driven formal verification solution for verifying multi-clock plesiochronous Rx path of PCIe physical layer logical sub-block.

Monday – 4 pm

Tuesday – 1 pm

Wednesday – 11 am

Reserve your seat

Formal Verification of a Resource Allocator Unit

How formal verification was used to prove that a Resource Allocator Unit correctly processed any combination and sequence of input requests to allocate, update or release resources.

Monday – 2:30 pm

Tuesday – 11 am

Wednesday – 1 pm

Reserve your seat

Thwarting Inevitable Bug Escapes with Exhaustive Formal Sign-Off

Learn how to 1) predict where your next inevitable bug escape will occur, 2) find all bugs in these high-risk areas, 3) and prove that the last bug has been found. Bug escapes are no longer inevitable.

Monday – 11 am

Tuesday – 4 pm

Wednesday – 2:30 pm

DAC Designer Track Invited Session – Organized by Oski

Session 5: Stop Wasting your Verification Budget – Know when to use Formal

Monday 1:30pm – 3:00pm | Room N262

5.1  A Novel Approach to PCIe Receiver Framing Checks

5.2  Formal Verification of a GPU Shader Sequencer

5.3  Effective Formal Solutions to CPU Verification Challenges