Using SystemVerilog Assertion to Verify the Constant Register Optimization
Tang Yueke, Wang Xin
Analogix Semiconductor
Abstract
In typical ASIC design flow, verification is based on two main approaches: one is dynamic (functional) simulation; the other is static (formal) verification. Functional simulation verifies the correctness of design’s function, and verified design is used as reference for formal verification. Formal verification checks the consistency between reference and implementation. So the functional correctness of implementation is verified in this indirect manner. In the process of transferring RTL to netlist, logic synthesis tool such as Design Compiler (DC) can identify constant registers base on its optimization algorithm.
Then DC can remove those registers to corresponding constant. Register removal will cause false error when formal verification tool (such as Formality) performs equivalence checking. To avoid this false error, SVF (Formality Automated Setup File) is used to guide Formality to set the corresponding register in reference to constant. Formality can verify the consistency between RTL and netlist, but it does not directly verify the correctness of constant registers in functional perspective. So checking whether these registers really function as constant is a weak point in the verification flow. In traditional flow, designers usually deal with this problem by manually check. But manually check is time-consuming and error prone. This paper describes a new method which utilizes SystemVerilog Assertion to verify those registers are constant. A script is developed to automatically extract the guide_reg_constant information from SVF file, and generate assertions.
Then we can back-annotate them to RTL code and do regressions test by dynamic simulation tool. During regression test of functional verification, these assertions will be triggered to report errors if DC misunderstands any non-constant register to be constant. Hence, the consistency between RTL intent and DC optimization are verified automatically.
1.0 Introduction
As the chip design becomes more and more complex, two significant trends can be observed: one is that more and more IP blocks are reused in design implement flow; the other is adoption of the advanced verification technique such as ABV (assertion-based verification) and CRV (constraint-random verification). The first trend belongs to implement flow, and the second trend belongs to verification flow.
This paper describes a method which uses the new technique (assertion) in verification flow to verify the correctness of implement flow. This paper is organized as below. Section 2 will describe the constant register optimization in detail, and explain why constant register checking is a weak point between dynamic simulation and static verification. Traditional solutions to this question and their drawbacks are also presented. Section 3 will describes our new solution and its influence on existing design flow. Section 4 will shows the results and benefit after we adopt this new method in our projects.
2.0 Challenge of Constant Register Checking
2.1 Source of constant registers
A register is considered to be constant if it is set to a state (0 or 1) and can never escape that state. A register is also considered to be constant if it cannot escape its reset state.
Constant registers can be generally classified into two types: global constant and local constant. Global constant means that register are variable at block level, but are assigned with constant value at upper level (usually chip level). So constant-value will propagate into blocks when integrated in chip. If cross-boundary optimization is disabled during synthesis, global constant-register will not be removed. This situation happens frequently in IP reusing design. IP block is often design to implement multiple functions, but only one is needed in a specific chip. The simplest way of IP integration is to connect the configuration port to constant. For example, a pipeline multiplier may be used as a constant multiplier by connecting one of its inputs to constant. In another example, chip just needs part of IP block’s address/data bus.
If cross-boundary optimization is enabled, large amount of constant registers can be propagated and optimized. As more and more IP blocks are reused, more and more constant-registers can be removed.
Local constant refer to the registers which have constant value even in block level. Designer may write redundant register to improve the readability and extendibility in RTL code. For example, a counter threshold of 10 bit serves as criterion to reset counter. Suppose there’re only two possible threshold values in design, some bits of the threshold registers may be constants. People may think the number of local constants is smaller than global constants, but according to our projects experience, amount of local constants is also huge.
By default, Design Compiler tries to identify and remove constant registers in design. In doing so, DC can reduce the area and power consumption, and design timing may also be improved. As the constant identification algorithm improved, newer version of DC can detect more constant registers than older version.
2.2 A Weak Point in Verification of Constant Registers
Also because the large scale of today’s design, dynamic simulation on gate-level netlist costs more and more run-time. So formal-tool (Formality for example) is introduced to do functional equivalency-checking (EC) between RTL and netlist, or between netlist and another version of netlist. The functional correctness of RTL design is verified by dynamic simulation tool. The consistency between RTL and netlist is verified by EC tool. So the functional correctness of netlist is verified in an indirect manner.
EC tool rely on registers to separate design into logic cones and then take as compare-point, so removing registers will cause false mismatch report. Fig.1 illustrates the logic cone and compare-point.
Fig. 1 Logic cone and compare point
In order to solve this problem, automated verification setup file (SVF) is used to assist Formality. SVF files can either be automatically generated by DC, or manually created by designers. When Design Compiler performs constant register removing base on its analysis of RTL, the constant information is recorded in automatically generated SVF file.
After Formality read in SVF file, it will first valid the guidance in SVF file, if the constant register guidance is accepted, Formality will set register bits in the reference design to the corresponding constant value.
One rule in today’s ASIC design is that every step in implementation flow should have corresponding verification step. Formality uses RTL as ‘golden’ because the RTL is verified by dynamic simulation. However the constant information in SVF file is not dedicatedly verified by dynamic simulation. Though Formality does its own validation, effective verification of these constant registers with a simulator will definitely increase the confidence of making a ‘golden’ reference.
2.3 Traditional Solution and Drawback
When the scale of design is not very large, to further increase the confidence, a possible solution is manually checking. Constant register’s information in SVF file is sent back to RTL designers. The RTL designer will check the RTL code to see whether these registers are constant or not. In some case of local constant, designer will change the RTL code, remove the redundant registers. But usually designer would not like to do that in order to protect the readability and extendibility of the code, and modification to the verified RTL may bring out un-expected bugs.
Another serious issue of manually checking is efficiency. As we can see, in a complex design, there may be thousands of constant registers removed. It may consume weeks for designer to check the constant registers one by one. Manually checking is boring and error-prone.
Another solution is to disable the constant-register removal. By the command:
DC’s constant register removal feature can be disabled. Obviously, the penalty is that unnecessary extra logic waste area and consumes power.
There are two things about constant registers need to be verified: one is the constant attribute, i.e. registers’ value can not change; the other is the constant value (0 or 1). Formality can not do these jobs, but dynamic simulation tool can. The problem is that constant registers checking is not the part of functional verification plan in traditional flow. To solve this problem, we use SystemVerilog Assertion to check the correctness of constant registers.
3.0 Solution with SystemVerilog Assertion
3.1 Brief Introduction of Assertion
SystemVerilog is the extension of Verilog language, and provide powerful construct to support state-of-the-art verification methodology. SystemVerilog Assertion (SVA) is one of them. Assertions can be divided into 4 levels: Boolean Expression Level, Sequence Level, Property Specification Level and Assertion Directive Level
Fig.2 Level of assertion
Assertion can be very simple or very complex. Complex assertions with sequence and property are often written by design or verification engineer. In this paper, we create script to automatically generate simple assertion at Boolean expression layer.
3.2 Brief Introduction of SVF File
The SVF file contains setup information for Formality. Its information is based on the design transformations that occur during design synthesis and optimization process. By default, Design Compiler automatically creates a SVF file called default.svf. This file is stored in binary format. Formality can translate this binary file to an ASCII file of Tcl format.
The ASCII version of SVF file consists of a set of Tcl commands that start with guide. Some of important commands include:
● guide_reg_constant. This command records that a register was optimized to a constant value by logic synthesis tool.
● guide_inv_push. This command identifies a register that has a logical inversion push across it.
● guide_reg_duplication. This command records that a single register in reference design was duplicated in the implementation design.
● guide_reg_merging. This command records that mul tiple registers in the reference design were merged into one register in the implementation design.
For the more information on SVF file, see Reference [2].
3.3 Automatically Extract from SVF
We develop a Perl script to automatically process the ASCII Tcl version of SVF file, and generate SystemVerilog Assertion to monitor the value of constant register. By now, we just extract the “guide_reg_constant” command. After examining the automatically generated SVF file, we found the “guide_reg_constant” command has regular format as:
There are several things need to be aware on process with SVF:
● designName and instanceName have differenct meaning in case of local constant and global constant. In local constant, designName is the name of module which contains the constant register, and instanceName is the name of the constant register. In global constant, designName is top module of the design, and instanceName is the full path of the constant register.
● The full path name of the global constant register is shown as “sub_module0/sub_module1/sig_name_reg [0]”. ‘/’ need to be replaced by ‘.’; ‘_reg’ need to be removed. And designName need to be connected for SystemVerilog’s path name.
● SVF designate specific bit in 2-dimension array as “sig_name_reg[1><2]”, we must convert to SystemVerilog style: sig_name[1][2]
Appendix is the full Perl script to extract assertion from SVF.
3.4 Back Annotation to RTL
Two types of assertion are defined in SystemVerilog: concurrent assertion and immediate assertion. Concurrent assertion is based on clock, and can be used in static (formal) verification and dynamic (simulation) verification. Following example is the concurrent assertion:
Concurrent assertion can be put into testbench module directly. But SVF file do not has information of clock, so it hard to convert SVF to concurrent assertion.
Immediate assertion does not need to be related to clock. So we generate immediate assertion instead of concurrent assertion. Immediate assertion must be put in procedural block. Following example is the immediate assertion:
After assertion is extracted from SVF file, the next important thing is how to back annotate to RTL. There are also two methods to connect assertion to the design: one is inline method, the other is binding method. Both methods are useful for back-annotation. If local register is found, SVF just put module name in designName field. In this case, binding method is preferred because it’s hard to get full path name of that register. In the case of global constant, full path name of the instance can be extracted. So assertion with full path name can be insert inline with testbench module.
When assertion is adopted, one of the important issues is to avoid false failure during reset condition. Because verilog simulator will set all registers to value ‘X’ at simulation time 0, but the constant value in assertion is either 1 or 0, a false failure will definitely fire at simulation time ‘0’ if we don’t disable assertion at that time. SystemVerilog provide “disable iff” construct to deal with this issue, but “disable iff” can only used in concurrent assertion. In case of immediate assertion, we can put a judgment before assertions.
Note that SVF don’t provide reset information of registers, so we use a top level reset signal to strobe the assertion.
A better solution is using SystemVerilog $isunknown operator to avoid such false error. $isunknown return 1 if any bit of the expression is X or Z.
3.5 Put It All Together
The technique described in this paper can be integrated in the existing design flow seamlessly. The original flow is shown in left side of Fig3. It can be divided into two phases: RTL design phase and design implementation phase. In RTL design phase, the goal of dynamic simulation is to verify that the function of RTL meet the requirement of design specification. Once the RTL design phase is done, design can move on to implement phase. At the same time, dynamic simulation perform regression test on RTL.
In implementation phase, SVF file can be generated and then we can extract assertions and back-annotate them to RTL. So, regression test of dynamic simulation has one additional task: to verify the correctness of implement tool. Right side of Fig3 shows the new flow base on extracted assertions.
Fig.3 back annotate assertion flow
4.0 Conclusion and Future Works
The method described in this paper has been applied to several projects in Analogix. The table 1 shows the experimental result in some designs:
Table.1 Experimental Results
Although the designs are not very large, it contain near one thousand of constant registers. In traditional flow, it may consume almost a week for RTL designer to manually check the constant register. However, we still feel lack of confidence about the result of manually check. By the new method, automatic extraction and debug of assertions just need about one hour of time, and quality of checking is guaranteed by commercial simulation tool.
Assertions will make the regression simulation more complex, so it possible to slow down the simulation speeds. But the automatically extracted assertions are simple assertions, we don’t observe any significant slow down in regression test.
Currently, only immediate assertion can be automatically generated. The future work involve extraction of clock information, hence concurrent assertion can be used. Because concurrent assertion may be formally proven by other formal verification tool, it’s possible to save run-time of regression test with back-annotated assertion.
In fact, assertion is a powerful feature of SystemVerilog. It can serve as bridge between implementation tool and verification tool. This aspect of assertion’s application is worthy of farther exploration.
5.0 Acknowledge
We would like to thank our colleagues and team member: Song Hongdong, Liu Su, Zhao Ya. This paper’s idea is inspired during discussion with them. We’d like to thank our colleague Liu Haipin for his suggestion on Perl script programming. We are grateful to Li Ang from Synopsys Inc. for his encouragement and continuous support.
6.0 References
[1] SystemVerilog 3.1a LRM
[2] Formality Automated Setup File (SVF) Manual
[3] A Practical Guide for SystemVerilog Assertions
[4] SystemVerilog for Verification
7. Appendix
#!/usr/bin/perl
###############################################################################
## Copyright (c) 2002 ~ 2008 Analogix Semiconductor Incorporated
## All Rights Reserved
##
##*****************************************************************************
##
## File Name: svf2assertion.pl
##
## Author: Tang Yueke
##
## Description: This script extracts guide_reg_constant of SVF file and
## generate SystemVerilog Assertions
##
## Usage: svf2assertion.pl svf_file.svf.txt > assertions.sv
##
###############################################################################
open(SVF_FILE, $ARGV[0]);
$c = 0;
$n = 0;
while (<SVF_FILE>) {
if($n==3) {
my @consts = split;
$const = @consts[1];
gen_assert($design,$inst,$const);
$n=0;
}
if($n==2) {
my @insts = split;
$inst = @insts[1];
$inst = &proc_inst($inst);
$n=3;
}
if($n==1) {
my @designs = split;
$design = @designs[2];
$n = 2;
}
if (/guide_reg_constant/) {
$n = 1;
$c++;
}
}
#print “$c assertions generated\n”;
sub proc_inst {
$inst =~ s/\//\./g; # change / to .
$inst =~ s/\>/\]/g; # change >< to ][
$inst =~ s/\</\[/g;
# remove _reg
$where = index($inst, "[");
$sub_inst1 = substr($inst, 0, ($where-4));
$sub_inst2 = substr($inst, $where);
$inst = $sub_inst1.$sub_inst2;
}
sub gen_assert {
if ($_[1] =~ /\w\.\w/) {
print “assert if(rst_n_top) (”.$_[0].”.”.$_[1].” == “.$_[2].”);\n”;
} else {
$sig_name = $_[1];
$_[1] =~ s/\[|]/_/g;
$chk_name = $_[0].”_”.$_[1];
print “module “.$chk_name.” (input logic a);\n”;
print ” always_comb if(!\$isunknow(a)) assert (a==”.$_[2].”);\n”;
print “endmodule\n”;
print “bind “.$_[0].” “.$chk_name.” chk_”.$c.”(”.$sig_name.”)\n\n”;
}
}
Insight China
-
SNUG
-
White Paper
-
Good Chip Series
