Axiomise Wiki

Why Choose Axiomise?

Dr Ashish Darbari founder & CEO of Axiomise has been involved in formal verification deployment in different organisations in the past decade. He has the experience of working in the field – both with the EDA tool companies as well as being a customer of EDA – deploying formal verification on different projects on the coal face in different organisations. He understands what it takes to work with real human beings who are desperate for help and would want honest and professional advice on using formal verification on projects with tight deadlines.

A keen innovator with 35 international patents in the area of formal verification, and over two dozen research papers Dr Darbari brings his passion for excellence, customer focus, and honesty to Axiomise. At Imagination Technologies, he led a team of three engineers to provide verification consulting for 5o+ projects ranging from MIPS, PowerVR, Ensigma and IMGWorks (SoC division). He believes that customers thrive on open and transparent consulting.

Multi-pronged

At Axiomise we take a multi-pronged approach to enabling customers in formal. Our mantra is very simple, we want you the customer to be successful and to do that we are able to provide flexibility in all our offerings. We understand that no two customers are the same and therefore their requirements would vary. We believe that the customers need a combination of training, consulting and project support to make them self sustainable in executing formal with success.

The core of our solutions is based on scalable formal verification methodologies that are proven to work in practice and this reflects in our three layers of training, consulting and project support. However, we understand that formal does not work in silos, so we provide detailed consulting to enable our customers to understand how to integrate formal with other verification solutions. We therefore provide our consulting services focussed on verification strategy, planning, execution and review. But since no two customers are the same in requirements for project execution we remain flexible in scoping and providing project support that our customer really needs.

Unique Training

We believe that good training and understanding in-depth on how to use formal verification in practice is the secret to success. At Axiomise we have spent years working on formal verification projects in industry to understand what works well in practice and what doesn’t. We have learnt by doing it ourselves and this hands-on experience is reflected in our vendor-neutral training programmes making it truly unique. Read some of the testimonials provided on the quality of training.

We have noted over the years that not only do engineers need technical training, sometimes their managers also need to understand the scope and value-proposition of formal. At Axiomise, we provide a training module that gives busy managers a quick view of formal’s key benefits and gives them insight on how to deploy formal on projects.

Methodology Focus

– Our training, consulting and services is focussed on methodologies of scalable formal verification
– Our knowledge is based on best practices developed at Axiomise
– We undertake verification audits whereby we can review your verification plans, strategies and your testbenches
– We provide services on real projects where we can advise you on the best strategies for applying formal
– Our methodologies have been used on industrial sized projects and are proven to work well in practice
– We cover the entire formal verification flow, not just focus on the use of properties

Tool Agnostic

Understanding how the tools work and how to use their features properly is equally important; so we offer an opportunity to learn this from us. At Axiomise we have people who have used a range of commercial tools in the market and have experience of building some themselves. We offer a training programme that can be adapted to work with your tool of choice, but at the same time, we provide insights into the tools in conjunction with our EDA partners.

What you will notice from our training is that our methodology focus is very much tool agnostic, and yet we bring in the focus on tools when we need to join the dots to complete the full picture.

Solutions

Consulting & Services

Modern processors implement numerous optimizations for power, performance, and area. Optimizations such as pipelining, interlocking, and data forwarding introduce numerous data dependencies and hazards causing processors to deadlock or produce incorrect results. The number of instruction combinations, together with instruction interleaving and multiple register files and operands make it impossible for any simulation-based verification to be exhaustive.

Formal verification produces exhaustive proofs of correctness and finds corner-case bugs in design implementations. The challenges with formal verification, however, are:

• Proof convergence is not guaranteed
• No consistency of formal coverage models across different formal verification tools.
• No consistency between formal coverage models and simulation

The formalISA® app addresses all these challenges successfully. Built on top of the first-generation ISA formal verification proof kit from Axiomise, the formalISA® app is powered by a clean graphical-user-interface that allows the end-user to push a few buttons to obtain formal verification results on a RISC-V core of their choice, using a formal verification tool of their choice.

The push-button ‘ Prove’ & ‘Cover’ solution eliminates the need to:

• Write a single test case
• Write complex test sequences
• Write scoreboard or checkers
• Write constraints
• Randomize stimulus

Company Website

Axiomise on SemiWiki