PV2 v2ctranslates a Register Transfer Level hardware circuit description into a C program

Verilog to C translator

Application domain/field

Type of tool

Translator

Expected input

Register Transfer Level (RTL) description of a hardware circuit

Format:

Verilog Hardware Description Language

Expected output

C program, also called a software netlist.

Internals

By translating a hardware circuit into a C program, allows you to use software verification techniques such as abstract interpretation and symbolic execution.
Hardware

Links

Project page: https://www.cprover.org/hardware/v2c/

Related papers

https://doi.org/10.1007/978-3-662-49674-9_38 (TACAS '16)

Last publication date

9 April 2016

Related tools

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.