diff --git a/User-Documentation.md b/User-Documentation.md
index 2e8b612..41af21f 100644
--- a/User-Documentation.md
+++ b/User-Documentation.md
@@ -5,9 +5,9 @@ The goal of this documentation is to enable smooth transition when using this DD
# Getting Started
-The recommended way to instantiate this IP is to use the top module [`rtl/ddr3_top.v`](https://github.com/AngeloJacobo/DDR3_Controller/blob/main/rtl/ddr3_top.v), a template for instantiation is also included in that file.
+The recommended way to instantiate this IP is to use the top module [`rtl/ddr3_top.v`](https://github.com/AngeloJacobo/DDR3_Controller/blob/main/rtl/ddr3_top.v), a template for instantiation is also included in that file. Steps to include this DDR3 memory controller IP is to instantiate design, create the constraint file, then edit the localparams.
-## Instantiate Design
+## :heavy_check_mark: Instantiate Design
The first thing to edit are the **top-level parameters**:
| Parameter | Function |
@@ -75,12 +75,12 @@ Next are the **DDR3 I/O ports**, these will be connected directly to the top-lev
Finally are the **debug ports**, these are connected to relevant registers containing information on current state of the controller. Trace each `o_debug_*` inside `ddr3_controller.v` to edit the registers to be monitored.
-## Create Constraint File
+## :heavy_check_mark: Create Constraint File
* One example of constraint file is from the [Kintex-7 Ethernet Switch Project](https://github.com/AngeloJacobo/DDR3_Controller/blob/main/kintex_switch_files/kluster.xdc#L227-L389) [[4]](https://github.com/AngeloJacobo/DDR3_Controller/wiki/User-Documentation#note) , highlighted are all the DDR3 pins. This constraint file assumes a dual-rank DDR3 RAM (thus 2 pairs of `o_ddr3_clk`, `o_ddr3_cke`, `o_ddr3_s_n`, and `o_ddr3_odt`) with 8 lanes of x8 DDR3 (thus 8 `o_ddr3_dm`, 8 `io_ddr3_dqs`, and 64 `io_ddr3_dq`). The constraint file also has [set_property](https://github.com/AngeloJacobo/DDR3_Controller/blob/main/kintex_switch_files/kluster.xdc#L453-L457) required for proper operation. The property `INTERNAL_VREF` must be set to half of the bank voltage (1.5V thus set to `0.75`). The property `BITSTREAM.STARTUP.MATCH_CYCLE` ([page 240 of UG628: Command Line Guide](https://docs.xilinx.com/v/u/en-US/devref)) is verified to work properly when value is set to `6`. Kintex-7 has HP bank where the DDR3 is connected thus allow the use of DCI (Digitally-Controlled Impedance) for impedance matching by using `SSTL15_T_DCI` type of `IOSTANDARD`.
* Another example of constraint file is for the [Arty-S7 project](https://github.com/AngeloJacobo/DDR3_Controller/blob/main/testbench/ARTY_S7/Arty-S7-50-Master.xdc#L87-L349), highlighted are the DDR3 pins. The Arty-S7 has x16 DDR3 and it works like two x8 (thus 2 `ddr3_dm`, 2 `ddr3_dqs`, and 16 `io_ddr3_dq`) [[1]](https://github.com/AngeloJacobo/DDR3_Controller/wiki/User-Documentation#note) . Arty-S7 only has HR bank where the DDR3 is connected, this restricts the design to use on-chip split-termination [(UG471 7-Series Select Guide page 33)](https://docs.xilinx.com/v/u/en-US/ug471_7Series_SelectIO) for impedance matching instead of DCI used in HP banks. `IN_TERM UNTUNED_SPLIT_50` signifies that the input termination is set to an untuned split termination of 50 ohms. The constraint file was easily created by retrieving the pin constraints generated by the Vivado Memory Interface Generator (MIG) together with the [`.prj` file](https://github.com/Digilent/vivado-boards/blob/master/new/board_files/arty-s7-50/B.0/mig.prj#L47-L96) provided by Digilent for Arty-S7. The generated `.xdc` file by the MIG can be located at `[vivado_proj].gen/sources_1/ip/mig_7series_0/mig_7series_0/user_design/constraints/mig_7series_0.xdc`
-## Edit Localparameters
+## :heavy_check_mark: Edit Localparams
The verilog file [`rtl/ddr3_controller`](https://github.com/AngeloJacobo/DDR3_Controller/blob/main/rtl/ddr3_controller.v) contains the timing parameters that needs to be configured by the user to align with the DDR3 device. User should base the timing values on _Chapter 13 Electrical Characteristics and AC Timing_ from [JEDEC DDR3 doc (page 169)](https://www.jedec.org/sites/default/files/docs/JESD79-3F.pdf). _The default values on the verilog file should generally work for DDR3-800_.
### Note:
@@ -92,22 +92,28 @@ The verilog file [`rtl/ddr3_controller`](https://github.com/AngeloJacobo/DDR3_Co
***
-# Compile and and Simulate Design
+# Lint and Formal Verification
The easiest way to compile, lint, and formally verify the design is to run [`./run_compile.sh`](https://github.com/AngeloJacobo/DDR3_Controller/blob/main/run_compile.sh) on the top-level directory. This will first run [Verilator](https://verilator.org/guide/latest/install.html) lint. Most likely this will show errors:
> %Error: rtl//ddr3_phy: Cannot find file containing module:
Disregard these errors as Verilator cannot access the verilog files for Xilinx-exclusive IPs. Other than this kind of error, there should be no other errors or warning.
-Next is compilation with [Yosys](https://github.com/YosysHQ/yosys), this will show warnings
+Next is compilation with [Yosys](https://github.com/YosysHQ/yosys), this will show warnings:
> Warning: Replacing memory ... with list of registers.
Disregards this kind of warning as it just converts small memory elements in the design into a series of register elements.
-After Yosys compilation is [Icarus Verilog](https://github.com/steveicarus/iverilog) compilation, this should not show any warning or errors but will display the `Test Functions` to verify that the verilog-functions return the correct values, and `Controller Parameters` to verify the top-level parameters are set properly. Delay values are also shown.
-
-Last is the [Symbiyosys Formal Verification](https://symbiyosys.readthedocs.io/en/latest/install.html), this will run the [`ddr3.sby`](https://github.com/AngeloJacobo/DDR3_Controller/blob/main/ddr3.sby). These will run multiple verification tasks and will take some time (running each task might take 10 mins or so). A summary is shown at the end where all task passed:
+After Yosys compilation is [Icarus Verilog](https://github.com/steveicarus/iverilog) compilation, this should not show any warning or errors but will display the `Test Functions` to verify that the verilog-functions return the correct values, and `Controller Parameters` to verify the top-level parameters are set properly. Delay values for some timing parameters are also shown.
+Last is the [Symbiyosys Formal Verification](https://symbiyosys.readthedocs.io/en/latest/install.html), this will run the [`ddr3.sby`](https://github.com/AngeloJacobo/DDR3_Controller/blob/main/ddr3.sby). These will run multiple verification tasks and will take some time (running each task might take 10 mins or so). A summary is shown at the end where all tasks passed:
+
+
+# Simulation
+Import all simulation files under [./testbench](https://github.com/AngeloJacobo/DDR3_Controller/tree/main/testbench) to Vivado then run simulation.
+
+# Sample Projects
+- The1