Accelerating exhaustive and complete verification of RISC-V processors
In this article, Axiomise and Cadence explore verification trends and ask the question: what makes processor verification hard and how it can be made easier? The answer lies in the use of formal methods in particular using the fully automated vendor-neutral formal formalISA app from Axiomise in combination with the JasperGold® Formal Verification Platform from Cadence. By leveraging the six-dimensional coverage including scenario coverage from Axiomise in conjunction with JasperGold coverage models, one can obtain the best possible assurances about the quality of formal verification for RISC-V. We also discuss a new automated debug, analysis and reporting solution (i-RADAR™) from Axiomise that allows accelerated debug and reporting.
Life in a Formal Verification Lane
Shivani Shah described her six-week internship in a new SemiWiki blog. Shivani found 30 new bugs in the previously formally verified WARP-V processor using the formalISA app that she also extended. She verified three cores in six weeks starting her life in formal verification from scratch by taking the brand new online formal verification training course.
Why I made the world’s first on-demand formal verification course?
Ashish Darbari describes why he designed the brand new online formal verification training course in the latest blog on SemiWiki.
Bugs: A verification engineer’s dream, a designer’s nightmare
One person’s nightmare is another person’s dream! This Diwali, take a pledge to wipe out the darkness coming from bugs in your design, and shine the light of exhaustive proofs using formal methods, so every day is a happy Diwali for you!
The Secret of RISC-V Formal Verification: Think Big, Think Small
In this article, we share our secrets of verifying RISC-V processors using formal verification. We describe a holistic methodology covering the entire spectrum of verification challenges ranging from the ‘big’ architectural ones to the ‘small’ micro-architectural ones. We have rolled this methodology out on several RISC-V implementations and found bugs ranging from trojans, to functional safety, to low-power issues, going beyond the standard remit of functional verification where we found loads of issues as well. We talk about this approach in the upcoming DVCon India conference in Bengaluru.
Reduce Risk with RISC-V Processors
Designing RISC-V processors has become easier due to the open-source ISA; however, verification remains a challenge. In this blog, Ashish Darbari discusses the Axiomise vision and the new unique solution that Axiomise is offering to verify RISC-V designs both architecturally as well as micro-architecturally. Several bugs have been found in a family of RISC-V cores using the Axiomise methodology and ISA formal proof kit.
Axiomising RISC-V processors
We describe our new RISC-V formal verification solution designed with our brand new proof kit. We provide a comprehensive history of processor formal verification and describe the key components of our methodology.
Getting Started with Formal
There are two ways to become introduced to the area of formal verification. One is to dive deep into the theoretical foundations of formal and understand how formal tools work, what algorithms they use, how the different flavors of theorem provers and equivalence checkers work, and also to master the principles of tool development. Alternatively, a more practical approach is to start using the tools to verify your designs; this is a much simpler way to get started with formal verification. In this article, I take the latter view and provide a quick introduction to formal property checking.
A Brief History of Formal
In this article I review the origins and evolution of formal verification, which is a field with a fascinating history spanning over 70 years. I’ve been a user of formal methods for over two decades and – although I’ve not had a career as illustrious as some of the people whose contributions I cover in this column – I’ve certainly enjoyed using formal methods in all their glory, from interactive theorem proving to state-of-the-art model checking to equivalence checking. Along the way, I like to think that I’ve made my own small contributions.
11 key questions on formal
During DVCon USA I was able to meet with numerous colleagues from industry and academia. I presented a new research paper and helped to present a Synopsys-sponsored tutorial. Whether presenting or not, events like these can and should be like multi-day Q&A sessions. What I’ve tried to capture here are some of the most important questions I faced during the conference, together with how we at Axiomise set about answering them.
Reflections on Verification
It is the week before DVCon – industry’s premier design verification conference. I will be delivering a tutorial on formal verification challenges for datapath and control on Thursday 28 Feb and will be presenting a research paper on applying formal in a smart manner to achieve scalable results on Wednesday 27 Feb — so its natural that verification is on my mind. I’ve reflecting a lot this week on challenges and opportunities for validation and verification and wondering if the glass is half empty or half full?
Introducing the ADEPT FV flow
In an industry which responds to technology changes so swiftly, the changes in process take a long time to come through. We are designing cutting-edge technology in our chips that are driving the revolution in the Internet-of-Things using age-old processes that do not respond that well to the requirements of modern-day design and verification. We cannot afford to build chips that are vulnerable from a security point of view or require massive re-engineering (due to finding late bugs). In this article I want to describe an agile design verification flow that uses formal verification to assist you in end-to-end design bring-up and verification. We call this flow ADEPT FV and it describes a concept formal verification (FV) flow that can be used by both designers and verification engineers to tape out designs without bugs.
Formal verification of packet-based designs
The verification of designs that transport data in a serial manner is a challenge for both simulation and formal techniques. The complexity of such designs stems from the ‘serialized’ nature of the packet flow where the state of each packet depends upon the history of all the previous packets in flight. What is interesting about such designs is that they are present everywhere in all kinds of hardware designs. Packet-based serialized data flows can be seen in networking routers, bus protocols, bus bridges, load-store units in CPUs, packing and unpacking designs, and SoC peripherals such as USB, UART, Ethernet.
The budget case for formal
Axiomise launched its formal verification training program at the same time as the recent Verification Futures 2018 conference in the UK, where I set out a new vision for formal. Afterwards, I was contacted by a number of seasoned simulation experts interested in formal verification. Quite a few asked me not only to explain how formal differs from simulation-based verification but also why one should make the investment in learning and deploying it.
Harness the power of invariant-based bug hunting
What’s the biggest design you can verify with formal? It’s a question I get asked a lot. The short answer I always give is it is not the size that matters but the micro-architecture of the design – and yes, design configuration does play a role, but it is not the only thing that rules the proof complexity.
Ten golden rules for formal
About three years ago I gave a couple of talks on the legend of myths surrounding formal. The talk I gave was on the “Ten Myths About Formal”, that was covered by Tech Design Forum and a video was recorded by Cadence at their DAC booth. Although, formal has seen more adoption since then, we have a long way to go before it is recognized as a mainstream technology used throughout design and verification. I still see some of these myths clouding the judgement of end users and their managers. I just came back from DVCon USA, and on the very entertaining panel on whether one should go deep or go broad with formal, we were discussing whether one needs a PhD to do formal! Well one thing we could all agree was that you don’t. What you do need is the combination of a disciplined process, plan and execution of good rules.
Living verification in the fast lane
When ‘silicon proven’ is not enough
Verification: Crisis of Confidence - III
Verification: Crisis of Confidence - II
Verification: Crisis of Confidence - I
This crisis of confidence has reached fever pitch: verification schedules routinely run late, bugs are often missed, silicon re-spins happen, and even worse, disgruntled customers are walking away from projects, hanging silicon vendors out to dry! When did this start? How did we get ourselves into such a mess? And how do we get out of it?
Evolution of formal verification – Part Two
This is the second part of an analysis as to how formal verification has evolved so that it can now be applied to major project challenges. Having described the technology’s foundations in Part One, this article moves on to look at real-world contemporary uses of formal as illustrated by practical examples.
Evolution of formal verification – Part One
We celebrate innovation and creativity in the way we cherish fortresses, castles, and other monuments built throughout history. We have always been infatuated with architecture, with the design of the finished structures, even with the process itself, but not with how these buildings were tested. Many books describe how amazing landmarks were built and explain their beauty, but you are unlikely to find much about how they were examined for quality and rigour.
Introducing DocFormal
Welcome, intrepid readers, to the Doc Formal column. Since this is my first post, let me introduce myself and describe how formal verification became my life’s passion. After all, when you are selecting a medical doctor, an initial peek at his/her credentials is wise. Your sources for technical insight should face the same scrutiny.