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...

Ausführliche Beschreibung

Bibliographische Detailangaben
Hauptverfasser:	Jain, H, Kroening, D, Sharygina, N, al., E
Format:	Journal article
Veröffentlicht:	Institute of Electrical and Electronics Engineers 2008

Ähnliche Einträge

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
von: Jain, H, et al.
Veröffentlicht: (2008)

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
von: Jain, H, et al.
Veröffentlicht: (2005)

Word level predicate abstraction and refinement for verifying RTL verilog
von: Jain, H, et al.
Veröffentlicht: (2005)

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
von: Jain, H, et al.
Veröffentlicht: (2008)

Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs
von: Kroening, D, et al.
Veröffentlicht: (2007)

VCEGAR: Verilog CounterExample Guided Abstraction Refinement
von: Jain, H, et al.
Veröffentlicht: (2007)

Verification of SpecC and Verilog using Predicate Abstraction
von: Jain, H, et al.
Veröffentlicht: (2004)

Checking consistency of C and Verilog using predicate abstraction and induction
von: Kroening, D, et al.
Veröffentlicht: (2004)

Checking Consistency of C and Verilog using Predicate Abstraction and Induction
von: Kroening, D, et al.
Veröffentlicht: (2004)

Verifying C++ with STL Containers via Predicate Abstraction
von: Blanc, N, et al.
Veröffentlicht: (2007)

Verifying C++ with STL containers via predicate abstraction
von: Blanc, N, et al.
Veröffentlicht: (2007)

System verilog RTL modeling with embedded assertions /
von: Chow, Chee Siang, 1984-, et al.
Veröffentlicht: (2012)

Predicate abstraction of ANSI-C programs using SAT
von: Clarke, E, et al.
Veröffentlicht: (2004)

Predicate Abstraction of ANSI–C Programs using SAT
von: Clarke, E, et al.
Veröffentlicht: (2015)

Predicate Abstraction of ANSI-C Programs Using SAT.
von: Clarke, E, et al.
Veröffentlicht: (2004)

SATABS: SAT−based Predicate Abstraction for ANSI−C
von: Clarke, E, et al.
Veröffentlicht: (2005)

Predicate Abstraction of ANSI-C Programs Using SAT
von: Clarke, E, et al.
Veröffentlicht: (2004)

System verilog RTL modeling with embedded assertions[electronic resource] /
von: Chow, Chee Siang, 1984-, et al.
Veröffentlicht: (2012)

The RTL design of 32-bit RISC processor using verilog HDL /
von: Hafizul Hasni Manab, 1987-, et al.
Veröffentlicht: (2012)

Approximating Predicate Images for Bit−Vector Logic
von: Kroening, D, et al.
Veröffentlicht: (2006)

Hooray For Hollywood: Onomastic rechniques in Bentelntans' “Dirty Eddie”
von: Leonard R.N. Ashley
Veröffentlicht: (1988-12-01)

Verification of SpecC using Predicate Abstraction
von: Clarke, E, et al.
Veröffentlicht: (2007)

Verification of SpecC using predicate abstraction.
von: Clarke, E, et al.
Veröffentlicht: (2007)

The RTL design of 32-bit RISC processor using verilog HDL [electronic resource] /
von: Hafizul Hasni Manab, 1987-
Veröffentlicht: (2012)

Predicate Abstraction with Under-approximation Refinement
von: Corina S. Pasareanu, et al.
Veröffentlicht: (2007-02-01)

Counterexamples with Loops for Predicate Abstraction
von: Kroening, D, et al.
Veröffentlicht: (2006)

The RTL design of 32-BIT 5- stage pipeline risc processor using verilog HDL /
von: Lim, Jonie Joo Nee, 1978-, et al.
Veröffentlicht: (2008)

The RTL design of 32-BIT 5- stage pipeline risc processor using verilog HDL [electronic resources] /
von: Lim, Jonie Joo Nee, 1978-, et al.
Veröffentlicht: (2008)

Verification and Falsification of Programs with Loops Using Predicate Abstraction
von: Kroening, D, et al.
Veröffentlicht: (2009)

Verification and falsification of programs with loops using predicate abstraction.
von: Kroening, D, et al.
Veröffentlicht: (2010)

Model Checking with Abstraction for Web Services
von: Sharygina, N, et al.
Veröffentlicht: (2007)

V2c – A Verilog to C translator
von: Mukherjee, R, et al.
Veröffentlicht: (2016)

Strengthening properties using abstraction refinement
von: Purandare, M, et al.
Veröffentlicht: (2009)

RTL cookbook/
von: 274324 Lancaster, Don
Veröffentlicht: (1969)

RTL2RTL Formal Equivalence: Boosting the Design Confidence
von: M V Achutha Kiran Kumar, et al.
Veröffentlicht: (2014-07-01)

Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
von: Kroening, D, et al.
Veröffentlicht: (2003)

Counterexample Guided Abstraction Refinement via Program Execution
von: Groce, A, et al.
Veröffentlicht: (2004)

Automated scripts for testing verilog designs with iVerilog
von: Ng, Gary Jia Hao
Veröffentlicht: (2015)

RTL Conversion Method From Pipelined Synchronous RTL Models Into Asynchronous Ones
von: Shogo Semba, et al.
Veröffentlicht: (2022-01-01)

Counterexample-guided abstraction refinement for symmetric concurrent programs
von: Donaldson, A, et al.
Veröffentlicht: (2012)