Video: Oski 72-Hour Live Verification Challenge DAC 2012

Video: Oski 72-Hour Live Verification Challenge DAC 2012

Oski hosted a live 72-hour formal verification challenge at DAC 2012, from June 3-6, 2012. It was about taking a new customer design, sight unseen, and formally verifying it in a limited time. The live challenge was streamed to the DAC floor, with real-time results on Twitter.

View the DAC 2012 Oski Challenge Wrap-Up & Video Wrap-up blog with photos, here: http://goo.gl/8aonNV

Click here for more information about the Oski 72-hour Live Oski Verification Challenge, and a wrap-up blog.

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 Hilton Hotel, Austin.  Continue reading

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 responsibility, or may manage multiple aspects of verification (e.g. both simulation and FV). However, even a full-time formal verification manager may or may not drive the overall formal program in their company or organization.

In part one of this discussion, I talked about the emerging role of the Formal Verification (FV) Program Leader, an individual who enables and drives the formal process by navigating organizational dynamics, understanding designs and their verification complexities and schedules, developing and presenting ROI trade-offs, etc.; all to help achieve project goals. I listed six aspects of this role that the FV Program Leader must master in order to effectively lead the adoption and deployment of formal verification: Organization, Training and Upskilling, Test Planning, Progress Metrics, Sign-off Process, and Post Mortem Analysis.

In the previous blog, I talked in more detail about the first two aspects: the organization of formal, and the structure and growth of the internal formal team; and training and upskilling of that team, meaning internal vs. external, structure and style of training. What follows is a discussion of two additional aspects of the role of the FV Program Leader that are crucial to the effective deployment of in-house formal verification in any organization: test planning and measuring progress via quantitative metrics.

Test Planning: Any formal project should begin with an examination of the reasons why formal verification is being used in addition to simulation – is the goal to supplement simulation by finding some corner-case bugs, to provide an environment for designers to bring up their designs as quickly as possible, to thoroughly test a specific feature, to replace block-level simulation entirely, or to provide system-level architectural properties? Answering these questions, and documenting the plan of execution comprises this test planning stage. This includes selection of what level(s) of formal will be used, what blocks are the best targets for formal and will return the best bang-for-the-buck, detailed scoping of the formal effort for those blocks, and a written test plan and schedule for the formal work. It must be determined what level(s) of formal should be implemented: architectural formal verification, end-to-end formal verification of RTL blocks, and/or employment of formal “apps”. The expertise of the formal team available must be mapped to the specific formal tasks chosen. A significant decision to be made at this stage is how the system or subsystem should be partitioned into those portions to verify with formal and those to verify with simulation – some blocks yield a much higher return-on-effort with formal than others. Blocks chosen for formal must be scoped to determine the magnitude and complexity of the formal verification effort for them, and detailed lists of formal checkers to be written (i.e., the formal test plan) must be created. Depending on the organization of the overall verification team, the formal team might be encouraged to work closely with the simulation team; including re-using formal properties, especially constraints, in simulation; as well as addressing simulation coverage holes using formal verification. The formal engineers might need to collaborate with each other to re-use properties, especially across their design interfaces, particularly if an assume-guarantee methodology is being used. Decisions need to be made as to whether there is value in validating formal constraints in simulation, as well as whether formal coverage will be deployed to measure the completeness of the formal work. The FV Program Leader will typically drive and coordinate these activities, as well as mapping the formal test plans to the tapeout schedule. These test plans will include progress metrics that help measure the progress of the formal team.

Progress Metrics: Historically, an Achilles’ heel of formal verification has been the ability of the formal team to predictably converge on the formal verification goals laid out at the beginning of the project. In executing the test plans, formal verification engineers face considerable barriers to predictability that are unique to FV. These include coming up with a complete list of checkers (with or without designer help), converging on a set of constraints by working through a series of false negatives, achieving proof convergence especially in the face of the exponential proof complexity, and measuring formal coverage to justify the completeness of the formal work. Once test planning is complete and the formal project is underway in earnest, measuring and reporting progress metrics will offer insights into how the project team is doing, provide a vehicle to measure each formal area, and provide critical visibility for management into progress and completion of each piece of the formal project. These metrics will include things such as number/percentage of checkers written, passing and failing; abstraction models completed; proof depth(s) required and achieved; number of constraints passing or failing; and formal coverage metrics that have recently become available in formal tools. At this stage a knowledgeable FV Program Leader will be able to decide whether adequate human and tool resources have been assigned for formal, and whether they are distributed properly or need to be reassigned; and whether the division of blocks and/or allocation of resources to formal versus simulation needs to be reevaluated if one or the other is falling behind. Depending on the specific design as well as what is being verified on it, the amount of work can be dominated by different aspects; such as work on building the checkers, on converging on the right set of constraints, or on managing proof complexity. While the formal test planning stage is meant to predict which aspects might be the long poles, the metrics help to judge the accuracy of those predictions during the project; and determine whether course-corrections are needed. Another task of the FV program leader in this phase is to decide whether to use formal regression testing, not as universally used as in simulation.

The last two aspects of the FV Program Manager’s role are the Sign-off Process and Post Mortem Analysis, which I will cover in the third and final installment of this multi-part blog. Meanwhile, if you are interested in learning about the Oski formal verification methodology, join us on June 9 for our Decoding Formal Training Day at DAC 2016 in Austin, Texas, where we will dive deep into end-to-end checkers, abstractions, managing proof complexity and formal coverage.

Oski Technology at DAC 2016

Oski Technology "Decoding Formal" Club Event October 2013

The Decoding Formal Club returns to DAC!  Please visit us at the Oski Technology DAC Booth #339 and our other DAC presentations and talks, and pre-register for our Decoding Formal Training Day: “Achieving Formal Sign-Off” on Thursday, June 9.

Register: Decoding Formal Training Day June 9, Austin Hilton

Join us for the Decoding Formal Club “Achieving Formal Sign-off” Training Day in Austin, Thurs. June 9, 10:00am – 5:00 pm, Hilton Hotel, Austin. Pre-registration is required. This is a full-day training program presented by Oski Technology, and covers writing end-to-end formal checkers, dealing with formal complexity, using abstraction models, managing constraints and using formal coverage. This event is Sponsored by Synopsys. Space is limited and you must register in advance.  Fee: $199.  Purchase tickets here.

Visit Oski at DAC Booth #339 for a “Live” Demo

Visit Oski at booth #339 to view a “live” case study and technical presentation that shows how a well designed set of end-to-end checkers and associated reference models can comprise a formal testbench that reaches greater proof depths, and can enable formal sign-off. See how Abstraction Models and other special techniques such as symbolic variables can be used to implement more efficient End-to-End Formal checkers, and formal coverage can be leveraged to measure the completeness of a formal testbench and track formal verification progress.

Other Oski Events at DAC

  • DAC Design Track “How to Verify the Gordian’s Knot of System Complexity” Ballroom E: June 8, 2016 1:30 pm – 3:00 pm. Vigyan Singhal, Oski’s CEO, will be part of this Design Track invited presentation session. The talk, entitled “Formal Verification: From Flops to Cones to Blocks to Systems” will discuss the history and evolution of formal adoption in the industry, from equivalence checking in the 1990s, to system level verification today.
  • “Using a Chessboard Challenge to Discover Real-world Formal Techniques” Verification Academy: June 8, 2016 3:00 pm – 4:00 pm. Prashant Aggarwal, Oski Principal Engineer will be at the Mentor Graphics DAC booth 839. This presentation will describe the challenge Oski gave formal users to solve a chessboard problem, an opportunity to show how formal techniques might be used to solve a puzzle, along with the winning solution from Intel’s Jesse Bingham.

About the Decoding Formal Club

The Decoding Formal Club is an open forum hosted by Oski Technology and offering a variety of talks and conversations on formal verification methodology, from big picture theory to a deep dive analysis of formal verification for formal sign-off. These meetings and events bring together design and verification professionals for meaningful conversations that make formal verification accessible and understood. Join us to learn about core tools and methodologies your formal verification team can use to enhance your verification capabilities.

Visit the Decoding Formal Club page: www.oskitechnology.com/decodingformals
Oski Technology Mailing List: Subscribe

Decoding Formal DAC Training Day: Achieving Formal Sign-Off

Oski Technology "Decoding Formal" Club Event October 2013
Registration is now open for the Decoding Formal: “Achieving Formal Sign-Off” DAC Training Day on Thursday June 9, 2016 at the Hilton Hotel, Austin, TX. This full day of training on formal verification has a packed agenda, with lunch included. Paid pre-registration is required. Check out the details below, and buy tickets here. The Decoding Formal DAC Training Day is co-sponsored by Synopsys.

Thursday June 9, Hilton Hotel
Decoding Formal DAC Training Day*: Achieving Formal Sign-Off
Time: 10:00 AM – 5:00 PM
Description: Formal sign-off is possible with today’s technology and methodology, but to get to formal sign-off takes knowledge of formal verification and immersion in ongoing practice with formal methods and techniques. The Oski Decoding Formal ”Achieving Formal Sign-Off” training day at DAC will discuss key components of Formal Sign-Off Methodology, with the goal of achieving formal sign-off.  The Decoding Formal DAC Training Day is co-sponsored by Synopsys. Fee: $199. Pre-registration is required.

About the Decoding Formal Club

The Decoding Formal Club is an open forum hosted by Oski Technology and offering a variety of talks and conversations on formal verification methodology, from big picture theory to a deep dive analysis of formal verification for formal sign-off. These meetings and events bring together design and verification professionals for meaningful conversations that make formal verification accessible and understood. Join us to learn about core tools and methodologies your formal verification team can use to enhance your verification capabilities.

Visit the Decoding Formal Club page: www.oskitechnology.com/decodingformals
Oski Technology Mailing List: Subscribe

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 because of its complexity, and it takes time for a verification engineer to become proficient in using it. Formal verification experts typically learn 100s of different techniques over the course of their careers.

Now that we are in the era of formal verification, an important new role is emerging –– the Formal Verification Program Leader (FV Program Leader). This individual has the mandate to drive the formal effort in the organization, and is tasked with managing the entire formal process.  He or she is usually organized, meticulous, an excellent communicator and an even better process manager, able to take a systematic approach to problem solving. This work is separate from the work done by an expert user of formal verification.

Today, this leadership role is emerging in almost every large semiconductor organization deploying formal verification on any significant scale, whether by circumstance or intent. It exists because formal verification is more complex than simulation; and senior ASIC management, while well versed in simulation and emulation, has little understanding of formal verification from the standpoint of process or return-of-benefit. Many ASIC managers wouldn’t know where formal verification works or doesn’t work and why, what designs it is good for, or what level of expertise is needed. How to include formal as part of a complete verification strategy, where and when to start formal, and how to synergistically combine it with simulation are strategic decisions few managers would be able to make effectively, either.

Engineers who are experts in formal verification methods often have a hard time communicating the level of difficulty of what they are trying to accomplish, or determining and expressing a schedule for formal verification. They may not know how to properly express the planning needed to implement formal verification to senior management, who doesn’t know formal (and may never know it). Formal tools don’t address these issues.

Companies in this situation have a difficult time building formal verification capability and deploying it. More important, perhaps, demonstrating a return on investment (ROI) for formal verification is different than for simulation; it is difficult to measure progress and, consequently, justify the investment.  Therefore, the role of the Formal Verification Program Leader is important.

Our industry lays claim to about 100-200 formal users who would be considered experts. FV Program Leaders have an even rarer skillset. Only a handful of people –– 20 at most –– could be considered FV Program Leaders.

The FV Program Leader drives the formal effort. A FV Program Leader may not come from a formal background, because expertise as a formal user is independent of formal program leadership. While FV Program Leaders need not be formal experts, they must be good at evangelizing formal, and pairing formal with other technologies. They are skilled at managing the formal process, effectively communicating with both upper management and engineers, assessing ROI and presenting the results to justify investment in formal verification, and influencing the formal roadmap. Success as an FV Program Leader does not require mastery of formal techniques, but implementing a successful formal verification program does require mastery of the processes.

The FV Program Leader’s role involves breaking down the abstract, translating it into familiar planning terminology, and providing insight as to the team’s progress relative to the plan. He or she must be able to interact and collaborate with the owners of the various ASIC projects, and should have the ability to leverage the formal process by understanding designs, schedules, and potential trade-offs to achieve project goals.

