使用 SymbiYosys 进行验证 Yosys 是一个开源的 Verilog HDL 综合工具包。它支持将电路的状态转换编码为 SMT-LIBv2 中的函数。由此出发，可以对电路进行一系列形式化验证。注意本文仅对相关工具的一般使用方法进行介绍，不涉及验证原理、算法分析等内容。本文讨论的内容均为 Assertion Based Verification (ABV)，除此之外 Yosys 还支持 Symbolic Model Checking、Formal Equivalence Checking，相关用法有待进一步整理。Motivating Exampletest.v 定义了一个简单的时序逻辑电路（此示例电路来自 Yosys Command Reference Manual），它只有输出，没有输入。它的输出可以理解为一个数列 yn+1=or(shl(yn),neg(yn))，首项 y0 的值是电路的初始状态。module test(input clk, output reg [3:0] y); always @(posedge clk) y <= (y << 1) | ^y; endmodule我们的目标是验证输出 y 的值不可能从一个非零值变为一个零值。为了验证该性质，需要将其写为 SMT-LIBv2 表达式，交给 SMT solver 求解。因此，首先需要明白编码电路的方式。使用以下综合脚本（synthesis script）test.ys 指示 Yosys 对电路进行变换，得到 test.smt2 文件。# Read Verilog source file and convert to internal representation .read_verilog test.v # Elaborate the design hierarchy. # Should always be the first command after reading the design. hierarchy -check -top test # Convert “processes” (the internal representation of behavioral Verilog code) # into multiplexers and registers .proc # Perform some basic optimizations and cleanups .opt # Check for obvious problems in the design .check -assert # Write a SMT-LIBv2 description of the current design .write_smt2 test.smt2理解 synthesis script以上脚本包含了3种类型的指令：Frontends：从文件中读取输入（一般为 Verilog 代码）Passes：在电路上应用等价变换Backends：将处理后的电路输出到文件（支持不同的格式，如 Verilog, BLIF, EDIF, SPICE, BTOR 等）这也是所有典型的 Yosys synthesis script 都具有的结构，由此可见综合的过程与编译的过程非常相似。事实上，Yosys 定义了一种电路的中间表示格式 RTLIL (RTL Intermediate Language)，所有的 Passes 都是在以此 IR 表示的抽象语法树（AST）上实现的。1 $ yosys test.ysYosys 输出的文件如下。此文件中定义了一个对应电路状态的类型 |_s|；电路中的输入（input）、输出（output）、寄存器（register）、线路（wire）都有各自对应的函数，这些函数名为 |_n |，它们接受一个电路状态作为输入，返回 Bool 类型或 BitVec 类型，对应具体的值。另外一个重要的函数为 |_t|，它接受两个状态 state, next_state 作为输入，当两者之间存在状态转换关系时，则返回 True，反之则返回 False。它们组合起来编码了电路的行为。SMT-LIBv2 description generated by Yosys 0.21+7 (git sha1 d98738db5, clang 10.0.0-4ubuntu1 -fPIC -Os); yosys-smt2-module test(declare-sort |test_s| 0)(declare-fun |test_is| (|test_s|) Bool)(declare-fun |test#0| (|test_s|) Bool) ; \clk; yosys-smt2-input clk 1; yosys-smt2-clock clk posedge; yosys-smt2-witness {"offset": 0, "path": ["\clk"], "smtname": "clk", "type": "posedge", "width": 1}; yosys-smt2-witness {"offset": 0, "path": ["\clk"], "smtname": "clk", "type": "input", "width": 1}(define-fun |test_n clk| ((state |test_s|)) Bool (|test#0| state)); yosys-smt2-witness {"offset": 0, "path": ["\y"], "smtname": 1, "type": "reg", "width": 4}(declare-fun |test#1| (|test_s|) (_ BitVec 4)) ; \y; yosys-smt2-output y 4;yosys-smt2-register y 4(define-fun |test_n y| ((state |test_s|)) (_ BitVec 4) (|test#1| state))(define-fun |test#2| ((state |test_s|)) Bool (xor (= ((_ extract 0 0) (|test#1| state)) #b1) (= ((_ extract 1 1) (|test#1| state)) #b1) (= ((_ extract 2 2) (|test#1| state)) #b1) (= ((_ extract 3 3) (|test#1| state)) #b1))) ; $reduce_xor $test.v:3$3_Y(define-fun |test#3| ((state |test_s|)) (_ BitVec 4) (bvor (concat ((_ extract 2 0) (|test#1| state)) #b0) (concat #b000 (ite (|test#2| state) #b1 #b0)))) ; $0\y3:0) Bool true)(define-fun |test_u| ((state |test_s|)) Bool true)(define-fun |test_i| ((state |test_s|)) Bool true)(define-fun |test_h| ((state |test_s|)) Bool true)(define-fun |test_t| ((state |test_s|) (next_state |test_s|)) Bool (= (|test#3| state) (|test#1| next_state)) ; $procdff$5 \y) ; end of module test; yosys-smt2-topmod test; end of yosys output现在，为了表示上述性质，可以定义两个状态 s1, s2，它们满足：1.s1 到 s2 存在状态转换关系2.s1 中 y != 03.s2 中 y == 0之后交给 SMT solver 验证其可满足性，若不能满足，则验证了不存在这样的情况。 we need QF_UFBV for this proof(set-logic QF_UFBV); insert the auto-generated code here%%; declare two state variables s1 and s2(declare-fun s1 () test_s)(declare-fun s2 () test_s); state s2 is the successor of state s1(assert (test_t s1 s2)); we are looking for a model with y non-zero in s1(assert (distinct (|test_n y| s1) #b0000)); we are looking for a model with y zero in s2(assert (= (|test_n y| s2) #b0000)); is there such a model?(check-sat)将上面的 test.ys 最后一行修改为：1 write_smt2 -tpl test.tpl test.smt2新的输出文件中包含了模版文件 test.tpl 的内容，并将其中的 %% 替换为了原本 write_smt2 命令的输出，可以将它作为 SMT solver 的输入。例如，调用 z3 进行求解，得到 unsat 的结果。12 $ z3 test.smt2unsat使用 SymbiYosys 进行验证上一节介绍的方法需要用户理解 write_smt2 命令的输出，并直接使用其中定义的函数，才能将需要验证的性质编写为 SMT-LIBv2 格式的表达式，这样不免有些繁琐。Yosys 还提供了 SymbiYosys (sby) 工具，它可以理解为一个前端驱动程序（front-end driver program），支持解析用户在源文件中定义的断言（assertions），直接尝试进行证明。来看另一个例子，下面是用 System Verilog 定义的一个计数器（此示例代码来自参考资料中 Formal Verification of RISC-V cores with riscv-formal 这一幻灯片的第3~4页）。module hello ( input clk, rst, output [3:0] cnt); reg [3:0] cnt = 0; always @(posedge clk) begin if (rst) cnt <= 0; else cnt <= cnt + 1; endendmodule现在来定义此电路需要满足的性质。首先用1个 assume 语句表明验证的前提（也就是在求解器考虑的所有情形中，此性质都得到满足）；assert 语句则是求解器需要证明的性质。module hello (/* ... */);/* ... */ `ifdef FORMAL always @* assume (cnt != 10); always @* assert (cnt != 15); `endif endmoduleSymbiYosys 使用一个 .sby 文件来描述验证过程中执行的任务，文件中包含若干个节（section），每个节由方括号括起的小标题表示。下面的文件中，[options] 节将证明模式设置为“使用 Unbounded model check 验证 safety properties”，并且将 k-induction 的深度设置为10；[script] 中是处理输入文件用到的 Yosys 命令；输入文件列在 [files] 节中。关于 .sby 文件语法的更多信息请参考 Reference for .sby file format，这里并不展开说明。mode provedepth 10[engines] smtbmc z3[script] read_verilog -formal hello.sv prep -top hello[files] hello.sv将上面的两个文件放在同一目录下，然后调用 sby 程序，即可获得证明结果。$ sby -f hello.sby...SBY 19:06:39[hello] engine_0.induction: finished (returncode=0)SBY 19:06:39 [hello] engine_0: Status returned by engine for induction: pass...SBY 19:06:39 [hello] engine_0.basecase: finished (returncode=0)SBY 19:06:39 [hello] engine_0: Status returned by engine for basecase: passSBY 19:06:39 [hello] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)SBY 19:06:39 [hello] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)SBY 19:06:39 [hello] summary: engine_0 (smtbmc z3) returned pass for inductionSBY 19:06:39 [hello] summary: engine_0 (smtbmc z3) returned pass for basecaseSBY 19:06:39 [hello] summary: successful proof by k-induction.SBY 19:06:39 [hello] DONE (PASS, rc=0)

