VL2SMV(1)                                               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.


SYNTHESIZABLE VERILOG COMPATIBILITY
       Synchronous Verilog does not contain the event based  con-
       structs  of  Verilog,  such as @(..). However, vl2smv does
       support inference of combinational logic  and  edge-sensi-
       tive storage devices as specified in IEEE P1364.1/D1.6.

       For  example here is a simple positive edge-triggered reg-
       ister, with input y and output x:

       always @(posedge clk)
         x <= y;

       Here is a positive edge-triggered register with active-low
       asynchronous reset:

       always @(posedge clk or negedge rst)
         if(!rst)
           x <= 0;
         else
           x <= y;

       Note  that  even  if  x is declared as a wire in the above
       examples, it will be treated as a register.

       Here is an example of inferred combinational logic:

       always @(x or y or z)
         a = (x | y) & z;

       Vl2smv does not  recognize  inferred  latches.  These  are
       treated as combinational logic.


SINGLE AND MULTIPLE CLOCK DESIGNS
       By default, Vl2smv assumes that all inferred registers are
       triggered on the same edge of the same  clock  signal.  It
       then  "extracts"  the clock, meaning that each step of the
       resulting SMV model corresponds to one full cycle  of  the
       clock.  For  single-clocked designs this generally results
       in improved verification efficiency, and has the advantage
       that  the  "next time" operator X has the interpration "at
       the next clock edge".  A side-effect of  clock  extraction
       is  that asynchronous resets become synchronous, since all
       state transitions correspond to clock edges.

       For multple clock designs, the user must set the  environ-
       ment  variable  VL2SMV_MULTI_CLOCK.  In  this  case, clock
       extraction will not occur, and both phases  of  the  clock
       signal  will be apparent in the SMV model.  Care should be
       taken in writing temporal properties in this  mode,  since
       the  X  operator  does  not mean "at the next clock edge".
       Also, note that if the clock signals  are  not  explicitly
       driven, they will be allow to rise and fall nondeterminis-
       tically (and thus are not guaranteed to toggle).


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                     23 Jan 1996                          1