VL2SMV(1)                 User Commands                 VL2SMV(1)

NAME
     vl2smv - translator from Synchronous Verilog to SMV

SYNOPSIS
     vl2smv file.v

DESCRIPTION
     Translates a "Synchronous Verilog"  source  file  file.v  to
     Cadence SMV source file file.smv.


VERILOG COMPATIBILITY
     Synchronous Verilog does not contain the  event  based  con-
     structs of Verilog, such as @(..). However, Vl2smv does sup-
     port some limited use of these constructs, in the  following
     way:

     Consider a block of the following form:

     always @(...sensitivity list...)
       begin ...statements... end

     If  the  "sensitivity  list"  contains  any  occurrences  of
     "posedge" or "negedge", then all signals assigned in "state-
     ments" are treated as registers, even if they  are  declared
     as wires.

     On the other hand, if the  "sensitivity  list"  contains  no
     occurrences  of  "posedge"  or  "negedge",  then all signals
     assigned in "statements" are treated as wires, even if  they
     are declared as registers.

     This gives agreement with Verilog in most  cases  where  you
     have only one clock signal and use only one clock edge. How-
     ever, your mileage may vary. If  you  need  to  translate  a
     design with a more complex clocking scheme, use vv.


SEE ALSO
     smv(1),vw(1)
     K.L.McMillan,The SMV language
     Kenneth L. McMillan, Symbolic Model Checking, Kluwer, 1993.



BUGS
     You must be kidding.


AUTHOR
     Kenneth L. McMillan, Cadence Berkeley Labs
     mcmillan@cadence.com

VL2SMV              Last change: 23 Jan 1996                    2