SAT-Riešitelia vo formálnej verifikáciu

[djhulme]

Dobrý deň, som výskumník University College v Londýne a ja rozvíjať logické algoritmy splniteľnosti (SAT-Riešitelia). Hľadám žiadosti o ne, a ja som bol hovoril, že SAT-riešiteľmi sú používané v celom procese formálnej verifikácie v priemysle EDA, a chceli by ste sa dozvedieť viac o tom. Mohol by mi niekto povedať viac o tom, ako je SAT aplikovaný na proces FV. Kto ho používa? Prečo sa používa? Ako sa to používa? Koľko to používa? Mená a čísla by bolo veľmi užitočné. So srdečným pozdravom, Daniel

 

[Meridian]

[Quote = djhulme] Dobrý deň, som výskumník University College v Londýne a ja rozvíjať logické algoritmy splniteľnosti (SAT-Riešitelia). Hľadám žiadosti o ne, a ja som bol hovoril, že SAT-riešiteľmi sú používané v celom procese formálnej verifikácie v priemysle EDA, a chceli by ste sa dozvedieť viac o tom. Mohol by mi niekto povedať viac o tom, ako je SAT aplikovaný na proces FV. Kto ho používa? Prečo sa používa? Ako sa to používa? Koľko to používa? Mená a čísla by bolo veľmi užitočné. So srdečným pozdravom, Daniel [/quote] Tu je pár odkazov, ktoré vám pomôžu čítanie ... : D http://www.satlive.org/ http://research.microsoft.com/users/lintaoz/papers/dac_2001.pdf http: / / www.cs.sfu.ca/ ~ mitchell/papers/colLogCS85.pdf http://www.satlib.org/solvers.html ... Nezabudnite stlačte tlačidlo mi pomohol Butón ... : D

 

[djhulme]

Ďakujeme, že ste pre tieto prípady. Som veľmi dobre oboznámení s technológiou, je to informácia o tom, kde So. Sedia v procese FV, ktoré potrebujem. Aj v podstate by som rád vedel, komerčný potenciál SAT riešič, ktorý môže hrať lepšie ako súčasný stav-of-the-art. Ako sa vám previesť skúšobnú FV problém na SAT? (Z hľadiska FV - viem o De Morgans právo, atď) Aké typy skúšok sú prevedené do problémov, SAT? (V laymans) Koľko problémov bežal na Solvers SAT-mesačne pre daný čip? Aké percento EDA / FV proces zdvihnutý pomocou SAT? Aké sú čas a náklady spojené s používaním SAT riešiteľov vo FV? Koľko prínosom by nový SAT-Riešiteľ dať procesu FV? Vzhľadom k tomu, že sú o 10% "rýchlejšie" ako ostatné riešiteľa, napríklad. S pozdravom, Daniel