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 Description: pdf BV/Hybrid runtimes for varying flits/packet: eps pdf BV/Hybrid runtime and problem size ratios: eps pdf