verilog-c

ANSI-C benchmarks generated from Verilog RTL circuits with safety assertions. Used for Formal Property Verification. If you are using the benchmarks, please refer to the following papers for the translation details from Verilog RTL to C programs.

@inproceedings{mkm2015,
  AUTHOR    = { Mukherjee, Rajdeep
                and Kroening, Daniel
                and Melham, Tom },
  TITLE     = { Hardware Verification using Software Analyzers },
  BOOKTITLE = { IEEE Computer Society Annual Symposium on VLSI },
  YEAR      = { 2015 },
  PUBLISHER = { IEEE },
  PAGES     = { 7--12 },
  ISBN      = { 978-1-4799-8719-1 },
}

@inproceedings{mtk2016,
  AUTHOR    = { Mukherjee, Rajdeep
                and Tautschnig, Michael
                and Kroening, Daniel },
  TITLE     = { v2c -- A {Verilog} to {C} Translator Tool },
  BOOKTITLE = { Tools and Algorithms for the Construction and Analysis of Systems (TACAS) },
  YEAR      = { 2016 },
  PUBLISHER = { Springer },
  PAGES     = { 580--586 },
  ISBN      = { 978-3-662-49673-2 },
  SERIES    = { LNCS },
  VOLUME    = { 9636 },
}

@inproceedings{mskm2016,
  AUTHOR    = { Mukherjee, Rajdeep
                and Schrammel, Peter
                and Kroening, Daniel
                and Melham, Tom },
  TITLE     = { Unbounded Safety Verification for Hardware Using Software Analyzers },
  BOOKTITLE = { Design, Automation and Test in Europe (DATE) },
  YEAR      = { 2016 },
  PUBLISHER = { IEEE },
  PAGES     = { 1152--1155 },
  ISBN      = { 978-3-9815-3707-9 },
}