Formální kontroly a kontroly konvenčních

S

steven852

Guest
Dobrý den, zajímalo by mě, kdy použít a jaké kritéria by bylo, pokud jde o používání formální ověření nástrojů a ověřování tradičních nástrojů (není jistý, jestli to jméno je pravé, mám na mysli obecné nástroje k tomu ověřování: Verilog, VHDL, e, atd.). I přes některá omezení formální verifikační nástroje (v případě rejstříku Retiming, atd.), je to dost silný, tak proč stále potřebujeme klasické nástroje? Díky
 
Dobrý den, mám pochybnosti. Jsem v tomto pojetí formální verication. mohou u ujasnit, zda funkčnost lze ověřit pomocí formální verifikace?
 
Jistě, formální verifikace nejen umí Ověření funkčnosti, ale i fyzické ověření (netlist kontrola). Stručně řečeno, 4 kombinace mezi RTL a brány úrovni netlist ověřit, stejně jako soubory knihovny.
 
Dva způsoby kontroly jsou 1 - Formální verifikace 2 - Funkční verifivication Každý z nich má svou vlastní metodiku
 
"Formální verifikace nemůže dokázat, že všechny vlastnosti konstrukce byla zahrnuta do výčtu, i když pro danou vlastnost, že může prokázat, zda nemovitost je spokojen." toto prohlášení, mám z knihy. doufám, jeho jasné odpovědi na první otázku.
 
No, všechno, co řekl, je pravda. Avšak to, co konkrétní situace může být účtován byla moje otázka. Díky ačkoli.
 
Formální verifikace se používá hlavně při testování na úrovni bloků, zatímco návrhář píše modul pro ověření, zda modul pracuje s ohledem na všechny případy (vstupy) dle tvrzení uvedených v návrhu. To může být jistě výhodou pro ověření projektu v rané fázi. díky a pozdravem
 
Formální verifikace převýšení kontrolu chyb v RTL.
Myslím, že to není rue. Formální verifikace je účinný způsob, jak najít chyby v návrhu, pokud máte dobře napsaný tvrzení a monitory
 
Formální verifikace je zkontrolovat, zda se jedná o stejnou funkci mezi RTL a netlist.
 
Mám pocit, že některé členské tady nechápou, co přesně je "formální verifikace". Nechte mě pokusit se dát trochu pozadí .... Formální verifikace není nic jiného než se snaží vyřešit problém formálně pomocí matematického přístupu. K dispozici jsou 3 druhy se na ní podílejí: 1. Model Kontrola 2. Ekvivalence prověřit 3. Dokazování vět. "Rovnocennost Kontrola" je nejčastější věc, kterou znám všechny, ale většinou jen formální verifikace (Tools: formální úkon). To se používá ke kontrole rovnocennost mezi RTL na RTL nebo RTL na netlist. "Model checking", je místo, kde budeme psát formální vlastnosti popisuje očekávané chování a nástroje mohou prokázat, zda je tato vlastnost platí ve všech možných podmínkách. (Nástroje: Cadence IFV - pronikavý formální ověřovatel) Některá kritéria se podívat na zde jsou: - Kdykoliv design je kontrola intenzivní, že je velmi dobrým kandidátem pro model checking. - Pokud je návrh datové cesty intenzivní, že je nejlepší kandidát na vysoké úrovni jazyků ověření (e-specman, Věra ..) S pozdravem, http://hdlplanet.tripod.com http : / / groups.yahoo.com / skupina / hdlplanet
 

Welcome to EDABoard.com

Sponsor

Back
Top