diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex
index 671fabb816b..17689c141aa 100644
--- a/manual/command-reference-manual.tex
+++ b/manual/command-reference-manual.tex
@@ -902,6 +902,11 @@ \section{clk2fflogic -- convert clocked FFs to generic \$ff cells}
 This command replaces clocked flip-flops with generic $ff cells that use the
 implicit global clock. This is useful for formal verification of designs with
 multiple clocks.
+
+This pass assumes negative hold time for the async FF inputs. For example when
+a reset deasserts with the clock edge, then the FF output will still drive the
+reset value in the next cycle regardless of the data-in value at the time of
+the clock edge.
 \end{lstlisting}
 
 \section{clkbufmap -- insert clock buffers on clock networks}
@@ -1554,12 +1559,17 @@ \section{equiv\_opt -- prove equivalence for optimized circuit}
     -undef
         enable modelling of undef states during equiv_induct.
 
+    -nocheck
+        disable running check before and after the command under test.
+
 The following commands are executed by this verification command:
 
     run_pass:
         hierarchy -auto-top
         design -save preopt
+        check -assert    (unless -nocheck)
         [command]
+        check -assert    (unless -nocheck)
         design -stash postopt
 
     prepare:
@@ -3122,6 +3132,12 @@ \section{miter -- automatically create a miter circuit}
         call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.
 
 
+    -cross
+        allow output ports on the gold module to match input ports on the
+        gate module. This is useful when the gold module contains additional
+        logic to drive some of the gate module inputs.
+
+
     miter -assert [options] module [miter_name]
 
 Creates a miter circuit for property checking. All input ports are kept,
@@ -3989,6 +4005,19 @@ \section{read -- load HDL designs}
 Load the specified VHDL files. (Requires Verific.)
 
 
+    read {-edif} <edif-file>..
+
+Load the specified EDIF files. (Requires Verific.)
+
+
+    read {-liberty} <liberty-file>..
+
+Load the specified Liberty files.
+
+    -lib
+        only create empty blackbox modules
+
+
     read {-f|-F} <command-file>
 
 Load and execute the specified command file. (Requires Verific.)
@@ -7926,6 +7955,20 @@ \section{verific -- load Verilog and VHDL designs using Verific}
 Load the specified VHDL files into Verific.
 
 
+    verific {-edif} <edif-file>..
+
+Load the specified EDIF files into Verific.
+
+
+    verific {-liberty} <liberty-file>..
+
+Load the specified Liberty files into Verific.
+Default library when -work is not present is one specified in liberty file.
+To use from SystemVerilog or VHDL use -L to specify liberty library.
+    -lib
+        only create empty blackbox modules
+
+
     verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|
                      -sv2012|-sv|-formal] <command-file>
 
@@ -8032,6 +8075,10 @@ \section{verific -- load Verilog and VHDL designs using Verific}
   -fullinit
     Keep all register initializations, even those for non-FF registers.
 
+  -cells
+    Import all cell definitions from Verific loaded libraries even if they are
+    unused in design. Useful with "-edif" and "-liberty" option.
+
   -chparam name value 
     Elaborate the specified top modules (all modules when -all given) using
     this parameter value. Modules on which this parameter does not exist will