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

Deskribapen osoa

Xehetasun bibliografikoak
Egile Nagusiak:	Jain, H, Kroening, D, Sharygina, N, al., E
Formatua:	Journal article
Argitaratua:	Institute of Electrical and Electronics Engineers 2008

Antzeko izenburuak

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
nork: Jain, H, et al.
Argitaratua: (2008)

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
nork: Jain, H, et al.
Argitaratua: (2005)

Word level predicate abstraction and refinement for verifying RTL verilog
nork: Jain, H, et al.
Argitaratua: (2005)

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
nork: Jain, H, et al.
Argitaratua: (2008)

Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs
nork: Kroening, D, et al.
Argitaratua: (2007)

VCEGAR: Verilog CounterExample Guided Abstraction Refinement
nork: Jain, H, et al.
Argitaratua: (2007)

Verification of SpecC and Verilog using Predicate Abstraction
nork: Jain, H, et al.
Argitaratua: (2004)

Checking consistency of C and Verilog using predicate abstraction and induction
nork: Kroening, D, et al.
Argitaratua: (2004)

Checking Consistency of C and Verilog using Predicate Abstraction and Induction
nork: Kroening, D, et al.
Argitaratua: (2004)

Verifying C++ with STL Containers via Predicate Abstraction
nork: Blanc, N, et al.
Argitaratua: (2007)

Verifying C++ with STL containers via predicate abstraction
nork: Blanc, N, et al.
Argitaratua: (2007)

System verilog RTL modeling with embedded assertions /
nork: Chow, Chee Siang, 1984-, et al.
Argitaratua: (2012)

Predicate abstraction of ANSI-C programs using SAT
nork: Clarke, E, et al.
Argitaratua: (2004)

Predicate Abstraction of ANSI–C Programs using SAT
nork: Clarke, E, et al.
Argitaratua: (2015)

Predicate Abstraction of ANSI-C Programs Using SAT.
nork: Clarke, E, et al.
Argitaratua: (2004)

SATABS: SAT−based Predicate Abstraction for ANSI−C
nork: Clarke, E, et al.
Argitaratua: (2005)

Predicate Abstraction of ANSI-C Programs Using SAT
nork: Clarke, E, et al.
Argitaratua: (2004)

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

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

Approximating Predicate Images for Bit−Vector Logic
nork: Kroening, D, et al.
Argitaratua: (2006)

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

Verification of SpecC using Predicate Abstraction
nork: Clarke, E, et al.
Argitaratua: (2007)

Verification of SpecC using predicate abstraction.
nork: Clarke, E, et al.
Argitaratua: (2007)

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

Predicate Abstraction with Under-approximation Refinement
nork: Corina S. Pasareanu, et al.
Argitaratua: (2007-02-01)

Counterexamples with Loops for Predicate Abstraction
nork: Kroening, D, et al.
Argitaratua: (2006)

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

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

Verification and Falsification of Programs with Loops Using Predicate Abstraction
nork: Kroening, D, et al.
Argitaratua: (2009)

Verification and falsification of programs with loops using predicate abstraction.
nork: Kroening, D, et al.
Argitaratua: (2010)

Model Checking with Abstraction for Web Services
nork: Sharygina, N, et al.
Argitaratua: (2007)

V2c – A Verilog to C translator
nork: Mukherjee, R, et al.
Argitaratua: (2016)

Strengthening properties using abstraction refinement
nork: Purandare, M, et al.
Argitaratua: (2009)

RTL cookbook/
nork: 274324 Lancaster, Don
Argitaratua: (1969)

RTL2RTL Formal Equivalence: Boosting the Design Confidence
nork: M V Achutha Kiran Kumar, et al.
Argitaratua: (2014-07-01)

Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
nork: Kroening, D, et al.
Argitaratua: (2003)

Counterexample Guided Abstraction Refinement via Program Execution
nork: Groce, A, et al.
Argitaratua: (2004)

Automated scripts for testing verilog designs with iVerilog
nork: Ng, Gary Jia Hao
Argitaratua: (2015)

RTL Conversion Method From Pipelined Synchronous RTL Models Into Asynchronous Ones
nork: Shogo Semba, et al.
Argitaratua: (2022-01-01)

Counterexample-guided abstraction refinement for symmetric concurrent programs
nork: Donaldson, A, et al.
Argitaratua: (2012)