Abstracting Verilog Designs to the Term-Level for Verification with UCLID
This page illustrates how to use v2ucl, the tool for abstracting Verilog to UCLID, described in the paper available below. To see the demo, first download the demo and the appropriate version of v2ucl below. For your convenience, there is a link to a copy of the paper and graphs which compare our novel hybrid BV/Term-Level models against pure BV models.
32-bit Linux binary: v2ucl
64-bit Linux binary: v2ucl
Demo files: tgz
BV/Hybrid runtimes for varying flits/packet: eps pdf
BV/Hybrid runtime and problem size ratios: eps pdf