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

Полное описание

Библиографические подробности
Главные авторы:	Jain, H, Kroening, D, Sharygina, N, al., E
Формат:	Journal article
Опубликовано:	Institute of Electrical and Electronics Engineers 2008

Схожие документы

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
по: Jain, H, и др.
Опубликовано: (2008)

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
по: Jain, H, и др.
Опубликовано: (2005)

Word level predicate abstraction and refinement for verifying RTL verilog
по: Jain, H, и др.
Опубликовано: (2005)

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
по: Jain, H, и др.
Опубликовано: (2008)

Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs
по: Kroening, D, и др.
Опубликовано: (2007)

VCEGAR: Verilog CounterExample Guided Abstraction Refinement
по: Jain, H, и др.
Опубликовано: (2007)

Verification of SpecC and Verilog using Predicate Abstraction
по: Jain, H, и др.
Опубликовано: (2004)

Checking consistency of C and Verilog using predicate abstraction and induction
по: Kroening, D, и др.
Опубликовано: (2004)

Checking Consistency of C and Verilog using Predicate Abstraction and Induction
по: Kroening, D, и др.
Опубликовано: (2004)

Verifying C++ with STL Containers via Predicate Abstraction
по: Blanc, N, и др.
Опубликовано: (2007)

Verifying C++ with STL containers via predicate abstraction
по: Blanc, N, и др.
Опубликовано: (2007)

System verilog RTL modeling with embedded assertions /
по: Chow, Chee Siang, 1984-, и др.
Опубликовано: (2012)

Predicate abstraction of ANSI-C programs using SAT
по: Clarke, E, и др.
Опубликовано: (2004)

Predicate Abstraction of ANSI–C Programs using SAT
по: Clarke, E, и др.
Опубликовано: (2015)

Predicate Abstraction of ANSI-C Programs Using SAT.
по: Clarke, E, и др.
Опубликовано: (2004)

SATABS: SAT−based Predicate Abstraction for ANSI−C
по: Clarke, E, и др.
Опубликовано: (2005)

Predicate Abstraction of ANSI-C Programs Using SAT
по: Clarke, E, и др.
Опубликовано: (2004)

System verilog RTL modeling with embedded assertions[electronic resource] /
по: Chow, Chee Siang, 1984-, и др.
Опубликовано: (2012)

The RTL design of 32-bit RISC processor using verilog HDL /
по: Hafizul Hasni Manab, 1987-, и др.
Опубликовано: (2012)

Approximating Predicate Images for Bit−Vector Logic
по: Kroening, D, и др.
Опубликовано: (2006)

Hooray For Hollywood: Onomastic rechniques in Bentelntans' “Dirty Eddie”
по: Leonard R.N. Ashley
Опубликовано: (1988-12-01)

Verification of SpecC using Predicate Abstraction
по: Clarke, E, и др.
Опубликовано: (2007)

Verification of SpecC using predicate abstraction.
по: Clarke, E, и др.
Опубликовано: (2007)

The RTL design of 32-bit RISC processor using verilog HDL [electronic resource] /
по: Hafizul Hasni Manab, 1987-
Опубликовано: (2012)

Predicate Abstraction with Under-approximation Refinement
по: Corina S. Pasareanu, и др.
Опубликовано: (2007-02-01)

Counterexamples with Loops for Predicate Abstraction
по: Kroening, D, и др.
Опубликовано: (2006)

The RTL design of 32-BIT 5- stage pipeline risc processor using verilog HDL /
по: Lim, Jonie Joo Nee, 1978-, и др.
Опубликовано: (2008)

The RTL design of 32-BIT 5- stage pipeline risc processor using verilog HDL [electronic resources] /
по: Lim, Jonie Joo Nee, 1978-, и др.
Опубликовано: (2008)

Verification and Falsification of Programs with Loops Using Predicate Abstraction
по: Kroening, D, и др.
Опубликовано: (2009)

Verification and falsification of programs with loops using predicate abstraction.
по: Kroening, D, и др.
Опубликовано: (2010)

Model Checking with Abstraction for Web Services
по: Sharygina, N, и др.
Опубликовано: (2007)

V2c – A Verilog to C translator
по: Mukherjee, R, и др.
Опубликовано: (2016)

Strengthening properties using abstraction refinement
по: Purandare, M, и др.
Опубликовано: (2009)

RTL cookbook/
по: 274324 Lancaster, Don
Опубликовано: (1969)

RTL2RTL Formal Equivalence: Boosting the Design Confidence
по: M V Achutha Kiran Kumar, и др.
Опубликовано: (2014-07-01)

Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
по: Kroening, D, и др.
Опубликовано: (2003)

Counterexample Guided Abstraction Refinement via Program Execution
по: Groce, A, и др.
Опубликовано: (2004)

Automated scripts for testing verilog designs with iVerilog
по: Ng, Gary Jia Hao
Опубликовано: (2015)

RTL Conversion Method From Pipelined Synchronous RTL Models Into Asynchronous Ones
по: Shogo Semba, и др.
Опубликовано: (2022-01-01)

Counterexample-guided abstraction refinement for symmetric concurrent programs
по: Donaldson, A, и др.
Опубликовано: (2012)