To be integrated into the verification flow, formal verification should not be treated like a separate island. Changing the perception that formal verification is somehow insular and distinct from the rest of the verification effort may be the biggest challenge for, but also the most important task of any FV Program Leader. The role of Formal Verification Program Leader, while not for everyone, is a critical one for companies making an investment in formal. It’s highly visible and ready-made for a capable individual who’s a good communicator, is able to manage tradeoffs and is a strong process leader.

There are six areas an FV Program Leader needs to think about: Organization, Training and Upskilling, Test Planning, Progress Metrics, Sign-off Process, and Post Mortem Analysis. A structured approach like this is not new to engineering, but it is new to formal verification. When addressing these six areas, formal can be incorporated seamlessly into the design flow, along with other traditional tools and methods. In this blog, I will discuss the first two of these six areas, and will cover the others in future posts.

Organization: Since the FV Program leader is chartered with building the program for an entire organization, involving multiple ASIC designs across many groups, and perhaps multiple geographies, the first question that needs to be addressed is how a formal team will be organized, within the existing organizational hierarchy. Will there be a centralized group of formal engineers (full-time or part-time?) reporting to a single manager, who may be the FV Program Manager, servicing multiple ASIC projects that are spread across the organization? Or is it better to have the formal engineers distributed among the project groups? The former is better if the organization is flexible enough to allow collaboration across organizational boundaries. Formal verification is a unique skill set in that its value is enhanced when ideas and strategies are shared by a team of skilled formal engineers supporting many different customers across the globe, and working under one roof. The question of a full-time vs. part-time focus for the engineers working with formal is also related to what scope will be verified; some applications of formal verification such as automated checking, or formal apps, are amenable to part-time work. However, if end-to-end formal verification is applied to replace unit-level simulation, it must almost always be executed by full-time formal verification engineers. We have seen some large organizations budget 15% of their entire verification manpower to full-time formal verification, with successful results. Another aspect of organization is mobility and career path. Will non-formal engineers be given an opportunity to move to a centralized formal verification team? Will formal engineers have an opportunity to learn other skills? As formal engineers succeed, how do we manage their career path? Will the building of a formal team be done by hiring experienced formal engineers? This is a difficult path, as there are few experienced formal engineers in the industry, perhaps fewer than 200. Or, is it better to hire and extensively train new college graduates?

Training and Upskilling: The learning curve for formal verification can be long. Having practiced formal verification for 23 years, I am still learning new techniques. Humility and the quest for learning is key to continuously building this expertise. If the formal team is comprised of engineers who are new to this area, a rigorous training program must be put in place. Our internal 10-course training program is a requirement for our new hires who have limited experience with formal.  More important than that is what follows – an apprenticeship-style training where a new formal verification engineer is coupled with more senior, experienced formal verification engineers. The road to success in formal verification is a challenging one, and it is important to receive guidance as one encounters failures, which could come in many forms – dealing with proofs that do not converge, numerous false failures and constraint iteration, missed bugs because of incomplete checkers, vacuously false proofs, etc. Some companies have gone through a more formalized training program by partnering with Oski, and having an Oski expert mentor one of their new formal engineers and/or provide classroom-style training. We have built a skillset chart of more than 40 different skills required by formal verification engineers. It is also important to understand both the background and aptitude of the formal verification engineers. Are they more analytical (mathematical) or practical (like engineers)? Formal verification is a very white-box style of verification. It is hard to enjoy this work if you do not like debugging or getting deep into others’ code. A formal verification engineer has to love debug, because most of the time he or she will debug false failures, as it is rare to find a designer with enough patience to iterate through formal verification false failures.

Test Planning, Progress Metrics, Sign-off Process, and Post Mortem Analysis are the other four areas the FV Program Manager should be concerned with. These will be covered in later installments.

Oski to Exhibit at DVCon 2016

Oski Technology will be exhibiting at DVCon 2016 booth #205, Feb. 29-March 2, San Jose, CA, where Oski’s Prashant Aggarwal will be presenting a paper titled “The Process and Proof for Formal Sign-off – A Live Case Study”.

Event: Oski Technology Exhibits at booth #205
Time: Monday Feb. 29, 5:00pm-7:00pm; Tuesday March 1 and Wednesday March 2, 2:30-6:00pm.
Venue: Oski Booth #205, DVCon, DoubleTree Hotel, San Jose, California.
Web: Oski Technology at DVCon booth #205

Event: Regular Session for Formal Techniques: 12.2 The Process and Proof for Formal Sign-Off – A Live Case Study
Time: Wednesday March 2, 3:00pm-4:30pm
Venue: Fir meeting room, DoubleTree Hotel, San Jose, California.
Speaker: Prashant Aggarwal – Oski Technology, Inc.
Authors: Ipshita Tripathi – Oski Technology, Inc., Ankit Saxena – Oski Technology, Inc., Anant Verma – Oski Technology, Inc. Prashant Aggarwal – Oski Technology. For more information, please visit the DVCon listing for the regular session on Formal Techniques at DVCon.

Visit Oski Technology www.oskitechnology.com
Oski Technology is the world’s only dedicated formal verification service provider. Oski’s Formal Sign-off Methodology™ uses end-to-end checkers, constraints, Oski Abstraction Models™ and formal coverage metrics to catch corner case bugs, replace simulation for the blocks verified, and improve overall verification efficiency. Oski has provided formal verification services to many leading semiconductor companies including Cisco, Cypress, NVIDIA, Rambus and Xilinx to tape out critical projects, establish formal sign-off methodology and develop customer formal expertise. Oski is a formal sign-off company.

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 holiday experience, I learned that Santa Claus comes to town – two months early!

With the holiday season upon us and reflecting on the past year, 2015 has been a very busy and rewarding time for Oski. The hard work put in by each of our colleagues is paying off – with the growing adoption of formal technology and formal sign-off methodology at many companies across the globe. Formal Verification is finally coming to town!

We would like to thank colleagues, customers, partners, friends, families, and everyone in the industry for their support in helping us succeed in our mission – maximizing the power of formal technology to enable innovative SoC designs and formal sign-off. More than in any time in the history of Oski and the semiconductor industry, formal has gained its rightful place in the design and verification flow. 2016 will be an even better year and we will continue our efforts in contributing to that history.

We at Oski like a good challenge, so what better gift to leave with you for the holidays, than a fun formal puzzler* – the 2016 Oski Formal Puzzler Chessboard Challenge!

Here it is –

formal-puzzler-chessboard_2015

On a 5 × 5 chessboard, a king moves according to the following rules:

  • It can move one square at a time, horizontally, vertically, or diagonally (these are the usual moves of the king in chess).
  • It can move in each of the eight allowable directions at most three times in its entire route.

The king can start at any square except the center. The goal is to determine:

  • Whether the king can visit every square.
  • Whether the king can visit every square except the center.

(*This puzzle is from Berkeley Math Circle Monthly Contest 8, 2011, and was proposed by Evan O’Dorney.)

You can try to solve the problem with paper and pencil. But for those of you familiar with running formal verification tools, we challenge you to solve it with your favorite formal verification (model checking) tool:

  1. Write a Verilog module to implement the moves for the chessboard – in every clock cycle the king makes one move and the state of the chessboard changes. The specific move is dictated by an input to the module.
  2. Allow the reset state to be any of the 24 squares except the center.
  3. Add constraint(s) to enforce that there are no more than three moves in any of the eight directions during the entire route.
  4. Implement two checkers that fire if the final conditions (a) or (b) are achieved, respectively.
  5. Run the model checker to see if you can get a proof, failure or a bounded proof for the checkers!

For further credit and to make the problem easier for the formal tools, try using reductions based on symmetry, or creating simpler checkers and using assume-guarantee, or any of your favorite formal verification techniques, including abstractions. For example:

  • You could over-constrain the reset state to be one of the 6 squares in top-left quadrant of the chessboard, exploiting the fact that the board and the moves are symmetric, and that means the correctness of the checkers will not be violated by making this reduction.
  • You could add a checker that at any state, the number of unvisited squares must not exceed the number of moves left (a simplification of a more complex pruning idea due to Joe Trapasso of NVIDIA). This smaller checker might be easier to prove, and can be assumed to make the proof for (a) or (b) easier.

Send us your paper-and-pencil solutions, or your Verilog programs, for the above. Use any techniques to simplify the problem. We will run your program in formal tools and see whose Verilog testbench runs the fastest. The winner will be announced at our next Decoding Formal Club meeting Monday, Feb. 29 at the Parcel 104 restaurant at the Santa Clara Marriott, where we will also discuss why certain techniques work better than others. (Registration is required. Pre-register, here). In addition, we will discuss how this chessboard problem related to structures often seen in hardware Verilog designs, like controllers managing linked lists, arrays, FIFOs, sets, tags, etc.

Please join us in taking our fun holiday Formal Puzzler Chessboard Challenge! Send your Chessboard Challenge solution to the email below. Three winners and the first 5 entries will receive special prizes, so don’t delay! We’ll post #formalpuzzler on twitter @oskitech.

Email your 2016 Oski Formal Puzzler Chessboard Challenge solution to formalpuzzle@oskitech.com. We’ll post updates: #formalpuzzler on twitter @oskitech.

Happy Holidays!!

HappyHolidaysOski-2015

 

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” 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 some are quite possible.

1. Formal will replace simulation
2. Verification will use 80% FV + 20% DV
3. The processors/tools will be powerful enough to check/prove any design in an unbound cycle.
4. Formal will replace simulation for unit testing
5. FV will be mature enough to support plug-and -play HW IP components.
6. No constraints written by a human will be needed
7. Formal will be the sign-off tool
8. Formal will scale to full subsystems of very large chips
9. We will be able to specify properties at higher levels of design/abstraction

We believe that in the next ten years formal will become the default verification strategy in the verification flow, routinely used to sign-off at the unit level. This is already possible today. The obstacle is not in formal technology or even lack of methodology. Instead, the barrier for broad adoption is that early adopters have experienced failure, and discovered how difficult it is to succeed without a solid strategy.

Will the technology advance enough wherein formal can be applied to any design without an unbounded cycle? This is an audacious prediction, but is surely possible. We may need quantum computing to assist, and true artificial intelligence in formal verification, to learn and reapply. This prediction appeals to us because it holds a bold “back to the future” vision, without which no advance in formal is possible.

We didn’t just focus on the future at our Decoding Formal event. We also focused on techniques readily available today that make the application of formal verification successful. Prashant Aggarwal, principal engineer from Oski Technology covered how to ensure the formal testbench is complete. Kenny Xing, principal design engineer, shared Broadcom’s success in verifying PCACHE using creative coloring techniques. Yogesh Mahajan, engineer from NVIDIA and Vigyan Singhal from Oski, talked about compositional gotchas. Both the Broadcom paper and NVIDIA presentation are available for download under the technical papers section on the Oski web site.  Attendees gave very positive feedback about these presentations, rating them as engaging, appropriate and focused.

With so much planned for the event, we wrapped up the day, slightly past our scheduled ending time – but aptly, just before 4:30 pm., with one highlight and popular prize drawing worth a mention. Not a replica of the silver DeLorean sports car in the movie, of course, but instead a beautiful midnight silver metallic diecast model of the Tesla Model S P85, shown below. Just like Tesla, who is pioneering and revolutionizing electric cars and helping our world to become a cleaner place, Oski is revolutionizing the way we approach the verification flow, and helping companies find bugs earlier on in the process. We are looking forward to the next Decoding Formal Club meeting in Q1, 2016 and keeping our sights on 2025, when we are optimistic that many of these predictions will have come true.

