让 RISC-V 走向市场：形式化验证的经济意义.pdf

1、 Axiomise Limited 2025.All rights reserved.Making RISC-V Market Ready Dr.Ashish DarbariFounder&CEOAxiomiseThe Economic Case for Formal Verification Axiomise Limited 2025.All rights reserved.Verification trendsWilson research reports 2022-202475%IC/ASIC projects run behind schedule60-80%Overall verif

2、ication costs86%ASICs require two or more respins62%Logical/Functional flaws causing re-spins in designs(1B gates)83%FPGA designs with non-trivial bug escapes1030 simulation cycles not finding bugs Axiomise Limited 2025.All rights reserved.Verification trendsWilson research reports 2024 Axiomise Lim

3、ited 2025.All rights reserved.Formal verification servicesScaling formal for big designs enabling end-to-end sign-offThe Axiomise team has experience in verifying over 150 designsDMA controllerMulti-threaded processorBus bridges(AXI/CHI/OCP/TileLink)Cache sub-systemsGPU shadersI2C/USB/HDMI/I2SNetwor

4、k-on-chip AI/ML acceleratorEthernet SwitchMixed-signalLow-powerPower controller150+Axiomise Limited 2025.All rights reserved.Why is chip verification hard?Why bugs escape to silicon?Axiomise Limited 2025.All rights reserved.A holistic approach is missingA unifying perspective is missingDESIGN/MICROA

5、RCHITECTUREARCHITECTURENETLIST SILICONArchitecturalMicro-architecturalSecurityX-propagationLockstep verificationDeadlockPower Axiomise Limited 2025.All rights reserved.Modern-day processorsPipeliningInterlockingForwardingBranchesJumpsExceptionsStalls Interrupts DebugExtensions Clock gating Arithmeti

6、cPower Safety SecurityMassively optimised Axiomise Limited 2025.All rights reserved.Complex control and data dependenciesBranches:Speculative branches Forward jumps,Backward jumps,Page size jumps,Page boundary jumps,Jumps across pages(same or different pages)Back-to-back memory operations:Cache hits