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

Bibliografiset tiedot
Päätekijät:	Jain, H, Kroening, D, Sharygina, N, al., E
Aineistotyyppi:	Journal article
Julkaistu:	Institute of Electrical and Electronics Engineers 2008

Samankaltaisia teoksia

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

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

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

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

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

VCEGAR: Verilog CounterExample Guided Abstraction Refinement
Tekijä: Jain, H, et al.
Julkaistu: (2007)

Verification of SpecC and Verilog using Predicate Abstraction
Tekijä: Jain, H, et al.
Julkaistu: (2004)

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

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

Verifying C++ with STL Containers via Predicate Abstraction
Tekijä: Blanc, N, et al.
Julkaistu: (2007)

Verifying C++ with STL containers via predicate abstraction
Tekijä: Blanc, N, et al.
Julkaistu: (2007)

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

Predicate abstraction of ANSI-C programs using SAT
Tekijä: Clarke, E, et al.
Julkaistu: (2004)

Predicate Abstraction of ANSI–C Programs using SAT
Tekijä: Clarke, E, et al.
Julkaistu: (2015)

Predicate Abstraction of ANSI-C Programs Using SAT.
Tekijä: Clarke, E, et al.
Julkaistu: (2004)

SATABS: SAT−based Predicate Abstraction for ANSI−C
Tekijä: Clarke, E, et al.
Julkaistu: (2005)

Predicate Abstraction of ANSI-C Programs Using SAT
Tekijä: Clarke, E, et al.
Julkaistu: (2004)

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

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

Approximating Predicate Images for Bit−Vector Logic
Tekijä: Kroening, D, et al.
Julkaistu: (2006)

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

Verification of SpecC using Predicate Abstraction
Tekijä: Clarke, E, et al.
Julkaistu: (2007)

Verification of SpecC using predicate abstraction.
Tekijä: Clarke, E, et al.
Julkaistu: (2007)

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

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

Counterexamples with Loops for Predicate Abstraction
Tekijä: Kroening, D, et al.
Julkaistu: (2006)

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

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

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

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

Model Checking with Abstraction for Web Services
Tekijä: Sharygina, N, et al.
Julkaistu: (2007)

V2c – A Verilog to C translator
Tekijä: Mukherjee, R, et al.
Julkaistu: (2016)

Strengthening properties using abstraction refinement
Tekijä: Purandare, M, et al.
Julkaistu: (2009)

RTL cookbook/
Tekijä: 274324 Lancaster, Don
Julkaistu: (1969)

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

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

Counterexample Guided Abstraction Refinement via Program Execution
Tekijä: Groce, A, et al.
Julkaistu: (2004)

Automated scripts for testing verilog designs with iVerilog
Tekijä: Ng, Gary Jia Hao
Julkaistu: (2015)

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

Counterexample-guided abstraction refinement for symmetric concurrent programs
Tekijä: Donaldson, A, et al.
Julkaistu: (2012)