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.

 

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

 

You can check our formalISA from Axiomise here