cadence-irun（xrun） 增量编译 irun支持MSIE编译，MSIE的全称是 multi-snapshot incremental elaboration。将多个编译好的snapshot，组合成一个最终的snapshot，去仿真。利用这个技术，我们就可以使用irun来进行增量编译，从而节约编译时间。为了实现增量编译，我们将snapshot分为primary snapshot和incremental snapshot，primary snapshot指环境中不经常变化的代码，编译成的snapshot，incremental snapshot指环境中经常变化的代码，编译成的snapshot，最后再将这两个snapshot进行组合，得到最终的snapshot，去仿真。一、编译流程下图是单个primary snapshot的编译流程：将DUT，编译成primary snapshot，TB载入primary snapshot后，和tb一起进行编译，得到仿真的snapshot，再去仿真。下图是多个primary snapshot的编译流程：将SOC编译成primary snapshot，将IP编译成primary snapshot，将2个primary snapshot，和tb一起编译，得到最终的仿真snapshot，再进行仿真。二、实现方法一般情况下，我们是将DUT和TB进行分开编译，以实现增量编译。对于验证人员来说，DUT是不会变化的，因此我们可以将DUT，编译成primary snapshot，TB部分载入DUT的primary snapshot，和自己的TB代码一起编译，成最终的incremental snapshot，去仿真。这样，当环境修改之后，不需要重新编译RTL，这样，就节省了编译时间。特别是RTL的设计规模很大之后，这节约的时间，就更明显了。三、测试测试环境，组织结构如下：flist.rtl ： 编译rtl的flistflist.tb : 编译tb的flistMakefiletop_tb.sv ： testbench顶层source： 存放rtl code的目录uvm_code：存放tb code的目录1、makefile解析 Makefile内容如下：tc:= base_test_0 irun_prim: irun -sv -64bit -f flist.rtl -mkprimsnap -top uart_tx -l irun_rtl.log irun_inca: irun -c -sv -64bit -f flist.tb -uvm -uvmhome CDNS-1.2 -primtop uart_tx -l irun_tb.log irun_run: irun -R +UVM_TESTNAME=$(tc) -l irun_run.log clean: rm -rf INCA_libs rm -f *.log 对于 irun_prim 目标，根据RTL代码生成primary snapshot。-sv： 启动sv编译-64bit： 启动64位的irun-f flist.rtl : 指定编译RTL的flist-mkprimsnap: 生成primary snapshot-top： 指定RTL的顶层-l： 指定log文件对于 irun_inca 目标，载入RTL编译得到的primary snapshot，根据TB代码生成incremental snapshot， -c: 只编译，不仿真-f flist.tb： 指定编译TB的flist-uvm： 启动uvm编译-uvmhome CDNS-1.2： 指定uvm的home目录为irun工具目录下的UVM-1.2目录-primtop uart_tx： 指定需要载入primary snapshot的顶层。对于 irun_run 目标，仿真。-R ： 不编译，直接仿真+UVM_TESTNAME： uvm指定testcase的选项2、第一次执行make irun_prim； 生成primary snapshotmake irun_inca： 载入primary snapshot，和tb一起编译生成incremantal snapshot。载入primary snapshot：生成incremantal snapshot。3、第二次执行此时，修改top_tb.sv的代码，增加一行打印。因为RTL没有编译，因此可以跳过编译RTL，直接make irun_inca。载入 primary snapshot，跳过了代码生成。生成incremantal snapshot。仿真，打印出hello。测试的RTL，规模比较小，感受不到增量编译的好处，但是当RTL的规模一旦变得很大，编译RTL就要花费数十分钟，此时，就可以体会到增量编译的好处了。在服务器，测试我们的环境，使用增量编译后，将编译时间，从5分钟，缩减到了20秒。https://www.cnblogs.com/david-wei0810/p/14177607.html

