Index: vis_dev/vis-2.3/src/bmc/bmcCmd.c
===================================================================
--- vis_dev/vis-2.3/src/bmc/bmcCmd.c	(revision 102)
+++ vis_dev/vis-2.3/src/bmc/bmcCmd.c	(revision 103)
@@ -1270,4 +1270,39 @@
 #endif
 
+/**Function********************************************************************
+
+  Synopsis    [write_cnf]
+
+  Description []
+  
+  CommandName [write_cnf]
+
+  CommandSynopsis [Generate the CNF form of a design]
+
+  CommandArguments [\[-h\] \[-f <ltl_filename>\] 
+		    \[-o <out_filename;\] 
+		    \[-k <number of steps;\] 
+		    
+
+  CommandDescription [Generate the CNF form of the network and the ltl specification if mentionned.
+  <p>
+  <dt> -o  <code>&lt;output_filename&gt;</code>
+  <dd> Specify the output filename to save the satisfying assignments and 
+  the statistics of SAT solving.
+  <p>
+  <dt> -f  <code>&lt;ltl_filename&gt;</code>
+  <dd> Specify the ltl filename that will be generate with.
+  <p>
+  <dt> -k  <code>&lt;value;</code>
+  <dd> Specify the number of step unrolled (by default = 0)
+  <p>
+
+  ]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
 
 int CommandWriteCnf(Hrc_Manager_t ** hmgr, int argc, char ** argv)