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

Mô tả đầy đủ

Chi tiết về thư mục
Những tác giả chính:	Jain, H, Kroening, D, Sharygina, N, al., E
Định dạng:	Journal article
Được phát hành:	Institute of Electrical and Electronics Engineers 2008

Những quyển sách tương tự

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
Bằng: Jain, H, et al.
Được phát hành: (2008)

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
Bằng: Jain, H, et al.
Được phát hành: (2005)

Word level predicate abstraction and refinement for verifying RTL verilog
Bằng: Jain, H, et al.
Được phát hành: (2005)

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
Bằng: Jain, H, et al.
Được phát hành: (2008)

Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs
Bằng: Kroening, D, et al.
Được phát hành: (2007)

VCEGAR: Verilog CounterExample Guided Abstraction Refinement
Bằng: Jain, H, et al.
Được phát hành: (2007)

Verification of SpecC and Verilog using Predicate Abstraction
Bằng: Jain, H, et al.
Được phát hành: (2004)

Checking consistency of C and Verilog using predicate abstraction and induction
Bằng: Kroening, D, et al.
Được phát hành: (2004)

Checking Consistency of C and Verilog using Predicate Abstraction and Induction
Bằng: Kroening, D, et al.
Được phát hành: (2004)

Verifying C++ with STL Containers via Predicate Abstraction
Bằng: Blanc, N, et al.
Được phát hành: (2007)

Verifying C++ with STL containers via predicate abstraction
Bằng: Blanc, N, et al.
Được phát hành: (2007)

System verilog RTL modeling with embedded assertions /
Bằng: Chow, Chee Siang, 1984-, et al.
Được phát hành: (2012)

Predicate abstraction of ANSI-C programs using SAT
Bằng: Clarke, E, et al.
Được phát hành: (2004)

Predicate Abstraction of ANSI–C Programs using SAT
Bằng: Clarke, E, et al.
Được phát hành: (2015)

Predicate Abstraction of ANSI-C Programs Using SAT.
Bằng: Clarke, E, et al.
Được phát hành: (2004)

SATABS: SAT−based Predicate Abstraction for ANSI−C
Bằng: Clarke, E, et al.
Được phát hành: (2005)

Predicate Abstraction of ANSI-C Programs Using SAT
Bằng: Clarke, E, et al.
Được phát hành: (2004)

System verilog RTL modeling with embedded assertions[electronic resource] /
Bằng: Chow, Chee Siang, 1984-, et al.
Được phát hành: (2012)

The RTL design of 32-bit RISC processor using verilog HDL /
Bằng: Hafizul Hasni Manab, 1987-, et al.
Được phát hành: (2012)

Approximating Predicate Images for Bit−Vector Logic
Bằng: Kroening, D, et al.
Được phát hành: (2006)

Hooray For Hollywood: Onomastic rechniques in Bentelntans' “Dirty Eddie”
Bằng: Leonard R.N. Ashley
Được phát hành: (1988-12-01)

Verification of SpecC using Predicate Abstraction
Bằng: Clarke, E, et al.
Được phát hành: (2007)

Verification of SpecC using predicate abstraction.
Bằng: Clarke, E, et al.
Được phát hành: (2007)

The RTL design of 32-bit RISC processor using verilog HDL [electronic resource] /
Bằng: Hafizul Hasni Manab, 1987-
Được phát hành: (2012)

Predicate Abstraction with Under-approximation Refinement
Bằng: Corina S. Pasareanu, et al.
Được phát hành: (2007-02-01)

Counterexamples with Loops for Predicate Abstraction
Bằng: Kroening, D, et al.
Được phát hành: (2006)

The RTL design of 32-BIT 5- stage pipeline risc processor using verilog HDL /
Bằng: Lim, Jonie Joo Nee, 1978-, et al.
Được phát hành: (2008)

The RTL design of 32-BIT 5- stage pipeline risc processor using verilog HDL [electronic resources] /
Bằng: Lim, Jonie Joo Nee, 1978-, et al.
Được phát hành: (2008)

Verification and Falsification of Programs with Loops Using Predicate Abstraction
Bằng: Kroening, D, et al.
Được phát hành: (2009)

Verification and falsification of programs with loops using predicate abstraction.
Bằng: Kroening, D, et al.
Được phát hành: (2010)

Model Checking with Abstraction for Web Services
Bằng: Sharygina, N, et al.
Được phát hành: (2007)

V2c – A Verilog to C translator
Bằng: Mukherjee, R, et al.
Được phát hành: (2016)

Strengthening properties using abstraction refinement
Bằng: Purandare, M, et al.
Được phát hành: (2009)

RTL cookbook/
Bằng: 274324 Lancaster, Don
Được phát hành: (1969)

RTL2RTL Formal Equivalence: Boosting the Design Confidence
Bằng: M V Achutha Kiran Kumar, et al.
Được phát hành: (2014-07-01)

Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
Bằng: Kroening, D, et al.
Được phát hành: (2003)

Counterexample Guided Abstraction Refinement via Program Execution
Bằng: Groce, A, et al.
Được phát hành: (2004)

Automated scripts for testing verilog designs with iVerilog
Bằng: Ng, Gary Jia Hao
Được phát hành: (2015)

RTL Conversion Method From Pipelined Synchronous RTL Models Into Asynchronous Ones
Bằng: Shogo Semba, et al.
Được phát hành: (2022-01-01)

Counterexample-guided abstraction refinement for symmetric concurrent programs
Bằng: Donaldson, A, et al.
Được phát hành: (2012)