Schlagwort: Oski

Oski Technology, an Expert in Formal Verification, Joins NVIDIA

We are exci짯ted to announ짯ce that Oski Tech짯no짯lo짯gy, a com짯pa짯ny spe짯cia짯li짯zing in for짯mal veri짯fi짯ca짯ti짯on methods, will be joi짯ning NVIDIA.

Modern pro짯ces짯sors pack tens of bil짯li짯ons of tran짯sis짯tors, tiny on/off swit짯ches con짯nec짯ted by bil짯li짯ons of micro짯sco짯pic pathways. A bug in a sin짯gle tran짯sis짯tor can pre짯vent a chip from ope짯ra짯ting cor짯rect짯ly, requi짯ring cos짯t짯ly revi짯si짯ons to fix.

Today, veri짯fi짯ca짯ti짯on engi짯neers rely on two very dif짯fe짯rent methods to make sure bugs don셳 make it into sili짯con simu짯la짯ti짯on and for짯mal verification.

The first approach reli짯es on mil짯li짯ons of simu짯la짯ti짯ons that search for bugs, exer짯cis짯ing cor짯ner cases in careful짯ly desi짯gned tests.

For짯mal veri짯fi짯ca짯ti짯on, Oski셲 spe짯cial짯ty, is a powerful alter짯na짯ti짯ve that uses mathe짯ma짯ti짯cal ana짯ly짯sis of a design ins짯tead of simu짯la짯ti짯ons to pro짯ve that a par짯ti짯cu짯lar fea짯ture beha짯ves cor짯rect짯ly for all pos짯si짯ble inputs.

Whe짯re짯as simu짯la짯ti짯on injects 1셲 and 0셲 into a design to test whe짯ther num짯bers are added pro짯per짯ly, Oski셲 approach for짯mal짯ly veri짯fies that 쐁 = a + b. () Wei짯ter짯le짯sen 쨩