docs: update README and README.zh-CN

README.md

@@ -23,6 +23,7 @@ Read more detailed Chinese README: [中文说明](README.zh-CN.md).
   - [TLB](#tlb)
   - [Memory Access](#memory-access)
 - [Verification Example](#verification-example)
+- [Publications](#publications)
 
 ## Usage
 
@@ -132,6 +133,6 @@ And then perform formal verification using BMC through ChiselTest.
 
 ## Publications
 
-**SETTA 2024: Formal Verification of RISC-V Processor Chisel Designs** [Link](https://link.springer.com/chapter/10.1007/978-981-96-0602-3_8) | [BibTex](https://citation-needed.springer.com/v2/references/10.1007/978-981-96-0602-3_8?format=bibtex&flavour=citation)
+If our work has been helpful to you, please cite:
 
-Chisel is an open-source high-level hardware construction language embedded in Scala to facilitate parameterizable, reusable circuit design generators. It is becoming increasingly popular and has been used to design many RISC-V processor variants. Formal verification has been adapted to check the (functional) correctness of RISC-V processor designs. However, the RISC-V instructions therein are specified in the low-level hardware languages Verilog/SystemVerilog, which are challenging to develop, maintain, and extend. This considerably lowers the advantage of RISC-V for designing highly customizable processors. In this work, we present the first end-to-end approach for formally verifying the correctness of RISC-V processor designs, fully at the Chisel high-level. Specifically, by utilizing the object-oriented and functional programming constructs offered by Chisel, we develop a high-level reference model of RISC-V instructions in Chisel. This reference model is a succinct, modular, and parameterized RISC-V processor design generator, thus can produce customized RISC-V processor variants. 
+**SETTA 2024: Formal Verification of RISC-V Processor Chisel Designs** [Link](https://link.springer.com/chapter/10.1007/978-981-96-0602-3_8) | [BibTex](https://citation-needed.springer.com/v2/references/10.1007/978-981-96-0602-3_8?format=bibtex&flavour=citation)

README.zh-CN.md

@@ -26,6 +26,7 @@
 - [使用建议](#使用建议)
   - [使用 GitHub Actions 进行验证](#使用-github-actions-进行验证)
 - [验证实例](#验证实例)
+- [出版物](#出版物)
 
 ## 安装
 
@@ -345,3 +346,9 @@ GitHub Actions 可以在每次 push 代码到 GitHub 的时候自动运行验证
 该项目是在 [NutShell](https://github.com/OSCPU/NutShell) 上进行验证的例子。
 我们修改了 NutShell 代码以获取验证所需的处理器信息，并与参考模型进行了同步。
 最终通过 [ChiselTest](https://github.com/ucb-bar/chiseltest) 提供的接口调用了 BMC 算法进行验证。
+
+## 出版物
+
+如果我们的工作对您有帮助，请引用：
+
+**SETTA 2024: Formal Verification of RISC-V Processor Chisel Designs** [Link](https://link.springer.com/chapter/10.1007/978-981-96-0602-3_8) | [BibTex](https://citation-needed.springer.com/v2/references/10.1007/978-981-96-0602-3_8?format=bibtex&flavour=citation)