Word-level predicate-abstraction and refinement rechniques for verifying RTL Verilog

Word-level predicate-abstraction and refinement rechniques for verifying RTL Verilog

As a first step, most model checkers used in the hardware industry convert a high-level register-transfer-level (RTL) design into a netlist. However, algorithms that operate at the netlist level are unable to exploit the structure of the higher abstraction levels and, thus, are less scalable. The RT...

Detaylı Bibliyografya
Asıl Yazarlar:	Jain, H, Kroening, D, Sharygina, N, al., E
Materyal Türü:	Journal article
Baskı/Yayın Bilgisi:	Institute of Electrical and Electronics Engineers 2008

Benzer Materyaller

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
Yazar:: Jain, H, ve diğerleri
Baskı/Yayın Bilgisi: (2008)

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
Yazar:: Jain, H, ve diğerleri
Baskı/Yayın Bilgisi: (2005)

Word level predicate abstraction and refinement for verifying RTL verilog
Yazar:: Jain, H, ve diğerleri
Baskı/Yayın Bilgisi: (2005)

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
Yazar:: Jain, H, ve diğerleri
Baskı/Yayın Bilgisi: (2008)

Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs
Yazar:: Kroening, D, ve diğerleri
Baskı/Yayın Bilgisi: (2007)

VCEGAR: Verilog CounterExample Guided Abstraction Refinement
Yazar:: Jain, H, ve diğerleri
Baskı/Yayın Bilgisi: (2007)

Verification of SpecC and Verilog using Predicate Abstraction
Yazar:: Jain, H, ve diğerleri
Baskı/Yayın Bilgisi: (2004)

Checking consistency of C and Verilog using predicate abstraction and induction
Yazar:: Kroening, D, ve diğerleri
Baskı/Yayın Bilgisi: (2004)

Checking Consistency of C and Verilog using Predicate Abstraction and Induction
Yazar:: Kroening, D, ve diğerleri
Baskı/Yayın Bilgisi: (2004)

Verifying C++ with STL Containers via Predicate Abstraction
Yazar:: Blanc, N, ve diğerleri
Baskı/Yayın Bilgisi: (2007)

Verifying C++ with STL containers via predicate abstraction
Yazar:: Blanc, N, ve diğerleri
Baskı/Yayın Bilgisi: (2007)

System verilog RTL modeling with embedded assertions /
Yazar:: Chow, Chee Siang, 1984-, ve diğerleri
Baskı/Yayın Bilgisi: (2012)

Predicate abstraction of ANSI-C programs using SAT
Yazar:: Clarke, E, ve diğerleri
Baskı/Yayın Bilgisi: (2004)

Predicate Abstraction of ANSI–C Programs using SAT
Yazar:: Clarke, E, ve diğerleri
Baskı/Yayın Bilgisi: (2015)

Predicate Abstraction of ANSI-C Programs Using SAT.
Yazar:: Clarke, E, ve diğerleri
Baskı/Yayın Bilgisi: (2004)

SATABS: SAT−based Predicate Abstraction for ANSI−C
Yazar:: Clarke, E, ve diğerleri
Baskı/Yayın Bilgisi: (2005)

Predicate Abstraction of ANSI-C Programs Using SAT
Yazar:: Clarke, E, ve diğerleri
Baskı/Yayın Bilgisi: (2004)

System verilog RTL modeling with embedded assertions[electronic resource] /
Yazar:: Chow, Chee Siang, 1984-, ve diğerleri
Baskı/Yayın Bilgisi: (2012)

The RTL design of 32-bit RISC processor using verilog HDL /
Yazar:: Hafizul Hasni Manab, 1987-, ve diğerleri
Baskı/Yayın Bilgisi: (2012)

Approximating Predicate Images for Bit−Vector Logic
Yazar:: Kroening, D, ve diğerleri
Baskı/Yayın Bilgisi: (2006)

Hooray For Hollywood: Onomastic rechniques in Bentelntans' “Dirty Eddie”
Yazar:: Leonard R.N. Ashley
Baskı/Yayın Bilgisi: (1988-12-01)

Verification of SpecC using Predicate Abstraction
Yazar:: Clarke, E, ve diğerleri
Baskı/Yayın Bilgisi: (2007)

Verification of SpecC using predicate abstraction.
Yazar:: Clarke, E, ve diğerleri
Baskı/Yayın Bilgisi: (2007)

The RTL design of 32-bit RISC processor using verilog HDL [electronic resource] /
Yazar:: Hafizul Hasni Manab, 1987-
Baskı/Yayın Bilgisi: (2012)

Predicate Abstraction with Under-approximation Refinement
Yazar:: Corina S. Pasareanu, ve diğerleri
Baskı/Yayın Bilgisi: (2007-02-01)

Counterexamples with Loops for Predicate Abstraction
Yazar:: Kroening, D, ve diğerleri
Baskı/Yayın Bilgisi: (2006)

The RTL design of 32-BIT 5- stage pipeline risc processor using verilog HDL /
Yazar:: Lim, Jonie Joo Nee, 1978-, ve diğerleri
Baskı/Yayın Bilgisi: (2008)

The RTL design of 32-BIT 5- stage pipeline risc processor using verilog HDL [electronic resources] /
Yazar:: Lim, Jonie Joo Nee, 1978-, ve diğerleri
Baskı/Yayın Bilgisi: (2008)

Verification and Falsification of Programs with Loops Using Predicate Abstraction
Yazar:: Kroening, D, ve diğerleri
Baskı/Yayın Bilgisi: (2009)

Verification and falsification of programs with loops using predicate abstraction.
Yazar:: Kroening, D, ve diğerleri
Baskı/Yayın Bilgisi: (2010)

Model Checking with Abstraction for Web Services
Yazar:: Sharygina, N, ve diğerleri
Baskı/Yayın Bilgisi: (2007)

V2c – A Verilog to C translator
Yazar:: Mukherjee, R, ve diğerleri
Baskı/Yayın Bilgisi: (2016)

Strengthening properties using abstraction refinement
Yazar:: Purandare, M, ve diğerleri
Baskı/Yayın Bilgisi: (2009)

RTL cookbook/
Yazar:: 274324 Lancaster, Don
Baskı/Yayın Bilgisi: (1969)

RTL2RTL Formal Equivalence: Boosting the Design Confidence
Yazar:: M V Achutha Kiran Kumar, ve diğerleri
Baskı/Yayın Bilgisi: (2014-07-01)

Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
Yazar:: Kroening, D, ve diğerleri
Baskı/Yayın Bilgisi: (2003)

Counterexample Guided Abstraction Refinement via Program Execution
Yazar:: Groce, A, ve diğerleri
Baskı/Yayın Bilgisi: (2004)

Automated scripts for testing verilog designs with iVerilog
Yazar:: Ng, Gary Jia Hao
Baskı/Yayın Bilgisi: (2015)

RTL Conversion Method From Pipelined Synchronous RTL Models Into Asynchronous Ones
Yazar:: Shogo Semba, ve diğerleri
Baskı/Yayın Bilgisi: (2022-01-01)

Counterexample-guided abstraction refinement for symmetric concurrent programs
Yazar:: Donaldson, A, ve diğerleri
Baskı/Yayın Bilgisi: (2012)