RISC-V open source architecture is creating new opportunities for semiconductor designs in a way that is unprecedented. However, as processors become more complex with design optimisations, verification is becoming a major roadblock. Quadrillions of simulation cycles are not picking up simple design bugs that ought to have been caught on day one. 

Processors are increasingly being used in automotive, and functional safety is a major requirement that needs addressing in verification for reliability and for compliance with standards such as ISO26262. 

Security flaws are detected now almost everyday in commercial grade processors, so security verification is equally important. As AI/ML dominates the landscape of semiconductors, functional correctness is as important as safety, security and low-power. 

Formal verification can establish proofs of bug absence whilst at the same time can catch corner-case bugs. At Axiomise, we have taken the formal verification for RISC-V processors to a whole new level providing end-to-end functional correctness, architectural compliance, as well as six-dimensional coverage to provide the best assurance possible by any verification technology.

Our RISC-V studio is a collection of public talks and product demos that showcase our formal verification solutions for RISC-V on several open-source RISC-V processors.

Who should view this?

Graduate students in EE, CS, Mathematics, Physics**

Practising engineering professionals 

Semiconductor design and verification engineers

Architects and managers in semiconductor companies


Knowledge of RISC-V

Some knowledge of digital design 

Verilog/VHDL knowledge would help

What you will learn?

Why use formal verification?

Why use formal methods for RISC-V verification?

What kind of bugs can be caught with formalISA?

How do you get started with RISC-V formal verification?

How do you sign-off a RISC-V processor using formal?