Drawing Prize: Tesla diecast Model S
A Tesla diecast Model S drawing prize, presented at the 2nd anniversary of the Decoding Formal Club, held at the Computer History Museum, Oct. 21, 2015. 
Vikas-Chandra_ARM_mobile-security
Vikas Chandra of ARM talks about mobile hardware security at the Decoding Formal Club meeting, Oct. 21, 2015 at the Computer History Museum. 
Networking at the Decoding Formal Club meeting Oct. 21, 2015.
Networking at the Decoding Formal Club meeting Oct. 21, 2015.
Vigyan Singhal cuts cake at the 2nd anniversary of the Decoding Formal Club meeting, Oct. 21, 2015.
Vigyan Singhal cuts a cake to celebrate the 2nd anniversary of the Decoding Formal Club and Oski Technology’s 10th anniversary in business, Oct. 21, 2015.   
Prashant Aggarwal delivers presentation on the Completeness of End-to-End Formal Testbench for formal sign-of at the Decoding Formal Club meeting Oct. 21, 2015.
Prashant Aggarwal delivers presentation on the Completeness of End-to-End Formal Testbench for formal sign-of at the Decoding Formal Club meeting Oct. 21, 2015. 
Kenny Xing, principal design engineer at Broadcom delivers presentation on Creative Formal Techniques to Verify PCache at the Decoding Formal Club meeting Oct. 21, 2015.
Kenny Xing, principal design engineer at Broadcom delivers presentation on Creative Formal Techniques to Verify PCache at the Decoding Formal Club meeting Oct. 21, 2015.

Networking at the Decoding Formal Club meeting Oct. 21, 2015.
Networking at the Decoding Formal Club meeting Oct. 21, 2015.

Oski Technology Names Chief Operating Officer Dave Parry Brings Extensive Engineering, Executive-Level Experience

MOUNTAIN VIEW, CALIF. –– October 20, 2015 –– Oski Technology, Inc., the only dedicated formal verification service provider, today appointed Dave Parry to the newly created role of chief operating officer.

Parry, an experienced executive who has contributed to and led ASIC and system development for high-performance computing and networking, and system-on-chip (SoC) interconnect intellectual property (IP), reports to Vigyan Singhal, Oski’s president and chief executive officer.

“Dave’s impressive background and understanding of the semiconductor industry neatly complements the skills the Oski team has, and we’re delighted he joined Oski,” notes Singhal. “His extensive knowledge about processors, servers, interconnects and networking designs will be valuable to our formal verification work.”

Most recently, Parry was vice president of engineering at Arteris, where he recruited and built an engineering team to develop next-generation SoC interconnect fabric IP. At Silicon Graphics, Inc. (SGI), he served in product development and leadership roles for multi-processor systems, with his last role being senior vice president and general manager for Server Products and Operations. Subsequently, Parry was vice president of engineering for Solarflare Communications where he led the development of controller ASICs, adapter cards and software for high-performance 10GbE and 40GbE networking products. Earlier, he was employed by MIPS Computer Systems and Hewlett-Packard.

Parry has seven granted and one pending U.S. patent in microprocessor, system and SoC design. He holds a Bachelor of Science degree in Electrical Engineering from the University of Colorado, Boulder.

“I was familiar with Oski, the quality of the company, people and service it provided, and embraced the opportunity to become a part of it,” remarks Parry. “Its extraordinarily talented team of experts has proven abilities to solve the hardest verification problems while meeting the needs of an inflexible tapeout schedule.”

More information about Oski Technology can be found at: www.oskitechnology.com

About Oski Technology

Oski Technology is a formal verification services company with expertise in deploying formal verification on complex, digital designs. Oski Technology has developed a unique Formal Sign-off Methodology and Oski Abstraction Models to solve challenging capacity problems with formal verification. Its formal methods bring a higher level of productivity than traditional simulation and formal verification approaches. Oski Technology, headquartered in Mountain View, Calif., with a design center in India, has built a team of the world’s foremost experts in formal verification. More information about Oski Technology can be found at: www.oskitechnology.com

Formal Sign-off Methodology is a trademark of Oski Technology, Inc. All trademarks and registered trademarks are the property of their respective owners.

Contact:
For more information, contact:
Nanette Collins
Public Relations for Oski Technology
(617) 437-1822

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

“The model checking solvers in the HWMCC competition continue to keep pace with industrial-strength model checkers. Oski Technology relies on advances in this technolology to deploy End-to-End formal verification methodology across the most complex designs in the industry” notes Oski Technology president and CEO, Vigyan Singhal, who congratulated this year’s winner and the runners up of the Oski Deep Bounds Award, and emphasized the outstanding calibre of the competition entries.

The Oski Deep Bounds Award was designed to recognize exceptional technological achievement for solutions that achieve deep bounds, and the model checking solvers in the competition continue to keep pace with industrial-strength model checkers.

Armin Biere is the organizer of HWMCC 2015, the competitive event for hardware model checkers, and also a professor of computer science at Jonannes Kepler University in Linz, Austria. HWMCC is a driving force to improve model checkers and encourages participants to present their work and share results with a broader audience. Entrants were invited to solve benchmarks in the AIGER format.

FMCAD is the leading conference and forum on formal methods theory and applications in hardware and system verification, where HWMCC is co-located.

Norbert-Manthey-winner_HWMCC-2015

Norbert Manthey, Winner Oski Deep Bounds Award HWMCC

 

 

 

 

 

 

Alberto Griggio

Alberto Griggio, Runner up Oski Deep Bounds Award HWMCC

 

 

 

 

 

 

Marco_Roveri, Runner up Oski Deep Bounds Award HWMCC

Marco Roveri, Runner up Oski Deep Bounds Award HWMCC

 

 

 

 

 

 

,

 

MEDIA ALERT: Oski Technology to Participate in Formal Verification Session, Industry Panel on Formal during FMCAD in Austin, Texas

Oski Technology to Participate in Formal Verification Session, Industry Panel at FMCAD 2015

Sponsors Annual Hardware Model Checking Competition Once Again

MOUNTAIN VIEW, CA–(Marketwired – Sep 22, 2015) –

WHO: Oski Technology, Inc., the only dedicated formal verification service provider

WHAT: Will participate in a Formal Verification Applications and Case Studies session, where Vigyan Singhal, Oski Technology’s president and chief executive officer, will present “The Compositional Reasoning Gotchas in Practice” during the Formal Methods in Computer-Aided Design (FMCAD) 2015. The session will be followed by a panel titled, “Formal Verification in the Industry — a 2020 vision.” Vigyan Singhal will serve as a panelist.

WHEN: Tuesday, September 29

WHERE: The University of Texas at Austin, Texas

Once again, Oski Technology will sponsor the annual Hardware Model Checking Competition (HWMCC) recognizing outstanding technological achievement for solving the most challenging formal verification problems, from end to end.

For more information about FMCAD Austin, go to: http://bit.ly/1KWvIb4
The Oski Technology website can be found at: www.oskitechnology.com

FMCAD is the premier conference on formal methods theory and applications in hardware and system verification. The complete program can be found at: http://bit.ly/1IUV7eG

About Oski Technology

Oski Technology is a formal verification services company with expertise in deploying formal verification on complex, digital designs. Oski Technology has developed a unique formal verification methodology and Oski Abstraction Models to solve challenging capacity problems with formal verification. Its formal methods bring a higher level of productivity than traditional simulation and formal verification approaches. Oski Technology, headquartered in Mountain View, Calif., with a design center in India, has built a team of the world’s foremost experts in formal verification. More information about Oski Technology can be found at: www.oskitechnology.com.

End-to-End Formal is a trademark of Oski Technology, Inc. All trademarks and registered trademarks are the property of their respective owners.

Contact:
For more information, contact:
Nanette Collins
Public Relations for Oski Technology
(617) 437-1822

Happy Birthday, Decoding Formal!

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.

While survey comments from attendees indicate that Decoding Formal meetings are enjoyable and worthwhile, the numbers provide hard evidence that these events have garnered quite a following: Attendance at Decoding Formal events has increased 4x since its inception. We regularly receive requests to bring Decoding Formal events to more cities, and attendees fly in from out of state, to attend our events. This demonstrates not only the success of our Decoding Formal events, but also the increasing and widespread interest in the adoption of formal verification, in the industry.

Our aim was to create a forum for the advanced application of formal verification, as well as offer lunchtime networking with peers, and the chance to explore the unique collection at the Computer History Museum, including the historic Babbage Engine. The Decoding Formal Club has largely achieved this objective, but not without lively (and sometimes heated) technical discussion. We are grateful to formal users who attend and share their experiences and challenges at these meetings, as well the many industry-leading formal experts who have presented valuable insights gleaned from their day-to-day practical application of formal verification:

• Vikram Khosa, “One Metric to Rule Them All: Tracking Progress on Formal Testbenches”
• Robert Kurshan, “Formal Verification of Cache Coherence”
• Jonathan Michelson, “Liveness vs. Safety – A Practical Viewpoint”
• Normando Montecillo, “Can Formal Go Mainstream? Broadcom DVT’s Formal Integration in the DV Flow”
• Syed Suhaib, “Experience with Formally Verifying the Denver CPU”
• Ross Weber, “Formal Verification and a New CPU Project at ARM”

At the upcoming meeting on October 21, we are pleased to present the following speakers:

1. Prashant Aggarwal, project lead and principal engineer at Oski, will present “How to Ensure Completeness of End-to-End Formal Testbench for Sign-off”
2. Kenny Xing, principal design engineer at Broadcom, will share “Creative Formal Techniques to Verify PCache”
3. Yogesh Mahajan, verification engineer at NVIDIA and Vigyan Singhal, Oski CEO, will discuss “Compositional Reasoning Gotchas in Practice”

In addition, we are delighted to have Vikas Chandra, Principal Engineer at ARM who will talk about Mobile Hardware Security.

Lastly, if you’ve seen the new video of our popular “Break the Testbench” Challenge at this year’s DAC, you will have seen formal in action. This is something we are regularly asked to incorporate at Decoding Formal, so for this meeting, we will be bringing the challenge to you. You will be able to examine the end-to-end formal testbench, insert functional bugs, debug counter examples to verify the failure was triggered by the bug, and prove for yourself that the bug you inserted, was in fact caught.

So please join us on October 21. There will be a large cake, and a small birthday celebration for Decoding Formal. We are happy to report that space is truly limited, so sign up today.

*The October 21 Decoding Formal Club meeting is sponsored by Synopsys. The “Break the Testbench” challenge is supported by Synopsys VC Formal.

Decoding Formal Club – Completeness of the End-to-End Formal Testbench

Oski Technology "Decoding Formal" Club Event October 2013
Decoding Formal Club Meeting – Completeness of End-to-End Formal 

Registration is now closed for this event. Please subscribe to our newsletter to receive notice of upcoming Decoding Formal meetings.

The next Decoding Formal Club lunch and meeting is on Wednesday, October 21, from 12:00 p.m. until 4:00 p.m., sponsored by Synposys.

October 2015 marks the second anniversary of the Decoding Formal Club, and as part of the celebration, we have planned a series of technical presentations to engage and delight formal enthusiasts.

Oski Principal Engineer Prashant Aggarwal will give our featured presentation titled “How to Ensure Completeness of End-to-End Formal Testbench for Sign-off”. As a live case study we are bringing back the popular 2015 DAC “Break the Testbench” Challenge*, where participants entered 73 functional bugs over the course of three days, 100% of which were caught, proving that an end-to-end formal testbench is complete. You can view our “Break the Testbench” recap video, here. If you didn’t get an opportunity to take the challenge at DAC, you can now experience it live at our Decoding Formal Club event on October 21.

In addition, Yogesh Mahajan from NVIDIA and Vigyan Singhal, CEO Oski Technology will co-present a paper titled “Compositional Reasoning Gotchas in Practice”. Kenny Xing from Broadcom will present “Creative Formal Techniques to Verify PCache”. Our guest speaker Vikas Chandra, Principal Engineer in R&D at ARM, will deliver a talk about mobile hardware security, the ARM Trusted Execution Environment and the ARM TrustZone as a specific implementation, as well as use cases and authentication.

* * * Registration is now closed for this event. * * *

12:00 PM   “Break the Testbench” Challenge* and Networking
12:30 PM    Welcome, Lunch and ARM Guest Talk
                  Mobile Hardware Security
                  Vikas Chandra, Principal Engineer, ARM
1:15 PM     How to Ensure the Completeness of End-to-End Formal for Sign-off
                  Prashant Aggarwal, Principal Engineer, Oski Technology 
2:00 PM     Coffee, “Break the Testbench” Challenge* and Networking
2:30 PM    Creative Formal Techniques to Verify PCache
                 Kenny Xing, Principal Design Engineer, Broadcom
3:00 PM    Compositional Reasoning Gotchas in Practice 
                 Yogesh Mahajan, Engineer, NVIDIA
                 Vigyan Singhal, CEO, Oski Technology
