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)