在deepin或者UOS下安装Uengine及自定义各个安卓app显示窗口的方法 之前一直不知道自行安装的安卓app如何设置界面，后来经deepin论坛“云的眼泪”大侠指导，终于学会了设置，然后就有了这个小白教程1、Uengine安装方法打开终端，输入sudo apt install uengine,回车，按照提示输入密码会进入下载安装过程，安装结束exit回车退出。 2、Uengine运行器安装在浏览器里面输入如下网址下载安装[https://gitee.com/gfdgd-xi-org/uengine-runner/releases](https://gitee.com/gfdgd-xi-org/uengine-runner/releases)3、非应用商店安卓app的安装先自行下载需要的安卓app，然后点击uengine运行器，选择该安卓app所在位置，点击“安装”及完成（以电视直播酒店版为例）  安装完成后默认点开是竖屏的，需要手动切换为横屏，且窗口大小不能调整，这样用起来很不爽，就需要我们后面的步骤来单独设置。4、安卓app默认窗口显示的设置（以电视直播酒店版为例）（1）首先在桌面上选择“电视直播酒店版”（如果没有桌面图标就从启动器里面右键发送图标到桌面），右键选择“属性”打开属性界面  然后把鼠标指针移动到“位置”，这时候就会显示如图，记住其中的”com.dianshijia.hoteltv”备用。（2）进入系统盘，鼠标选中“usr”文件夹。右键选择“以管理员身份打开”，在跳出来的框里输入密码后确认打开该文件夹 依次点击进入share\uengine\appetc文件夹。右键新建一个以”com.dianshijia.hoteltv”命名的文本文件。  在该文本文件里面输入如下内容：verticalWidth 540  //竖屏宽verticalHeighe 960 //竖屏高horizontaltWidth 960 //横屏宽，备选为1280horizontaltHeighe 540 //横屏高 ，备选为720verticalScreen  1 //设置默认横屏还是竖屏，1为竖屏，0为横屏   allowFullScreen 0 //设置是否允许全屏，1为允许，0为不允许   allowScreenSwitching 0 //设置是否允许横竖屏切换，1为允许，0为不允许  defaultFullScreen 0 //设置是否默认显示最大化，1为默认最大化，0为不是可以视需要自行修改默认横屏还是竖屏显示，默认显示分辨率等。如图： 注意：分辨率等设置要适当，不能超过显示器支持的范围。  其他自行安装的app参照示例设置即可。（用uengine运行器安装app建议卸载的时候也用uengine运行器来卸载，直接卸载会有残留。）

数字后端知识点扫盲 HVT SVT LVT cell  知乎上有位大佬，领导要求做一个实验，在design进行综合的时候，只允许使用SVT cell，不允许使用LVT cell，实验结果出乎意料。先介绍一下背景，现在的design对功耗的要求很高，代工厂会提供多种电压阈值的单元库，大致可以分为三类，分别为HVT，SVT，LVT。这里的H/S/L分别为 high/standard/low阈值电压。HVT cell：阈值电压高，但是功耗低，速度慢LVT cell：阈值电压低，但是功耗高，速度快SVT cell：介于两者之间通常情况下，综合工具会把这几种cell库都吃进去，然后根据timing约束，由综合工具在满足timing约束的情况下自动选择使用什么cell，大部分情况下三种cell都会使用，在timing比较吃紧的path上会大量使用LVT cell，timing裕量比较大的地方使用HVT/SVT cell。最后的结果是：本来为了节省功耗，拿掉了LVT的cell以后，因为design太大，timing无法meet，所以综合工具自动插入了很多buffer，结果导致综合后design的面积增大了约15%，power反而比以前更大，充分证明了什么叫过犹不及。

wsl 子系统安装QT 概述在《Win10的Linux子系统Ubuntu安装图形界面》https://zhuanlan.zhihu.com/p/393145947https://blog.csdn.net/chentuo2000/article/details/119104547一文中我们为WSL安装了图形界面。在本文中我们在WSL图形界面的基础上安装和使用Qt。安装Qt2.1 Qt和Qt Creator的区别Qt是C++的一个库，里面集成了一些库函数，提高开发效率。Qt Creator是一个集成了C++语言和CMake工具的IDE开发环境。2.2 安装Qt5在WSL终端创建目录hkmkdir hk进入hkcd hk安装Qt5sudo apt-get updatesudo apt-get install cmake qt5-default qtcreator出错，按照提示，输入：sudo apt-get install cmake qt5-default qtcreator --fix-missing验证安装是否成功qmake -versionOK!查看Qt目录：找qt5的安装目录sudo find / -name qt5ls -l /usr/lib/x86_64-linux-gnu/qt5查看配置文件qt.conf2.3 运行Qt Creator启动XLaunch看《Win10的Linux子系统Ubuntu安装图形界面》https://zhuanlan.zhihu.com/p/393145947https://blog.csdn.net/chentuo2000/article/details/119104547在terminal执行命令qtcreator启动Qt Creator出错，解决方法：[https://stackoverflow.com/questions/63627955/cant-load-shared-library-libqt5core-so-5]sudo strip --remove-section=.note.ABI-tag /usr/lib/x86_64-linux-gnu/libQt5Core.so.5再执行qtcreator有错误，但Qt Creator启动了：2.4 解决错误问题QStandardPaths: XDG_RUNTIME_DIR not set, defaulting to '/tmp/runtime-ccdc'告知用户XDG_RUNTIME_DIR环境变量未设置，可以不管它，系统默认使用目录/tmp/runtime-ccdc：ccdc是我的用户名。XDG_RUNTIME_DIR给出用户运行时目录，如果不需要就不要定义这个变量。如果需要，在/etc/profile末尾增加一句：export XDG_RUNTIME_DIR=/your/dir/your/dir是你定义的目录。注意：这个目录对于执行qtcreator命令的用户一定要有读写权限。然后刷新全局变量：source /etc/profile解决libGL错误libGL error: No matching fbConfigs or visuals foundlibGL error: failed to load driver: swrast无匹配的帧缓存设置和视图，无对应swrast驱动。swrast主要用于图形渲染，其出现问题说明没有发现显卡的硬件驱动。解决方法参考文档：WSL下使用VcXsrv启动chromium browser及常见错误解析 (ubuntu18.04， 图形界面)[https://www.cnblogs.com/freestylesoccor/p/9630758.html]在启动XLaunch时关闭openGL 选项，该错误即消失，说明wgl(windows自带图像处理器）跟Qt存在兼容问题。取消Native opengl勾选。重新启动启动Qt Creatorqtcreator没有错误信息了，Qt Creator启动正常：QT项目测试创建项目File > New File or Project选择Qt Widgets Application，点击Choose。项目名称Name：hello创建目录：/home/ccdc/hkNext >默认，Next >默认，Next >默认，Next >默认，Next >Finish完成hello项目创建，进入代码编辑页面。出现错误：unkown type name ‘QApplication’unkown type name ‘MainWindow’解决办法：About > About Plugins > C++ 去掉ClangCodeModel的勾选。重新启动Qt Creator。打开我们之前创建的项目hello。错误信息没有了。界面设计双击mainwindow.ui打开UI设计窗口：拖拽一个Label组件到Type Here上。编辑text属性：OKCtrl+S保存。按F5或者点击左下角的Run按钮运行程序。参考文档.ubuntu 查找qt是否安装_ubuntu18.04 安装qt5.12.8及环境配置的详细教程https://blog.csdn.net/weixin_42352222/article/details/114472231?utm_medium=distribute.pc_relevant_download.none-task-blog-baidujs-1.nonecase&depth_1-utm_source=distribute.pc_relevant_download.none-task-blog-baidujs-1.nonecase.安装QT5 出现错误 unkown type name ‘QApplication’ unkown type name ‘MainWindow’https://blog.csdn.net/u01478378