3:45 PM    Wrap-up and Prize Drawing
4:00 PM    Computer History Museum Tour (Self-Guided) 

* “Break the Testbench” Challenge supported by Synopsys VC Formal

Vikas Chandra Vikas Chandra is a Senior Principal Engineer at ARM Research in San Jose. He received his Ph.D. from Carnegie Mellon University in 2004. He serves as an AE for TCAS-I and is on the program committee for VLSI Circuits, CICC, ISLPED, ITC and IRPS. He also holds a Visiting Scholar position at Stanford University. Dr. Chandra is a recipient of ACM-SIGDA Technical Leadership Award and is a senior member of IEEE.

Prashant Aggarwal is Principal Engineer at Oski Technology where he leads End-to-End formal verification projects including network system IPs, modems, security, interconnect, and standard based IP with many leading edge semiconductor customers. He was an SoC Architect at VirtualWire Technologies, designed SRAM compilers at STMicroelectronics and holds a graduate degree in electrical engineering from IIT Delhi. He has authored four patents, and been published five times at DAC, MCAD, and CAV.

Kenny Xing has been at Broadcom for five years and is currently Principal Design Engineer. He has nine years’ experience as design or verification lead for various IP and SoC designs at Broadcom and others. He holds a doctorate in circuits and systems from Nanyang Technological University in Singapore and is an important contributor in verification areas including UVM and Mixed-signal simulation, as well as formal verification.

Yogesh Majahan is an Engineer at NVIDIA, and an invited speaker at this year’s FMCAD, where he will present the paper Compositional Reasoning Gotchas in Practice.

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, three 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.

Formal Sign-Off with Formal Coverage (JUG) 2015

Oski Technology will co-present with ARM at the Jasper User Group Conference October 7 and 8, 2015 at the Cadence San Jose Auditorium, Building 10. The title of the paper is “Formal Sign-Off with Formal Coverage”, and the authors include Vigyan Singhal (Oski Technology),  Ashutosh Prasad  (Oski Technology) and Vikram Khosa (ARM).

Formal verification can replace simulation for block-level verification. In order to achieve this in practice, we need a methodology to demonstrate the completeness of the formal testbench (constraints, checkers and achieved proof depths when proofs are bounded).

Formal coverage is a relatively new advancement that enables the quantification of the completeness of the formal testbench, and progress of the project, with a measurable metric. This presentation discusses a methodology that relies on the JasperGold Design Coverage Verification App to measure formal coverage, and demonstrates how formal coverage (FVCOV) is being used on ARM’s next-generation processor design to plan for and achieve sign-off quality verification on specific design units.

The Jasper User Group Conference is an interactive, in-depth technical conference connecting designers, verification engineers, and engineering managers to share the latest design and verification practices based on Cadence® JasperGold® formal verification technologies and methodologies.

About Oski

Oski Technology is the world’s first and only formal verification services company to successfully leverage off-the-shelf EDA tools with a unique formal verification methodology for the proper integration of formal with simulation and End-to-End Formal verification. Oski has pioneered a new approach with its proprietary Oski Abstraction Models, delivering complete End-to-End Formal verification of even the most complex SOC designs.

Visit Oski Technology at www.oskitechnology.com.

Formal Methods in Computer-Aided Design (FMCAD) 2015

FMCAD 2015 is the fifteenth in a series of conferences on the theory and applications of formal methods in hardware and system verification. FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing.

Oski Technology will again sponsor the annual Hardware Model Checking Competition (HWMCC) Deep Bound track award. This is the 8th competitive event for hardware model checkers, and recognizes outstanding technological achievement for solving the most challenging formal verification problems, from end to end. Oski has been a key sponsor for these events over the years, and proposed the addition of Deep Bound Track in 2011 to sponsor research in formal verification, in order to reach deeper proof bound.

Oski will participate in the following events:

  • Tuesday September 29, 2pm Applications and Case Studies
    • Chirag Agarwal, Paul Hylander, Yogesh Mahajan, Jonathan Michelson and Vigyan Singhal. Compositional Reasoning Gotchas in Practice
  • Tuesday September 29, 4:30pm
    • Industry Panel: Formal Verification in the Industry – a 2020 vision (Session Chair: Roope Kaivola)

Panelists:

  • David Hardin (Rockwell Collins)
  • Roope Kaivola (Intel)
  • Naren Narasimhan (Calypto)
  • Vigyan Singhal (OSKI)
  • Daryl Stewart (ARM)

About Oski

Oski Technology is the world’s first and only formal verification services company to successfully leverage off-the-shelf EDA tools with a unique formal verification methodology for the proper integration of formal with simulation and End-to-End Formal verification. Oski has pioneered a new approach with its proprietary Oski Abstraction Models, delivering complete End-to-End Formal verification of even the most complex SOC designs.

Visit Oski Technology at www.oskitechnology.com.

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 with formal in their verification flow. See the six-minute video and blog recap of the 2012 Live Oski Verification Challenge, here.

This event reflected the extremely high level of confidence we place in formal, to find corner case bugs under tight schedule constraints. End-to-End Formal is a new concept. Can it in fact catch all design bugs, and so be useful for sign-off? This year we are hosting the Oski “Break the Testbench” live challenge at DAC to prove formal can be used for sign-off, and we are inviting you to try it for yourself, and win a prize.

Here’s how the 2015 DAC challenge works. Visit the Oski “Break the Testbench” kiosk at DAC, booth #1215, and try to insert functional RTL bugs that break our End-to-End formal testbench for an 8×8 multicast design. The client can send requests to many targets (multicast), and an arbiter is used to decide which client’s request gets forwarded to the target, based on certain priority and arbitration scheme. Kick off the formal run, and see how Formal Sign-off works as your intentional bugs are caught live, with our End-to-End formal testbench. Our scoreboard will display the challenge results as they come in!

The design has 312 flops and about 1000 lines of RTL code, and is intentionally small to allow for faster tool runtime on the showroom floor, and quicker turnaround on the challenge results.  We are using VC Formal. The formal testbench contains 5 End-to-End Checkers, 11 constraints, a total of 500 lines of testbench code, written in SV and SVA.

Before you take the challenge, our engineers will show you how to use symbolic variables to write End-to-End Checkers, and how to apply the Wolper Coloring technique to catch drop, reorder or duplicate data. This technique is especially useful in formally verifying data-transport designs.

Participating in this year’s Oski “Break the Testbench” challenge at DAC is a fun way to learn about and apply End-to-End formal, plus you’ll have an opportunity to win a paid registration for the one-day Decoding Formal Training “Achieving Formal Sign-off” on Thursday June 11, valued at $199.  Oski is also hosting daily Decoding Formal lunch lectures at noon, and customer lectures at 3 PM at Oski booth #1215; pre-register for lunch lectures here, as space is limited. Please visit our 2015 “Break the Testbench” kiosk at DAC, and enjoy the fun of breaking the formal testbench!

Thanks to Synopsys for co-sponsoring the 2015 Oski “Break the Testbench” challenge at DAC. We hope to see you there.

MEDIA ALERT: Oski Technology Kicks-Off 2015 Series of Decoding Formal Club Meetings February 9

Agenda includes Presentations on Variety of Formal Verification Topics

MOUNTAIN VIEW, CA–(Marketwired – Jan 20, 2015) –

WHO: Oski Technology, Inc., the only dedicated formal verification service provider

WHAT: Kicks-off the 2015 Series of Decoding Formal Club meetings, a forum for formal verification enthusiasts, pioneers and leaders who work to promote the sharing of ideas, advancement of formal technology, and adoption of formal sign-off. This meeting is sponsored by Synopsys.

WHEN: Monday, February 9, 2015, from 11:30 a.m. until 4:15 p.m.

WHERE: Computer History Museum, Mountain View, Calif. Pre-registration is required.

The Agenda:

  • Vigyan Singhal, Oski’s chief executive officer, will address constraint management in Formal Sign-off
  • NVIDIA Principal Engineer Jon Michelson, co-author of “The Art of Verification with SystemVerilog Assertions” and “The Art of Verification with Vera,” will discuss “A Practical Viewpoint on Liveness versus Safety”
  • Ross Weber, formal verification engineer at ARM and author of the best paper award at the Jasper User Group 2014, will present formal verification on a new CPU project at ARM

And, special invited guest TED Talk Speaker Cliff Stoll of Newfield Wireless and Acme Klein Bottles will demonstrate the Klein Bottle.

Registration information for the Decoding Formal Club can be found at: http://tiny.cc/szfjsx

The Oski Technology website is located at: www.oskitechnology.com

About Oski Technology

Oski Technology is a formal verification services company with expertise in deploying formal verification on complex, digital designs. Oski Technology has developed a unique formal verification methodology and Oski Abstraction Models to solve challenging capacity problems with formal verification. Its formal methods bring a higher level of productivity than traditional simulation and formal verification approaches. Oski Technology, headquartered in Mountain View, Calif., with a design center in India, has built a team of the world’s foremost experts in formal verification. More information about Oski Technology can be found at: www.oskitechnology.com.

Formal Sign-off Methodology is a trademark of Oski Technology, Inc. All trademarks and registered trademarks are the property of their respective owners.

Contact:
For more information, contact:
Nanette Collins
Public Relations for Oski Technology
(617) 437-1822

 

Oski Tutorial at Haifa Verification Conference 2014

Vigyan Singhal from Oski Technology Technology is to present a tutorial at the Haifa Verification Conference on Monday November 17, from 4 p.m. until 5:30 p.m. at the IBM Haifa facility is located at the northwest corner of the University of Haifa campus, Haifa, Israel.

Achieving Sign-off with End-to-End Formal

This tutorial focuses on the most complex yet most rewarding usage of formal – using End-to-End formal to replace simulation and achieve Sign-off. The four Cs of the Formal Sign-off methodology, checkers, constraints, complex and coverage, will be presented. We will discuss the complexity barriers to achieving proof convergence with formal tools, and describe some techniques to overcome these barriers within a given project schedule.

The HVC 2014, now in its tenth year, is a series of conferences dedicated to advancing the state-of the art and state-of-the-practice in verification and testing, and provides a forum for researchers and practitioners from academia and industry to share their work, exchange ideas, and discuss the future directions of testing and verification for hardware, software, and complex hybrid systems.

About Oski

Oski Technology is a formal verification services company with expertise in deploying formal verification on complex, digital designs. Oski Technology has developed a unique formal verification methodology and Oski Abstraction Models to solve challenging capacity problems with formal verification. Its formal methods bring a higher level of productivity than traditional simulation and formal verification approaches. Oski Technology, headquartered in Mountain View, Calif., with a design center in India, has built a team of the world’s foremost experts in formal verification. More information about Oski Technology can be found at: www.oskitechnology.com. www.oskitechnology.com.

Decoding Formal Club Oct. 23, 2014: Formal Ph.D Talks: Methodology, Application, Real-World Experience

