Autocheck是自动对RTL代码使用形式验证进行规则检查的检查器，是Questa Verify tools的一部分。Autochenck功能包括对设计的结构和功能属性进行静态验证，分析设计的各种逻辑结构，并验证这些结构是否符合特定的设计规则。
Autocheck analysis 在batch mode下使用TCL指令来配置环境，对代码进行编译检查。在Debug GUI下，对验证的结果进行debug。
Autocheck是对代码进行设计规则条件检查，验证的设计规则包括：
•Arithmetic rules such as divide-by-zero and value overflow.•Bus rules such as multiply-driven/undriven buses and one hot/cold conformation.•Case rules such as full/parallel case conformation anddefaultcase branching.•Combinational logic rules,such as combinational feedback loop implementations.•Logic rules,such as unused and undriven logic.•Register rules, such as multiply-driven, un-resetable and stuck-at registers.• FSM rules such as deadlock, livelock and reachability.•Other rules such as inferred latches,unreachable indexes,incomplete sensitivity lists。大概会有40+种规则检查，我们可以通过指令屏蔽一些规则的检查，提高性能。也可以添加信息，让它在分析中识别clock，reset，还有常量信号，具体信息要看autochenck_user；它对设计代码检查的结果按照severity分成下面几种：
•Violations—Must-fix design problems.•Cautions—Potential design problems.•Info— informational issue.•Inconclusion—Analysis timed out before determining if a violation was present•Evaluated—Evaluatedwithno problem found•Off—No analysis performed .design check type was disable before analysis 
我在终端上具体跑的flow：
下面是Makefile，里面有具体的指令：
Autocheck_designMakefile# V10.2 AutoCheck Design Checks Tutorial######################################################################### run: clean compile autocheck debug###### Define Variables ################################################# VLIB = ${QHOME}/modeltech/plat/vlib VMAP = ${QHOME}/modeltech/plat/vmap VLOG = ${QHOME}/modeltech/plat/vlog VCOM = ${QHOME}/modeltech/plat/vcom###### Compile Design ################################################### compile: rm -rf work transcript 删除work transcript $(VLIB) work 建立一个初始的设计库，库里包括所有的设计单元 $(VMAP) work ./work 建立设计从逻辑到物理的映射 $(VCOM) -f qs_files/filelist_vh 编译代码 $(VLOG)-f qs_files/filelist_vl 编译代码###### Compile Design ################################################### autocheck: rm -rf log_ac qverify -c -do" \ -c 启动CLI模式 -do"comman" or do_file configure output directory Output_Results; \ 设置输出目录 do qs_files/directives.tcl; \里面包含autocheck的一些参数指令 #### do qs_files/waivers.tcl; \ autocheck run -d vending_machine_controller -effort high; \ exit" vending_machine_controller 设计的顶层单元###### Debug Results #################################################### debug: qverify Output_Results/autocheck.db###### Clean Data ####################################################### clean: qverify_clean rm -rf work Output_Results transcript replay* modelsim.ini *.wlf`Makefile里面的directives.tcl是关于autocheck的一些指令，可以禁止autocheck做某种类型的检查，改变autocheck的一些参数。如果你做了某种检查的禁止的话，那么这个检查的结果就是Off。
在autocheck anaysis也就是第三步完成后，会在Output_Resuilts里面生成很多.db，.log，还有.rpt文件等，其中.db文件是启动debug GUI所需要的数据库文件，如果第四步无法打开GUI，就是我们数据生成的路径和我们调用的路径不一致，需要我们从Makefile里面查找原因。
因为这一步主要是debug，autocheck最有价值的地方就是在这里，所以单独的说一下这一步。其他的如果环境设置正确，代码符合各项规则，很容易就通过前面的检查。debug主要是针对设计的缺陷而言，可能设计中存在一个端口被赋值了两次或者有两个驱动，规则检查不出来，debug可以发现这个问题。
Questa Verify GUI 改正错误，用来检查和调试设计中的问题，可以追踪问题的原因。通过对代码的处理来改正错误，或者把某些instances设为Waived，这样就会默认为正确，或理解为对设计来说，这个问题是无关紧要的。对了，还可以设为filter，过滤掉这个错误。
Debug GUI打开的时出现的Design check window：
如何把某一种或某一个violation 设置为waived，或者 filter？
选中所要filter（或者waived）的violation → 右键 → Filter →Select
这样，Filter checks dialog就会显示我们所要过滤的violations，点击ok就完成了Filter,对于caution也是一样的操作。
如何查找设计的缺陷或者说如何Fix violation（caution）？
选中我们所关心的violation 或者 caution →右键 →show →schematic ；
这样，会出现电路原理图，我们可以根据电路模型图，推断出错误的原因。
或者也可以这样，选中我们所关心的violation 或者 caution →右键 →show →source；
这里会出现violation的信号或端口的声明，选中这部分定义→ Navigate →Drivers；
会出现所有跟violation的端口或信号有关的代码，颜色会特别标明，就像这样：
Questa Functional Verification-autocheck
原文：http://www.cnblogs.com/lylfate/p/4989772.html