A Few Pointers

A Few Pointers

  • Make sure your CTL formulae refer to the Blifmv variable names (These are not the same as Verilog names).
  • Use the ordering file provided.
  • Remember that latched variables are output at the next clock cycle, but wires are output immediately.
  • Keep in mind your property may be wrongly formulated.

Previous slide Back to the first slide View Graphic Version

Contact 
©2002-2018 U.C. Regents