Oski Technology "Decoding Formal" Club Event October 2013
Decoding Formal Club Event, “Formal Ph.D Talks: Methodology, Application, Real-World Experience” 
The next Decoding Formal Club event on October 23, 2014 is sponsored by `Synopsys.

Three engineers with more than 60 years of combined industry experience with formal verification will share insights on formal sign-off methodology, cache coherence verification, as well as real-world formal experience verifying NVIDIA Denver CPU. Speakers include one of the pioneers of formal verification, Robert Kurshan, CPU and Tegra Formal Verification Team Manager NVIDIA, Syed Suhaib, and Oski CEO, Vigyan Singhal.

  • Formal sign-off is used to verify a design block using formal verification without simulation. Vigyan Singhal will present on End-to-End checkers, and explain what they are, how to write them efficiently to achieve formal sign-off.
  • Syed Suhaib will share insights on real-world formal experience verifying the recently announced NVIDIA Denver CPU.
  • Robert Kurshan will talk about formal verification of cache coherence. This is a well-known sweet spot for formal verification, however what it means and entails is widely misunderstood. His talk will cover history, and discuss actual requirements and practical options for verifying memory consistency with your favorite model checker.

11:45 AM    Arrival and Networking
12:00 PM   Welcome and Lunch
12:45 PM   Formal Sign-off with End-to-End Checkers
                  Vigyan Singhal, CEO, Oski Technology
1:30 PM     Experience with Formally Verifying the Denver CPU
                  Syed Suhaib, CPU and Tegra Formal Verification Team Manager, NVIDIA
2:10 PM    Coffee Break
2:15 PM    Formal Verification of Cache Coherence
                  Robert Kurshan, a pioneer in formal verification
3:15 PM    Wrap-up and Prize Drawing
3:30 PM    Computer History Museum Tour (Self-Guided)

Robert Kurshan was a fellow at Cadence from 2001 until his retirement this month. Before that, he was a Distinguished Member of Technical Staff at Bell Labs after receiving his Ph.D in mathematics in 1968, from the University of Washington. Bob is an author of over 80 technical publications, holds 27 patents in communications, digital filtering and verification, and is the author of the book “Computer-Aided Verification of Coordinating Processes (COSPAN)”, which was the basis of the birth of formal verification research in UC Berkeley in 1992. In 2005, Bob won the ACM Kanellakis Theory and Practice Award for his work in automata-theoretic verification. He began working in formal verification since 1983. COSPAN has been applied directly to a number of projects inside AT&T, Lucent, NCR, Intel, and Cadence. FormalCheck, a formal verification tool from Bell Labs/Cadence, which used COSPAN as the engine, won the Innovation of the Year Award from EDN in 1998. Currently, COSPAN is utilized by Cadence for commercial hardware verification in its formal products and for constraint-solving in its simulator products.

Syed Suhaib is the CPU and Tegra Formal Verification Team Manager at NVIDIA. He drives the formal verification effort across various projects for next-generation designs, starting from test plan development, to application of various formal verification technologies. He is also involved with development of efficient methodologies and frameworks that are most effective for verification. Syed has a Ph.D in formal methods and modeling of communication protocols for intellectual property composition from Virginia Tech.

Vigyan Singhal is responsible for overall leadership of Oski Technology. He has worked in the semiconductor and EDA industries for more than 20 years, having founded two venture-funded start-ups – Jasper (acquired by Cadence) and Elastix (acquired by eSilicon). Vigyan started his career as a Research Scientist at Cadence Berkeley Labs. He has authored more than 70 publications, of which 3 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.

MEDIA ALERT: Oski Technology to Exhibit at Synopsys User Group Austin Designer Community Expo

MOUNTAIN VIEW, CA–(Marketwired – September 16, 2014) –

WHO: Oski Technology, Inc., the only dedicated formal verification service provider
WHAT: Will exhibit at SNUG® (Synopsys Users Group) Austin Designer Community Expo in the IC Verification community, open to all registered SNUG attendees. It will present the Oski Formal Sign-off Methodology using the Synopsys VC Formal product. Oski will highlight the benefits of creating a formal test plan and applying custom Abstraction Models during formal analysis to reach deeper search depth and achieve faster proof.

A tutorial, “From Formal Apps to End-to-End Formal Verification — Formal Analysis for Everyone,” will be presented by Vigyan Singhal, Oski’s president and chief executive officer, and Anders Nordstrom, senior corporate applications engineer, Verification Group at Synopsys. Held from 1:30 p.m. until 3 p.m., the tutorial will explain how verification engineers can implement Formal SoC Connectivity Checking and End-to-End Formal verification through examples and components of the sign-off methodology.

WHEN: Tuesday, September 23, from 5 p.m. until 7 p.m.
WHERE: Hyatt Regency Austin in Austin, Texas

For more information about Oski Technology, visit: www.oskitechnology.com.

About SNUG Designer Community Expo

The SNUG Designer Community Expo (DCE) is a unique networking event featuring Synopsys and its ecosystem partners from across the electronics industry. At SNUG DCE, Synopsys users can interact with exhibitors and see the latest design enablement solutions spanning seven designer communities: Compute and Design Infrastructure, Custom Design and AMS Verification, FPGA, IC Design, IC Verification, IP, and Prototyping & System Design.

About Oski Technology
Oski Technology is a formal verification services company with expertise in deploying formal verification on complex, digital designs. Oski Technology has developed a unique formal verification methodology and Oski Abstraction Models to solve challenging capacity problems with formal verification. Its formal methods bring a higher level of productivity than traditional simulation and formal verification approaches. Oski Technology, headquartered in Mountain View, Calif., with a design center in India, has built a team of the world’s foremost experts in formal verification. More information about Oski Technology can be found at: www.oskitechnology.com.

Formal Sign-off Methodology is a trademark of Oski Technology, Inc. All trademarks and registered trademarks are the property of their respective owners.

Contact:

For more information, contact:
Nanette Collins
Public Relations for Oski Technology
(617) 437-1822

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 using key metrics (the how much question); and planning the specific formal verification tasks on the chosen designs (the what question).

A good planning session can take several weeks to analyze the design, understand formal complexity hotspots, estimate the effort and craft a workable blueprint for formal verification. However we often see engineers jumping into the act of formal verification without spending enough time in formal test planning. Without proper formal test planning, it is not possible to achieve formal sign-off.

Win a Formal Test Planning Session with Oski Technology

What: Win a one-week formal test planning session with Oski Technology

Why: The goal of this offer is to promote the practice of proper formal test planning as well as demonstrate the proper way to do so.

How to Enter:
Oski Technology will present an achievable plan on how the chosen design should be verified with formal, to achieve formal sign-off. Interested companies should select one or more designer-size blocks to be formally verified. You will need to complete a short 5-question questionnaire about the design characteristics so we can assess the applicability of formal for this design.

Contact: Send email to marketing@oskitech.com

Results at DAC Insight: Formal Test Planning Tutorial June 5
The winning company will be announced on June 5 at DAC, during Oski Technology’s DAC Insight Tutorial Session on Formal Test Planning from 2:00pm – 4:00pm; this session is free to all DAC registrants.

Terms:
• Exact time of service will be determined based on mutually agreed-upon dates.
• The deliverable will be supplied on an as-is basis.
• Winner must schedule the formal test planning session within one year of winning, by June 5, 2015.

Oski Technology to Highlight the Oski Formal Sign-Off™ Methodology at DVCon, Outlining Benefits of Applying Custom Abstraction Models During Formal Analysis

AT DECODING FORMAL CLUB MEETING, MOUNTAIN VIEW, CALIF. THURSDAY, JANUARY 23

MEDIA ALERT: Oski Technology to Host Decoding Formal Club for Formal Verification Enthusiasts
Abstraction Models to be Discussed

MOUNTAIN VIEW, CALIF. –– January 13, 2013 –– (reminder June 20)
WHO: Oski Technology, Inc., the only dedicated formal verification service provider
WHAT: Will highlight the Oski Formal Sign-off Methodology during DVCon 2014 in Booth #305, outlining the benefits of applying custom Abstraction Models during formal analysis to reach deeper search depth and achieve faster proof. Oski representatives will be available to discuss the way in which the Oski Formal Methodology makes formal sign-off possible with end-to-end checkers and formal coverage.
WHEN: Monday, March 3, from 5 p.m. until 7 p.m., Tuesday and Wednesday, March 4-5, from 2:30 p.m. until 6 p.m.
WHERE: DoubleTree Hotel in San Jose, Calif.

Vigyan Singhal, chief executive officer of Oski Technology, will present “Sign-off With Bounded Formal Verification Proofs” during Session 2, “Formal and Semi-Formal Techniques,” Tuesday March 4, from 9 a.m. until 10:30 a.m. in the Fir Ballroom.

Additionally, Singhal will participate in a tutorial organized by Mentor Graphics titled, “Formal Verification in Practice: Technology, Methods and Applications.” It will be held Thursday, March 6, from 2 p.m. until 5:30 p.m. in the Siskiyou Ballroom.

More information about Oski Technology can be found at: www.oskitechnology.com

To learn more about DVCon, visit: http://www.dvcon.org

About Oski Technology

Oski Technology is a formal verification services company with expertise in deploying formal verification on complex, digital designs. Oski Technology has developed a unique formal verification methodology and Oski Abstraction Models to solve challenging capacity problems with formal verification. Its formal methods bring a higher level of productivity than traditional simulation and formal verification approaches. Oski Technology, headquartered in Mountain View, Calif., with a design center in India, has built a team of the world’s foremost experts in formal verification. More information about Oski Technology can be found at: www.oskitechnology.com.
###

Formal Sign-off Methodology is a trademark of Oski Technology, Inc. All trademarks and registered trademarks are the property of their respective owners.

For more information, contact:
Nanette Collins
Public Relations for Oski Technology
(617) 437-1822
nanette@nvc.com

Oski Technology at DAC 2014

Oski Technology will be exhibiting at booth #2301, DAC 2014 June 2 – 6, 2014, San Francisco, CA

Time: DAC exhibits are open June 2 – 4, 2014
Venue: Oski Booth #2301, Moscone Convention Center, San Francisco California.
Web: http://www.dac.com

Oski will also be participating in the following events at DAC:

Monday June 02, 1:30pm – 3:00pm | Room 101
Track: IP Topic Area:Verification
Modeling Xs in Behavioral Models for Hard IPs
Speaker: Prashant Aggarwal – Oski Technology, Inc., Mountain View, CA
Authors: Prashant Aggarwal – Oski Technology, Inc., Mountain View, CA
George Curkowicz – Cypress Semiconductor Corp., San Jose, CA
Mark Glasser – NVIDIA Corp., Santa Clara, CA
Vigyan Singhal – Oski Technology, Inc., Mountain View, CA


Monday June 02, 1:30pm – 2:15pm | Booth 313
Track: EDA Topic Area: Business
Pavilion Panel: China Fabless: Threat or Opportunity?
Moderator: Junko Yoshida – EE Times, Madison, WI
Organizer: Thomas Wong – Cadence Design Systems, Inc., San Jose, CA

Panelists:
Limin He – Cadence Design Systems, Inc., San Jose, CA
Jin Zhang – Oski Technology, Inc., Shanghai, China
ShaoJun Wei – Tsinghua Univ., Beijing, China

The 2013 smart phone market was close to 1 billion units. Chinese brands accounted for 50% of the total. 70% of Chinese phones used apps processors and SoCs designed in China or Taiwan. Has the center of gravity of SoC innovation shifted to China? Where is funding available for fabless chip start-ups? Come and find the answers for yourself! Are you ready to pack your bags and head to China or can you still launch your business from Silicon Valley?


Tuesday June 03, 4:00pm – 6:00pm | Room 105
Track: EDA Topic Area: Designer\IP Track
Session 38
Designer Track: Accelerating Productivity Through Formal and Static Methods
Chair: Vigyan Singhal – Oski Technology, Inc., Mountain View, CA

Formal and static methods, which analyze a design directly rather than depending on large numbers of simulation vectors, are becoming increasingly important in the world of modern design. In the first part of this session, real-world practitioners who have been successful with formal verification describe case studies and use them to supply useful advice for those who wish to achieve similar results. Then we move on to describe some new and powerful uses for static and formal techniques in conjunction with other tools and methods, providing new insights into IP integration, clock domain crossings, power issues, and clock/reset design.


Wednesday June 4, 2014, 11am | Mentor Verification Academy
Introduction to Formal Sign-off Methodology
Speaker: Vigyan Singhal, CEO, Oski Technology

Formal sign-off is a new concept in the industry. Like simulation sign-off, formal sign-off requires a thorough and systematic methodology, which includes End-to-End checkers to verify complete functionality, constraints, Abstraction Models to overcome complexity and coverage to measure results. This talk discusses each component of the formal sign-off methodology so formal can be applied in the verification sign-off flow to maximize efficiency & productivity.

Thursday June 05, 2:00pm – 4:00pm | Room 256
Track: EDA Topic Area: Verification
DAC INSIGHT: Starting Formal Right from Formal Test Planning
Organizer: Jin Zhang – Oski Technology, Inc., Mountain View, CA

Verification planning is key to the success of any verification tasks and this is especially true for formal verification. Formal technology, while it can be very powerful in proving complete functional correctness of designs, is not suited for all design types.

This session discusses the 3 stages of Formal Test Planning – IDENTIFYING the right design blocks for formal verification; ESTIMATING the formal verification effort using key metrics; and PLANNING the actual formal verification tasks on the chosen designs. Through case studies and interactive discussions, audience will walk away knowing how to start formal verification right from Formal Test Planning.

Speakers: Vigyan Singhal – Oski Technology, Inc., Mountain View, CA
Prashant Aggarwal – Oski Technology, Inc., Mountain View, CA
Jin Zhang – Oski Technology, Inc., Mountain View, CA

Oski Technology is the world’s only dedicated formal verification service provider. Oski’s Formal Sign-off Methodology™ uses end-to-end checkers, constraints, Oski Abstraction Models™ and formal coverage metrics to catch corner case bugs, replace simulation for the blocks verified, and improve overall verification efficiency. Oski has provided formal verification services to many leading semiconductor companies including Cisco, Cypress, NVIDIA, Rambus and Xilinx to tape out critical projects, establish formal sign-off methodology and develop customer formal expertise. Oski is a formal sign-off company.

DAC is the largest semiconductor conference in the industry.

Visit Oski Technology at www.oskitechnology.com.

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 are the days when formal can only be used to compliment simulation on a given block. Oski Formal Sign-off Methodology and formal verification can replace block-level simulation for suitable designs to improve overall verification coverage, efficiency and productivity. The logic is simple – control and data transport types of blocks and designs with complex corner scenarios are better suited to be verified with formal than simulation. We have applied such methodology to tapeout many of our customers’ mission-critical projects and at the same time develop formal expertise in our customer base.

2013 saw Oski’s customer base expanding to Japan, China, Korea and Taiwan, as companies in Asia are retooling their verification methodology and adding formal technology to the mix for verification sign-off. Oski has quietly added distribution channels in the region and increased its engineering staff by 20% consecutively, for the past 2 years, to support its growth in Asia.

To help customers learn about formal technology – its applications and benefits, besides attending various trade shows in different regions to promote formal verification (DVCon and DAC in the U.S., Verify and EDSFair in Japan, CDNLive and ARMTechCon in China), Oski has also increased its marketing effort in the following areas:
• Completed a redesign of the Oski Technology Web site, adding new content and structure so it is easier for customers to find relevant information
• Produced the “Decoding Formal” series of video tutorials on formal verification , covering a broad array of topics and interest for verification engineers and managers, available on the Oski website
• Sponsored the Deep Bounds Award at the FMCAD-affiliated annual Hardware Model Checking Competition (HWMCC)
• Launched the Decoding Formal Club forum to foster knowledge sharing and networking among formal enthusiasts so as to build critical mass of formal experts in the industry. This event was featured in several articles including John Cooley’s DeepChip. The next Decoding Formal event is scheduled for January 2014, and we hope you can join us! Please register Please register here.

In 2014, we hope to maintain the momentum we have built this year and move our customers up the formal adoption pyramid from automatic formal and the use of formal apps to assertion-based verification (ABV) and ultimately to End-to-End Formal for Formal Sign-off.

Thank you to all our customers for being a part of our success in 2013! We look forward to another banner year, and wish you all a happy holiday and all the best for 2014.

Happy Holidays From Oski Technology

Happy Holidays From Oski Technology

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 in the industry:

1. Our formal verification service offering includes training for customers on End-to-End formal verification and Oski Formal Sign-off Methodology so they can leverage formal effectively and across all design projects.

2. We produced the “Decoding Formal” series of video tutorials on formal verification covering a broad array of topics and interests, and made the series available on the Oski website.

3. We recently launched the Decoding Formal Club, a forum to foster knowledge-sharing and networking among formal enthusiasts so as to build critical mass of formal experts in the industry.

4. The Oski 72-hour Live Verification Challenge hosted at DAC 2012 was an impressive demonstration of the power of End-to-End formal verification over a very short period.

5. Finally, Oski is the sponsor of the Deep Bounds Award at the annual Hardware Model Checking Competition (HWMCC) affiliated with FMCAD (Formal Methods in Computer Aided Design). This award recognizes outstanding technological achievement for solving the most useful End-to-End formal verification problems.

FMCAD 2013 Oski Deep Bounds Award Presentation

Oski Deep Bounds Award winner Niklas Sörensson and Vigyan Singhal, Oski Technology

FMCAD 2013

FMCAD 2013

FMCAD 2013 Panel Discussion: “Teaching Formal Methods: Needs, Challenges, Experiences and Opportunities”

FMCAD 2013 Panel Discussion: “Teaching Formal Methods: Needs, Challenges, Experiences and Opportunities”

FMCAD 2013 held in Portland, OR was well attended this year, and Oski was invited to participate in a panel discussion with participants from industry and academia. The goal of the panel discussion – “Teaching Formal Methods: Needs, Challenges, Experiences and Opportunities” – was to share experiences and insights about the most effective ways to teach formal methods and improve formal education so as to enhance the adoption of formal in the industry.

During the FMCAD panel discussion Oski shared the following perspectives and insights. Some that apply to educating engineers on how to leverage formal can also be applied to building successful formal teams and developing formal expertise.

1. Better one full-time user of formal than several part-time users – When companies begin to deploy formal verification for the first time, they sometimes start with a few people doing part-time formal verification work. In our experience, one full-time dedicated formal engineer delivers much more than two or three part-time formal engineers. Compared to simulation, formal is an orthogonal technology, and the user really needs to be immersed in it to gain the necessary expertise.

2. Success is about more than bugs – Most companies deploy formal in “bug-hunting” mode and measure the success of formal by tracking the bugs it finds. In contrast, Oski is teaching customers to deploy formal for sign-off, i.e. for the blocks verified with formal, no simulation testbench needs to be developed; formal verification guarantees complete functional correctness of the design through end-to-end checkers. The Formal Sign-off approach truly leverages the power of formal in the verification flow. While bug hunting is valuable, it doesn’t help to develop a “sign-off-worthy” formal methodology. Once customers see success in using the Formal Sign-off Methodology, they tend to want to deploy formal on more projects. We have to aim high to be successful and Formal Sign-off Methodology should be a must-have in the verification flow, so formal engineers are held responsible for design quality and also receive well-deserved credit for it.

3. Relate formal to simulation plans – If formal verification is mostly used as a bug-hunting solution, the synergy it has with simulation is rarely leveraged. The downside is the application of formal becomes an isolated event and it doesn’t lead to the most successful usage of formal. In fact, formal and simulation are complementary; both are needed and they also support one another in application. A complete verification methodology needs to leverage both technologies to where is most appropriate for each, and to each its fullest potential.

4. Learn how to overcome the complexity barrier – We all know formal verification is hard and people often run into the complexity barrier with state space explosion problem. While formal technology is improving every year, fighting exponential run-times is usually futile. When formal tools fail to give conclusive results within a few hours, running the tools overnight (or over the weekend) usually does not help. When they run into such inconclusive results, formal users are discouraged and often give up, hindering formal adoption. In reality, much can be done to overcome the complexity barrier. Users need to quantify the benefits of bounded proofs, and apply the appropriate techniques when proof bounds are not good enough.

5. Focus on solving the right problem – We all prefer easy-to-use or automated solutions. However to make the best use of formal technology, manual work is necessary. We need to change the problem by decomposing the proofs and building Abstraction Models. With such techniques, proofs can often run millions of times faster, and formal can be used for sign-off. In our experience with hiring our own team members, having past verification experience (with formal or not) is not critical. What is critical is a willingness to use analytical skills to find creative solutions. We hire people who are good problem-solvers rather than people who prefer tools that are completely automated.

In summary, Oski’s formula for educating engineers on how to leverage formal, building successful formal teams and developing formal expertise: Hire problem-solvers to be dedicated, full-time users of formal who can relate formal to simulation plans, explore bounded proofs, and use formal to its fullest potential by deploying formal for sign-off.

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 verification can become part of the verification sign-off flow.

Oski Technology's new engineering office in India is within walking distance to the Metro Rail Network and just 15 minutes away from the international airport, making it easily accessible for customers who wish to attend meetings and formal verification training events.

Oski’s new office is easily accessible for customer meetings and formal verification training.

For the past eight years since it’s inception in 2005, Oski has been highly successful in promoting the adoption of formal verification and in helping to develop formal expertise in large semiconductor companies in North America. With recent advancements of technology in Asia, leading semiconductor companies in this part of the world are starting to add formal technology to their overall verification strategy so as to improve verification efficiency and boost productivity. As demand for formal services has grown in Asia, Oski has quietly expanded its sales channels in Japan, China and Korea, and increased its engineering staff by 20% consecutively for the last 2 years.

To facilitate growth, Oski’s main engineering office relocated this year to the heart of India’s “Millennium City”, Gurgaon. The office is within walking distance of the Metro Rail Network and 15 minutes away from the international airport, making it easily accessible for customers who wish to attend meetings and formal verification training events. Visitors to the new office find a bright, well-lit interior with large, open common spaces accented by Oski’s signature-blue dash, and Oski employees enjoy the new work environment and convenient location. This space reflects Oski’s core company values – openness, zero hierarchy and an understated commitment to excellence.

Oski Technology's new office space in Gurgaon, India was designed to include two highly secure chambers for use by customers; each chamber has its own isolated networks, monitored daily through CCTV cameras, with access controlled directly by the customer using that space.

Oski’s new space was designed to include two highly secure chambers for customer use, each with its own isolated networks, CCTV cameras, with customer-controlled access.

Oski has always paid special attention to meeting and exceeding customers’ strict design access requirements, and the new office space has made a significant investment to ensure customer data are protected. The space was designed to include two highly secure chambers, each with their own isolated networks, and CCTV cameras, and customer-controlled access. Each secure chamber has seating for five, large enough to accommodate customer staff and Oski engineers. During the course of a project, each secure chamber effectively becomes the customer’s remote facility, fully monitored, controlled, and highly secure.

The new facility can accommodate growth for the next six years. But with ongoing success, Oski may find it has once again outpaced its newly expanded capacity. For now, both Oski – and our customers – have a secure space in New Delhi that they can truly call their own.

Visitors to the new Oski Technology office find a bright interior with large, open common spaces, reflecting Oski’s core company values - openness, zero hierarchy and a commitment to excellence.

Visitors to the new Oski office find a bright interior with large, open common spaces, reflecting core company values – openness, zero hierarchy and a commitment to excellence.

Oski Decoding Formal Club October 10, 2013: Bounded Proofs

Oski "Decoding Formal" Club
Oski “Decoding Formal” Club

Oski “Decoding Formal” Club invitation-only event at the Computer History Museum, Mountain View, October 2013.

For more information on the Oski Decoding Formal Club, please visit www.oskitechnology.com/decodingformal

Decoding Formal Club event, Computer History Museum

Decoding Formal Club event, Computer History Museum

Oski Technology: Bullish on Formal Verification

Oski Technology may be named for the famous University of California at Berkeley’s bear mascot, but Oski is not bearish at all on the formal verification market. In fact, it’s downright bullish on this form of verification and its importance to chip design.

One recent morning, Vigyan Singhal, Oski’s president and CEO, was in the Mountain View, Calif., corporate headquarters ready to discuss his life in formal verification and what inspires him and the company he founded.

Vigyan Singhal is Oski Technology’s founder, president and CEO

Vigyan Singhal is Oski Technology’s founder, president and CEO

Vigyan and Oski Technology may seem synonymous to anyone familiar with the company, though he demurs at that portrayal and points to the formal verification services company’s 25 employees in the U.S., India and China. Yes, he started the consulting business in 2005, but that’s only a small part of the story.

Let’s start, then, with Vigyan’s story and move it forward. Vigyan’s from Northern India and studied at the Indian Institute of Technology (IIT, as it’s known) Kanpur, the prestigious and hard-to-get-into college in India. After completing his Bachelor of Science degree in computer science and engineering at IIT Kanpur, he was accepted at Cal and started working toward a Master of Science degree and Ph.D. in database systems. He was not making much progress even after three years and was discouraged. After repeated cajoling from a friend, he finally agreed to take a course with Dr. Robert Brayton, the Cadence Distinguished Professor of Electrical Engineering and Computer Science and a Phil Kaufman Award recipient.

Soon after, he switched majors and was part of Professor Brayton’s group. Right after inducting Vigyan in his group, Professor Brayton got him an internship working at Motorola in Austin, Texas. His supervisor was Carl Pixley, now of Synopsys, who asked him to do research on formal verification techniques, which later would evolve into his thesis topic. Carl also asked him to verify the cache controller in a PowerPC chip, where Vigyan found his first post-silicon bug using formal verification.

When his doctoral studies were wrapping up, he was assigned a dream-team thesis committee if there ever was one. Along with Professor Brayton, he presented to Dr. Alberto Sangiovanni-Vincentelli and the late Dr. Richard Newton. A funny thing happened during his qualifying examination presentation for his thesis topic. Professor Newton stopped him and said that the formal verification methodology he was outlining wouldn’t work. Professor Sangiovanni-Vincentelli jumped in, arguing Vigyan’s points. Vigyan and Professor Brayton went back to Brayton office to talk it through. He went on to get his Ph.D., with a thesis in the methodology he proposed.

With the newly minted degree, Vigyan joined Cadence Berkeley Labs and began developing what would become Cadence’s formal verification entry HECK, an equivalence checking tool. Vigyan stayed around for about 18 months after his project was commercialized, then partnered with another Cadence engineer, Joe Higgins, originally from the analog/mixed-signal group, to launch a verification company. They called their fledgling startup Tempus Fugit, Latin for “time flies.” Vigyan and Joe looked at areas within the formal verification discipline, bootstrapping themselves with consulting services projects. Their customers’ designs became their inspiration.

“I was inspired by the designs I saw at Apple,” says Vigyan. He and Joe began developing model checking software to verify the correctness of standard interfaces, such as PCI, USB or FireWire. Even though there were nine other commercial tools in formal verification market from 0-In, Averant, Axiom, Cadence, Chrysalis, Real Intent, Synopsys, Verplex and Verysys at that time, Vigyan and Joe believed they could build a differentiated company. Within three months from the start of product development, they had their verification engines and attracted early customers Ikanos and NVIDIA.

Vigyan persuaded both with the convincing offer: “Let me use my tool on your design and pay me if I find bugs.” He succeeded at both companies by finding important bugs.

Rahual Joshi, Oski Technology’s managing director of India Operations

Rahual Joshi, Oski Technology’s managing director of India Operations

For those EDACafe readers who don’t recognize the name Tempus Fugit, it’s been renamed as Jasper Design Automation, a well-respected verification provider, since 2003. About two years later, and after an influx of capital and the appointment of Kathryn Kranen to the role of CEO, Vigyan left to form Oski Technology.

Here’s where the discussion turns fully to Oski Technology, a company that’s been growing steadily since 2005. To support the growth of formal adoption in semiconductor companies, Oski quietly acquired a company in New Delhi, India, comprised of talented and clever engineers, almost all of whom are IIT graduates, led by Rahul Joshi.

“They brought with them new ideas and concepts,” remarks Vigyan, who’s building a core group of engineers to offer formal verification services, along with training programs to teach chip verification engineers how to build test cases.

Additionally, Jin Zhang has been hired to serve as general manager for Asia Pacific to support demand for formal verification services and manage the distribution channel in this region. Jin holds a Ph.D. in formal verification and a MBA in international management, and has held technical and management positions with increasing responsibilities at EVE, Real Intent, Cadence Design Systems and Lattice Semiconductor.

Jin ZJin Zhan, Oski Technology general manager of Asia Pacific and senior director of marketing.

Jin Zhang, general manager of Asia Pacific and senior director of marketing.

Today, Oski is focusing on the tip of the pyramid of all formal applications –– or what it refers to as End-to-End Formal. The goal is formidable because it means catching bugs early, increasing verification efficiency, replacing block-level simulation and enabling formal verification sign-off. A heady goal, to be sure, but one Oski’s managing with aplomb.

When the Oski team of formal verification experts is deployed on a chip design, it uses an internal Formal Sign-off Methodology to find the most elusive bugs. That methodology includes end-to-end checkers, Abstraction Models and formal coverage. Oski’s verification engineers have developed formal verification IP that’s licensed and sold to their customers, but Vigyan makes it clear that Oski is a formal verification services company and not a tools supplier.

Formal adoption pyramid for End-to-End formal

Oski is bullish on expanding the understanding of the pyramid so verification engineers can implement End-to-End formal technologies and methodologies to accomplish their verification goals.

A rule of thumb from the early days of Tempest Fugit is employed again today, Vigyan notes with pride: “Formal is unpredictable and we’re paid only if it works.” He quickly adds: “We know so much about formal verification and how to make it tractable.”

Formal Verification includes a range of technologies, he remarks as he points to a pyramid on his computer screen (see above). Oski is bullish on expanding the understanding of the pyramid so verification engineers can implement End-to-End formal technologies and methodologies to accomplish their verification goals to the point that they can sign-off on certain blocks using formal alone. Currently, the awareness and understanding is at the bottom of the pyramid and Oski’s often called into a chip design and verification project to solve the hardest problem at the tip of the pyramid.

Expanding the pyramid is more easily typed than done. “We have few teachers, so few people know how formal verification works,” remarks Vigyan, shaking his head sadly. “It’s not taught at universities and tool providers are supplying apps that automate tools.”

This unfortunate state was another inspiration for Vigyan and Oski Technology, which unveiled the Oski Deep Formal Award last year at the Formal Methods in Computer-Aided Design (FMCAD) Conference. In doing so, Oski became the first industrial sponsor of the annual Hardware Model Checking Competition (HWMCC).

The award, to be given again this year during FMCAD in Portland, Ore., in October, is designed to encourage research for developing tools and making formal verification more practical. “Our hope is that cool ideas will make its way into tools,” he says. The second reason is to help advances in bounded model checking. Currently, model checking results often appear inconclusive. For the experts at Oski Technology, unbounded proofs are useful and rather reliable, but it is not a well-understood concept.

On a lighter note, Oski Technology is more than committed to formal verification. It lives it. It’s hard to forget Oski’s show-stealing feat at DAC 2012 in San Francisco with its 72-hour verification challenge. An engineer, Chirag Agarwal, was holed up in a conference room close to the Moscone Center and tasked with debugging an NVIDIA design with Oski’s Formal Sign-Off Methodology in 72 hours, on a design he had never seen before. Nor had anyone else at Oski.

Oski Live Verification Challenge DAC 2012

Oski Live Verification Challenge DAC 2012

A CCTV was installed in the conference room and the video was streamed live in the Oski booth. Talk about a nail biter! Even Vigyan will admit that there were a few tense moments on the first day of DAC, but then they knew they had pulled it off. The NVIDIA team received detailed verification results delivered at 5 p.m. Wednesday as DAC was closing, including the end-to-end formal testbench, and three formerly undetected corner-case bugs.

This year’s DAC was a bit more subdued, but no less creative and bullish on formal verification. Oski offered a verification test challenge each day. Attendees who walked up to the booth were given a problem to solve and awarded great prizes for the correct answer.

Winners of Oski’s "Decoding Formal" Challenge Competition this year received a beer stein.

Winners of Oski’s “Decoding Formal” Challenge Competition this year received a beer stein.

If that’s not all, the wildly inventive Oski Technology team is at it again. It formed the Oski “Decoding Formal” Club to foster formal idea sharing among formal verification enthusiasts and proselytize formal verification. The first invitation-only meeting will be held at the Computer Museum in Mountain View in October 10.

As the discussion with Vigyan comes to a close, it’s clear that while the Oski Technology mascot may be a bear and its founder inspired by Cal, Oski Technology is quite bullish on formal verification.

(Editor’s Note: Nanette Collins manages Oski Technologies’ Public Relations activities.)

Calling All Formal Enthusiasts: Join the Oski “Decoding Formal” Club

In our years of providing formal verification services to leading-edge semiconductor companies, I have had the pleasure of meeting and working with many smart and dedicated engineers who paved the way of formal adoption in their companies – studiously applying formal technology to verify more complex designs as well as building up formal methodology so formal can become part of sign-off criteria in their verification flow. I have had countless discussions with these individuals on the nature of formal technology, best practices in formal application, and ways of getting the most out of formal tools in verification. These are valuable mutual learning experiences for all of us.

In working with these formal technologists and practitioners, I have always wanted to create a forum for these kindred spirits – formal enthusiasts, pioneers, leaders and friends who work in different companies but on the same mission. The goal is to promote idea sharing among us so together we can further advance formal technology and broaden formal adoption in the industry.

Now that time has come, and Oski Technology is pleased to announce the launch of the Oski “Decoding Formal” Club, a quarterly gathering for formal enthusiasts to meet, mingle and have fun while decoding the secrets of formal technology and its application.

These events will be organized as luncheons for a small group of formal enthusiasts. We will feature interesting technical presentations and discussions, good food and above all, formal fun!

The first luncheon will be held in Mountain View, October 10 at the Computer History Museum. We will discuss best practices in the application of formal, so everyone can leverage the best of industry know-how in their own application. We at Oski will share our own insights, and are excited to hear about the tips and tricks you have learned over the years.

If you would like to participate and we have not already contacted you, please contact us at decodingformal at oskitech dot com. In your email, please introduce yourself and your experience with the application of formal verification, and what you would like to see discussed at future events. There will only be space for 12 people in our “Decoding Formal” Club launch event, so don’t wait to contact us!

I am very excited about hosting these events and I look forward to seeing YOU there!

Vigyan Singhal, Oski Technology

IP Customers Beware! “Silicon Proven” IP May Not Be Fully Verified

The verification of all configurations (reaching in millions) of an (silicon) IP is a challenge. I have experienced this problem first-hand both from the vendor side as an embedded SRAM (eSRAM) compiler designer, and from the customer side, as an architect of a wireless SoC using 3rd party IPs.

When I was eSRAM compiler designer, eSRAM used to support hundreds of thousands of configurations based on address widths, data widths, data masking, low power features, etc. In order to meet performance for different configurations, I sometimes designed different internal architectures of eSRAMs for different configurations. Due to the large number of configurations, verification is performed only on the configurations where the designer identifies the greatest need, for example when there is an architecture change either in the design or layout. Though this approach may appear to be comprehensive, I have seen silicon failures because the configurations picked for silicon had not been verified. The failures were due either to design modeling error or layout programming error. These failures could have been caught at the verification stage, if all configurations of eSRAMs were verified. However using simulation as the sole verification technology, verifying all configurations was simply not possible.

When I started building a wireless SoC (for transferring video real time), my team developed baseband (BB) and medium access control (MAC). For the rest of IPs, we decided to source from external 3rd party IP vendors, thinking that it would save us time and money since the IPs would be mature, in another word, completely verified. I needed some specific cuts of eSRAMS and a specific configuration of flash memory controller for my SoC and contacted 3rd party IP and library vendors for the same. When I asked the vendors about the maturity level of their IPs, they ensured me that their IPs are “Silicon Proven” and hence I should not worry. My experience as eSRAM designer have taught me that “Silicon Proven” configurable IPs may not mean that my specific eSRAM cuts and flash controller configuration were verified on silicon. So, I inquired if our particular requirements were proven on silicon. Not surprisingly the answer was negative. When I asked the IP vendor if we could get the testbench of the flash memory controller so we could verify our specific configuration, he pointed me to a verification IP (VIP) company. We were paying for an IP that was not fully verified. Moreover we had to pay for a VIP to verify that unverified IP (what a shame!).

I wondered if this this challenge was faced by every designer using 3rd party IP, and if there might be a better solution. Enter Oski Technology.

These days I work with Oski Technology where I deploy formal verification for verifying complex blocks of SoC and vendor IPs, and I no longer worry about missing corner case bugs. Formal tools explore all possible (legal with constraints) inputs for the design under test (DUT) and are hence able to find all corner case bugs. Moreover, by using end-to-end checkers, we verify the end-to-end functionality of the design. This means that even if the internal design architecture is changed, there is no need to change my verification setup for verifying DUT (awesome!).

Recently, Oski formally verified all possible configuration of a configurable IP (over 1 million combinations) using just one (yes, just one) formal testbench. The testbench is written in way that IP customers can use the formal testbench as VIP to verify the specific configuration in use so they can be fully confident that the IP will not fail in silicon.

The benefits of formal verification for IP vendors and their customers are summarized below:

1. For IP vendors, “Formally Certified” IP is better than so called “Silicon Proven” IP, as all configurations are verified formally (no corner case bugs!). This can be an competitive edge for the IP vendors
2. By using end-to-end checkers in formal verification, there is no need to change the testbench even if internal design architecture is changed, saving time and effort
3. For IP customers, the formal testbench (formal VIP) can be used to further ensure the specific configurations in use do not cause any integration issues with the rest of the SoC.

Given these benefits, why aren’t all IP vendors using formal technology to verify their IPs? We will discuss this question and Oski’s approach in future blog posts, so stay tuned!

Congratulations to Oski’s Online Competition Winners!

To complement the “Decoding Formal” Contests hosted live at DAC 2013 in Austin TX, Oski Technology launched a parallel online “Decoding Formal” Contest so engineers who were not attending DAC could also participate. The online competition concluded on June 21st with many participants from Europe, Asia and US. The 3 winners were chosen based on their answers on all the questions. Congratulations to Oski Online “Decoding Formal” Winners:

Amit Rustagi from Broadcom
Charu Aggarwal from Apple
Junhyuk Park from Samsung

There were 10 questions covering formal technology and its application. Most questions were multiple choice except for the last which was an essay question – “ Do you think formal technology is a must have technology in the verification flow? Why or why not?” Most participants answered yes, echoing what we have seen in our projects with our customers, that formal technology has become an integral component and in some cases one of the sign-off criteria in the verification flow.

There were many reasons for this. Answers submitted by contestants included the following –

“Yes. It complements simulation based DV flow. There are a lot of freebies you get just for running the design through a formal tool. Localized properties make debugging easier. Properties can be ported from unit level all the way to top level DV”

“Yes, because many functional bugs in designs with large state space may not be caught by simulation over large number of runs. Formal Verification needs to be run on such designs before sign-off of the design.”

“Formal Verification removes end to end bugs in a design which is not plausible using simulations. It can catch bugs in very early stages of the design. For the correct type of design it will save both time and resources and would give a better result as compared to simulations. So, a MUST-HAVE technology in the verification flow”

“Yes, I think formal verification is a must have technology in the verification flow. The prime reason is that formal proves to be really quick in hunting bugs on some specific designs, for example data transport designs, if applied with suitable abstraction methods”

“Formal verification is a must-have technology. Because we can verify design exhaustively with formal”

The competition results showed most participants have a good understanding of what formal technology is, its application and benefits.

In the question “Can formal verification replace simulation in a verification methodology”, all the contestants answered yes to different levels of application. While formal technology is commonly used to complement simulation methodology, on many blocks, it is possible to replace simulation completely with formal. Oski has done many such projects for our customers to build block-level formal testbench so no simulation needs to be run at that level.

Can formal verification replace simulation in a verification methodology?

Oski Decoding Formal” Online Competition Question: Can formal replace simulation in verification methodology?

In answer to a follow-up question “What kind of checkers are needed in order for formal to replace simulation for a block”, most participants understood that it takes interface assertions and end-to-end checkers for formal to replace simulation.

What kind of checkers are needed for formal to replace simulation for a block?

Oski “Decoding Formal” Online Competition Question: What kind of checkers are needed for formal to replace simulation for a block?

As formal technology has an inherent complexity barrier due to the large state space it needs to analyze, often the formal run doesn’t converge. In response to question “What should I do when formal verification times out”, participants correctly explained that all is not lost. Indeed many things can be done to achieve convergence, and the spread of the answers showed a nice mix of techniques such as adjusting constraints, writing abstraction models and ensuring bounded proof is good enough. It is particularly encouraging for us to see that the technique that Oski Technology has been using in all our projects – using Abstraction Models to overcome the complexity barrier – are becoming more widely accepted and regarded as an effective technique.

What should I do when formal verification times out?

Oski Decoding Formal” Online Competition Question: What should I do when formal verification times out?

Oski Technology has been a instrumental in the formal space, fostering the growth of formal technology adoption and its application in design houses worldwide, and it is our goal to see that the engineering community discovers the significant benefits to be had with leveraging formal, and that formal continues to be adopted and understood by the engineering community, worldwide.

Once again we want to thank all contest participants and congratulate our winners on a job well done! Look forward to seeing some of you in San Francisco, June 2014!

Another Awesome DAC for Oski Technology

It is not surprising that so many attendees remember and talk about the excitement of Oski 2012 DAC, where Oski set out to win a daunting and unthinkable 3-day game: “The Oski Live Verification Challenge“. Under the admittedly skeptical eyes of DAC attendees, Oski formal expert Chirag successfully verified a design from NVIDIA sight unseen, and found 4 bugs in 72 hours, using Cadence Incisive Formal Verifier (IFV). It was an incredible testimony of the power of formal technology and the productivity gain one can achieve by applying formal technology in design verification.

This year we decided to turn the challenge around and put DAC attendees to the test on Monday and Tuesday. Fortified with popcorn and ice cream, contestants in Oski’s 2013 “Decoding Formal Challenge” were offered two tracks – Engineer and Manager. All contestants watched a short technical video. Different questions were then posed to the contestants in each track and whomever gave the best answer would get an Oski limited edition “Decoding Formal” Trophy. There was some hot debate and a few very happy winners as seen in the photos below.

Formal-Verification-ChallengeFormal-Verification-Challenge Oski “Decoding Formal” winners at #50DAC

With pre-DAC predictions of low attendance in Austin, we were delighted to have a constant booth traffic, as well as animated discussion and great attendance at booth activities.

It is unfortunate that John Cooley’s “Must See” list has, to date, excluded service providers. It means DeepChip’s readers are missing on some of the Best stories of the industry. Like the Oski DAC 2012 Live Verification Challenge, and the 2013 follow-up demo showing how Oski Abstraction Models can shorten the formal verification run, from 991 days to 3 minutes, a 600,000x improvement. An impressive way to achieve early formal convergence. Demo attendees walked away amazed and inspired to explore how to use Abstraction Models in their work.

If you missed the Oski 2013 Abstraction Models demo at DAC, please contact us. We’d love to show you how we achieved these impressive results.

There was particular interest in Formal sign-off. Formal Sign-off is a relatively new buzzword. Most companies that have deployed formal technology in verification are now looking at taking it to the next level – using formal verification as part of the sign-off criteria. This is where Oski’s methodology and approach, truly shine. Oski’s Formal Methodology focuses on the 4 Cs in a formal Testbench: Constraints, Checkers, Complexity and Coverage. This methodology is applied systematically. The Oski Plan, Verify, and Measure approach is the only way to achieve Formal Sign-off. No surprise that leading semiconductor companies seek us out to get insights on how.

If you missed all the DAC fun, don’t despair. Our newly updated website www.oskitechnology.com has lots of information as well as a few new technical videos where Vigyan shares tips to get you started with the application of formal. Check out our new “Decoding Formal” video series. You won’t be disappointed:

  • How to know when a formal testbench is complete
  • How to achieve early formal convergence with Oski Abstraction Model
  • How to formally verify – and reuse – highly configurable IP designs

Thanks to those who visited us in Austin, TX. Look forward to seeing you all again in San Francisco, June 2014!

“Memoir Systems designs high performance and highly configurable memory IP cores. Formal verification has always been an important strategy to ensure functional correctness of its configurable memory IPs, as it is hard to cover all configurations using simulation. Due to the complex nature of Memoir Systems’ design, Oski Technology is involved to help identify formal verification complexity spots and craft solutions to overcome the complexity challenge. Due to Oski’s engagement, the memory IPs from Memoir Systems are formally verified and exhaustively proven – 100% verified.” (Update: Memoir was acquired by Cisco in September 2014.)

Da Chuang
Co-Founder & COO, Memoir Systems

Oski Technology’s formal verification services and training offers a way for anyone, with or without prior experience, to become expert in the strategic deployment of this methodology. OneSpin is delighted to partner with Oski Technology, to deliver unique verification solutions and execute on the proven Oski formal methodology, enabling our mutual customers to reduce their verification schedules with this powerful approach.

raikRaik Brinkmann
CEO, OneSpin Solutions

‪DAC 2012: Vigyan Interview with Joe Hupcey on Oski Technology’s Courageous “72 hour Verification Challenge”

2_Dvcon-13
I’ve seen a lot of intriguing promotions over the years, but at DAC 2012 our partners at Oski Technology (‪http://www.oskitechnology.com) tackled a truly unique challenge: to show off their formal verification prowess they took an IP block from NVIDIA sight unseen (actually, on Sunday evening before the DAC they received a spec and a 15 minute briefing) and over the course of 72 hours from Sunday at 5pm to Wednesday at 5pm they used Incisive Enterprise Verifier (“IEV”) and their years of verification experience to deliver impressive results. In this video Oski’s CEO Vigyan Singhal gives a snapshot of the challenge while it was in progress, and then reports on the results after the dust has settled.

Oski Tutorial on End-to-End Formal

Oski’s Vigyan Singhal presented an invited tutorial on October 30 at FMCAD 2011, the eleventh in a series of conferences on the theory and applications of formal methods in hardware and system verification.

FMCAD Oski Tutorial

When: October 30 – November 2
Where: FMCAD 2011, Austin, TX
Paper: End-to-End Formal using Abstractions to Maximize Coverage

FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing.

About Oski

Oski Technology is the world’s first and only formal verification services company to successfully leverage off-the-shelf EDA tools with a unique formal verification methodology for the proper integration of formal with simulation and End-to-End Formal verification. Oski has pioneered a new approach with its proprietary Oski Abstraction Models, delivering complete End-to-End Formal verification of even the most complex SOC designs.

Visit Oski Technology at www.oskitechnology.com.

Oski to Exhibit Formal Verification Methodology at #ARM TechCon 2012 Chip Design Day, Oct. 30

Oski Technology will be presenting a video recap of its recent groundbreaking success with the Oski Live Formal Verification Challenge wherein Oski formally verified a new design, sight unseen from NVIDIA live at DAC 2012, finding four corner-case bugs plus end-to-end checkers in less than 72 hours. Oski Technology will be exhibiting at ARM TechCon 2013 Chip Design Day, Tuesday Oct 30, San Jose, CA.

Oski Technology provides formal verification methodology for complex SOC designs. Oski verifies ARM-based designs both for ARM AMBA AXI protocol compliance, and ACE cache coherence. Oski will be at #ARM 2012, booth 49. ARM TechCon is the leading conference on the practice of functional verification of IC designs.

The 2012 ARM TechCon Expo offers attendees a unique opportunity to learn about technology solutions, which can lead to better and correct decision making in product and vendor selections. Chip Design Day is a one-day intensive conference for chip design teams working with ARM silicon IP and tools, and the only conference dedicated to the ARM architecture.

Time: ARM TechCon Chip Design Day exhibits are open October 30, 10:30am-7:00pm
Venue: Oski Booth #49, Santa Clara Convention Center, California.
Web: http://exhibitors.techweb.com/armtechcon/2012/

Visit Oski Technology at www.oskitechnology.com.

Video: How to Know When a Formal Testbench is Complete

Decoding Formal Video Tutorial Series: How to Know When a Formal Testbench is Complete

This is an important problem because if you have decided to replace simulation with formal verification on a block you are working on, you want to know when to sign off with the work you have done. Three factors determine whether or not you are done with your formal testbench: constraints, checkers, complexity.

Video: How to Achieve Early Formal Convergence with Oski Abstraction Models

Decoding Formal Video Tutorial Series: How to Achieve Early Formal Convergence with Abstraction Models

The state space for formal is huge. If you have a design with 300 flops, that is already more states than there are atoms in the universe. So the state space is growing exponentially. Formal tools are limited by design size and where the proofs stop converging. Abstraction models can transform the search space for a formal verification run, and bring states which are distant close to the search state, allowing the proofs to converge much faster.

Video: How to Formally Verify – and Reuse – Highly Configurable IP Designs


Decoding Formal Video Tutorial Series: How to Formally Verify and Reuse Highly Configurable IP

Many designs these days support all sorts of IPs, and we want to verify these designs. However with tight schedules, we don’t have the luxury of building from scratch, so the best thing to do is re-use IPs from 3rd parties or internal designs. We are still responsible for IP from 3rd parties. The designs are very configurable and the IPs themselves are highly configurable. The problem is that there are billions of different configurations. The beauty of formal verification is that you can try all of these different configurations together by making them a symbolic constant.

Verifying IP especially highly configurable IP becomes extremely valuable if you do it with formal because you get a level of coverage that is almost impossible to get with simulation.

DVCON 13: Vigyan Interview with Joe Hupcey about how careful advanced planning can substantially reduce risk in verification projects

2_Dvcon-13

Joseph Hupcey speaks with Vigyan Singhal, CEO and formal and ABV specialist Oski Technology at DVCon 2013. Singhal shares insights about how careful, advanced planning can substantially reduce risk with formal verification.