[fpv/doc] Add coding guidelines
Add coding guidelines in terms of where to place the assertions
Signed-off-by: Cindy Chen <chencindy@google.com>
diff --git a/hw/formal/README.md b/hw/formal/README.md
index 5522788..62308bc 100644
--- a/hw/formal/README.md
+++ b/hw/formal/README.md
@@ -311,6 +311,19 @@
$past(rv_plic.le[src_sel]) || $past(intr_src_i[src_sel]), clk_i, !rst_ni)
```
+## Implementation Guidelines
+The recommended guidelines for where to implement assertions are as follows:
+* Basic assertions should be implemented directly in the RTL file. These basic
+ functional assertions are often inserted by designers to act as a sanity
+ check.
+* Assertions used for the testbench to achieve verification goals should be
+ implemented under the `ip/hw/module_name/fpv/vip` folder. This FPV environment
+ can be automatically generated by the [`fpvgen.py` script](../../util/fpvgen/README.md).
+* Portable assertions written for common interfaces or submodules should also be
+ implemented under the `ip/hw/submodule_or_interface/fpv/vip` folder. These
+ portable assertion collections can be easily reused by other testbench via a
+ bind file.
+
## References
* [SVA Basics](https://www.systemverilog.io/sva-basics)
* [SVA Tutorial](https://www.doulos.com/knowhow/sysverilog/tutorial/assertions/)
