VL2SMV(1)                                                            VL2SMV(1)



[1mNAME[0m
       vl2smv - translator from Synchronous Verilog to SMV

[1mSYNOPSIS[0m
       [1mvl2smv file.v[0m

[1mDESCRIPTION[0m
       Translates  a  "Synchronous  Verilog" source file file.v to Cadence SMV
       source file file.smv.


[1mSYNTHESIZABLE VERILOG COMPATIBILITY[0m
       Synchronous Verilog does not contain the event based constructs of Ver-
       ilog, such as @(..). However, vl2smv does support inference of combina-
       tional logic and edge-sensitive storage devices as  specified  in  IEEE
       P1364.1/D1.6.

       For  example  here  is  a simple positive edge-triggered register, 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 combi-
       national logic.


[1mSINGLE AND MULTIPLE CLOCK DESIGNS[0m
       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 environment 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 nondeterministically (and thus are not guaranteed to tog-
       gle).


[1mSEE ALSO[0m
       [1msmv(1),[22mvw(1)
       [1mK.[22mL.[1mMcMillan,[22mThe SMV language
       [1mKenneth L. McMillan, [4m[22mSymbolic[24m [4mModel[24m [4mChecking,[24m [1mKluwer, 1993.[0m



[1mBUGS[0m
       You must be kidding.


[1mAUTHOR[0m
       Kenneth L. McMillan, Cadence Berkeley Labs
       mcmillan@cadence.com





VL2SMV                            23 Jan 1996                        VL2SMV(1)
