Axiomising RISC-V processors through formal verification

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.

Read the article here

Getting Started with Formal Verification

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. 

Read the article on EEWeb

A Brief History of Formal Verification

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.

Read the article on EEWeb

11 key questions on formal verification

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.

Read the article on Tech Design Forum

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?

Read the article on Medium

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.

Read the article at Tech Design Forum

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.

Read the article at Tech Design Forum

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.

Read the article at Tech Design Forum

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.

Read the article at Tech Design Forum

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.

Read the article at Tech Design Forum

Living verification in the fast lane

I have been associated with formal verification for so long yet I still wonder why it remains a niche verification paradigm despite its tremendous success in numerous forms throughout the industry. We have seen the deployment of industrial-grade theorem provers, commercial formal tools, and even scalable equivalence checking. But formal is not used every day by every design verification engineer.

Read the article at Tech Design Forum

When ‘silicon proven’ is not enough

Who would have thought the New Year would start on such a rocky note for all things digital? I am talking, of course, about Spectre and Meltdown.

I admit I didn’t pick up the signs when trouble started brewing last June. Having done some research, the problems appear to have been kept deliberately under wraps, so that hackers would not immediately start looking for exploits.

Read the article at Tech Design Forum

Verification: Crisis of Confidence - III

In the first two parts of this series, I described the verification crisis, explained how it came about, and began to describe the pillars and, within them, components of a responsive design verification (DV) flow. In this part we focus on debug.

Read the article at Tech Design Forum

Verification: Crisis of Confidence - II

In the first part of this series  I described the need for good verification meta models and the qualities that define them. Those are the right combination of verification technologies and methodologies deployed in the correct order, by a trained workforce of skillful design verification (DV) engineers, with the goal of minimizing risk by hunting down bugs before they reach silicon.

The key requirement within the meta model is that it outlines a methodology that describes an efficient DV flow to catch bugs as early as possible (shift-left) and gives the user certainty that desired quality levels will be met on schedule. In simple terms: Quality must not compromise productivity, and equally, productivity must not compromise quality.

Read the article at Tech Design Forum

Verification: Crisis of Confidence - I

In this three-part series, I look at broad challenges facing semiconductor verification and explain how they have grown to leave us facing a crisis of confidence. I will explore some of the key reasons why, despite astronomical growth in constrained random, emulation, and FPGA prototyping, we continuously grapple with poor quality.

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?

Read the article at Tech Design Forum

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.

Read the article at Tech Design Forum

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

Read the article at Tech Design Forum

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.

Read the article at Tech Design Forum