Home

User`s Manual Formal Checkers - a Productivity Tool

1. end fail outputs Standard formula description is used for error message string 8 3 2 Count Events Syntax formula count lt t signal name gt lt Tp gt lt cn class name gt lt vn variable name gt Sugar formulation Note lt xxx gt is used for optional values supplied by the user For each count event if the class or variable name are not defined by the user the checker automatically produces a class name and a variable name using the name of checker s entity class name count_class_ lt checker entity name gt variable name count_ lt checker entity name gt _i where i is an index of the count event Examples for possible definitions assuming checker entity name is chkr formula count Sugar formula will be translated to count outputs 1 FoCs Formal checkers 87 CHAPTER 8 ai count_class_chkr count_chkr_i no_trigger end count outputs formula count t clk cn user_class_name Sugar formulation will be translated to count outputs Sahil 1s i user_class_name count_chkr_i clk tend count outputs formula count t clk Tp cn user_class_name vn user_var_name Sugar formulation will be translated to count outputs Sahl Tes i user_class_name user_var_name clk TracePoint 88 IBM Haifa Research Laboratory Provided by specia
2. the rule name will be used as the entity name e User defined you will be asked to provide a name during translation 6 4 2 Checker Module Name Verilog Only This is the module name of the resulting checker By default the rule name is used You can select User Defined and provide a name e Use rule name the rule name will be used as the module name e User defined you will be asked to provide a name during translation 6 4 3 Generate Module Verilog only This option allows you to choose whether or not to encapsulate the checker within a module e Yes e No 64 IBM Haifa Research Laboratory Provided by special agreement with IBM Customizing FoCs Settings 6 4 4 Produce Instantiation Code e FoCs can provide automatic generation of instantiation statements Component and Instance in VHDL Call in Verilog The instantiation code is produced according to the defined Mapping Options see CHAPTER 3 Linking Checkers with your Design e Yes e No 6 4 5 Create Enable Signals This option allows you to add these signals to the checkers code It either enables or disables the checkers during run time All checkers are enabled initially To disable a whole rule set enable_ lt rule_name gt to 0 To disable a formula set enable_ lt rule_name gt _ lt formula_number gt to 0 e Yes e No 6 4 6 Interface Filename By default FoCs regards signals that are only referenced not assigned in the rules
3. if endif etc and include See man cpp on your unix system for more details FoCs provides additional preprocessing abilities in addition to cpp These are the for and if constructs described below for The for construct replicates a piece of text a number of times with the possibility of each replication receiving a parameter The syntax of the for construct is as follows for lt var gt in lt exprl gt lt expr2 gt do Send Or sfor lt var gt in lt exprl gt lt expr2 gt step lt expr3 gt do send step can be negative or gfor lt var gt in lt item gt lt item gt lt item gt do Send where lt item gt is either a number an identifier or a string in double quotes When the value of an item is substituted into the loop body see below the double quotes will stripped Be aware that for generates a formula for each iteration of the for loop 46 IBM Haifa Research Laboratory Provided by special agreement with IBM The Sugar Specification Language In the first case the text inside the for end pairs will be replicated expr2 expr1 1 times assuming that expr2 gt expr1 In the second case the text will be replicated expr2 expr1 1 expr3 times if both expr2 expr1 and expr3 are positive or both are negative In the third case the text will be replicated according to the number of items in the list During each replication of the text the l
4. Checker Tool 105
5. INTEG ER variable result STD_LOGIC_VECTOR SIZE variable temp integer return STD_LOGIC_VECTOR 1 downto 0 synopsys built_in SYN_INTEG R_TO_SIGN begin synopsys synthesis_off ARG temp for i in SIZE 1 downto 0 loop if temp mod 2 1 then result i 1 else result i 0 end if if temp gt 0 then temp temp 2 else temp temp 1 2 simulate ASR end if end loop return result synopsys synthesis_on end i2vl convert a boolean to an STD_LOGIC_VECTOR function b2v1 ARG BOOLEAN SIZE INTEG ER is return STD_LOGIC_VECTOR FoCs a Formal Checker Tool 99 CHAPTER 10 variable result STD_LOGIC_VECTOR SIZE 1 downto 0 begin if ARG false then result SIZE 1 0 else result SIZE 1 1 end if if SIZE 1 then return result end if for i in SIZE 2 downto 0 loop result i 0 end loop return result end b2vl convert a logic vector to integer function vl2i src STD _LOGIC_VECTOR return integer is variable R integer variable mult integer begin R 0 mult 1 for i in src high downto src low loop if src i 1 then R R mult end if 100 IBM Haifa Research Laboratory Provided by special agreement with IBM Appendix A mult mult 2 end loop return R
6. as design signals The file defined as Interface Filename can be used to add signals that you want to regard as design signals If the signal has auxiliary EDL definitions in the rules file they will be ignored This option is useful when using the rule file for both model checking and checker generation The file is either a VIM DFF file or list of lines one signal name in each line 6 4 7 Design Entity Name Mvisim Bugspray Simulation Only This option allows you to define the design entity to which the checkers refer This is mandatory when using Bugspray It produces the Bugspray code design entity lt name gt 6 4 8 Vector Direction This option allows you to define the bit order in which FoCs generates vectors All FoCs a Formal Checker Tool 65 CHAPTER 6 vectors in the checker are written in the same way e Ascending 0 n e Descending n 0 6 4 9 Logic Signal Type VHDL only This option allows you to choose the standard logic support package to use e std_logic e std_ulogic 6 5 Reporting Tab The following sections describe the options available within the Reporting tab 6 5 1 Severity of Assertion VHDL Only This option allows you to define the severity of the generated VHDL assertion e Note e Warning e Error e Failure 6 5 2 Report Template File Mechanism Verilog and VHDL 93 full 6 5 2 1 Report template file In order to configure the checker output you can wr
7. cancel_read or write and no cancel_write until done then ok is asserted with done it is possible to write request read cancel_read done write cancel_write done done gt ok Writing an or between two subsequences means that only one of them must happen for the sequence to hold The subsequences may be of different length e To express the property Tf there is no abort during start a b c d end success will be asserted with end it is possible to write start a b c d end amp amp abort gt success The subsequences that have a amp amp operator between them occur simultaneously This means that they begin and end together and must have a non contradicting length The amp amp operator cannot appear in the right side sequence 5 2 2 4 Applying Never to SERE s We can use a sequence to check that a bad trace never happens This is done by applying the never operator to the forbidden sequence Examples e If request is asserted it will remain active until inclusive grant never request grant grant request e If request is asserted it will remain active until not inclusive grant never request grant request amp grant e Ifgrant is active and there is no ret ry in the next cycle busy must become active two cycles after grant 36 IBM Haifa Research Laboratory Provided by special agreement with IBM The S
8. cycle or later end is asserted e The other consecutive repetitions can also be applied to subsequences For example start end describes a trace in which the subsequence start end occurs at least once e start end 8 describes a trace in which the subsequence start end occurs exactly eight times e start end 8 describes a trace in which the subsequence start end occurs at most eight times The following are examples that use subsequences e After start if we see 8 gets not necessarily consecutive and there is no abort during this period then one cycle after the last get must begin 8 puts not necessarily consecutive before done done may not come at all start get labort get abort 8 gt put amp done put amp done 8 e If reql is active it will be granted gnt1 within no more than 7 gnts veql gt gnt gnt amp gnt1 0 6 gnt gnt amp gntl e pis true in cycle 0 and every fifth cycle true true 4 gt p FoCs Formal Checkers 35 CHAPTER 5 For details on all subsequence options see Section 5 3 2 2 on page 41 5 2 2 3 The and amp amp operators It is possible to define an AND and OR relation between subsequences using the Il and amp amp respectively e For example to express the property Tf there is a request that is followed either by read and no
9. end vl2i BEGI PROCESS VARIABLE focs_vout_0 std_logic_vector 0 TO 6 BEGI WAIT UNTIL clk EVENT AND clk 1 IF 12b rst THEN focs_enable_0 lt 1 focs_ok_0 lt 1 focs_v_0 0 TO 6 lt 1110000 ELSIF 12b focs_enable_0O THEN focs_ok_0 lt NOT focs_v_0 6 AND request AND NOT acknowledge AND NOT busy_flag focs_vout_0 0 TO 6 707 amp focs_v_0 1 AND amp focs_v_0 2 AND request AND NOT acknowledge focs_v_0 3 AND request AND NOT acknowledge amp focs_v_0 4 AND request AND NOT acknowledge amp focs_v_0 5 AND request AND NOT acknowledge amp focs_v_0 6 AND request AND NOT acknowledge AND NOT busy_flag FoCs a Formal Checker Tool 101 CHAPTER 10 focs_v_0 0 TO 6 lt focs_vout_0 0 amp focs_vout_0 0 OR focs_vout_0 1 amp focs_vout_0 0 OR focs_vout_0 1 amp focs_vout_0 2 amp focs_vout_0 3 amp focs_vout_0 4 amp focs_vout_0 5 END IF END PROCESS ASSERT NOT NOT clk OR NOT focs_enable_0 OR focs_ok_0 OR rst 0 REPORT FAILURE EVENT rule CHECK _BUSY_FLAG formula 1 formula 1 SEVERITY NOTE END checker 102 IBM Haifa Research Laboratory Provided by special agreem
10. flag gives a specific name for the output file checker name S This flag reads the setup file from the command line instead of reading the default setup file focs setup from the current directory 10 IBM Haifa Research Laboratory Provided by special agreement with IBM CHAPTER 3 Linking Checkers with your Design 3 1 Introduction In order to monitor design behavior during simulation the generated checkers must become part of the simulated model This occurs through the following three steps 1 Linkage The checker module in Verilog or entity architecture in VHDL must be compiled and linked to the design under test The actual commands are specific to the compilation simulation environment and are not within the scope of this document 2 Instantiation A call to the module in Verilog or instantiation of the entity in VHDL must usually be included in the design FoCs assists in this step by generating the calling statements 3 Signal Connection The checker signals must be connected to the real design signals The solution depends on the language and on the simulation environment FoCs provides a standard language solution for port mapping and specific signal connection solutions for several simulations FoCs Formal Checkers 11 CHAPTER 3 In the following sections we describe the mapping method and linkage 3 2 Signal Mapping To keep your formulas simple and readable you can use shor
11. formula fails The syntax is lt lt signal_name gt gt Every signal which appears in the formula description in lt gt brackets is replaced by its current value in the simulation output when the formula fails For example Formula description formula type COVER Values of signals fool lt fool gt formula body FoCs finds the signals in lt gt brackets in the description and adds them to the parameters list of the printf command If the signal is not a checker signal neither a checker port nor checker internal signal its type is assumed to be std_logic in VHDL or boolean in Verilog Note The use of the special names rule_name and desc is optional 6 5 2 4 Writing output to the file streams There are two options for defining file descriptors Option 1 The user controls file opening and closing outside the checker There is no special definition for file descriptors FoCs finds them in the fprintf commands and adds them to the checker ports as port of type FILE in VHDL or port of type reg 31 0 in Verilog In this option the user opens and closes the files and maps the file descriptors to the appropriate checker ports Option 2 Implicit file opening and closing within the checker In this option the user defines the file descriptors connections in the file section of the report template The syntax of the file section FILES lt file descriptor gt lt file name on disk gt lt fil
12. if src 0 then R 0 else Rassias end if return R end i21 function 121i src std_logic return integer is variable R integer begin if src 0 then R 0 else R 1 end if return R end 12i 96 IBM Haifa Research Laboratory Provided by special agreement with IBM Appendix A function b21 src boolean return std_logic is variable R std_logic begin if sre then R 1 else R 0 end if return R end b21 function 12b src std_logic return boolean is variable R boolean begin if sre 1 then R true else R false end if return R end 12b function b2i src boolean return integer is variable R integer begin FoCs a Formal Checker Tool 97 CHAPTER 10 if sre then else R 0 end if return R end b2i function i2b src integer return boolean is variable R boolean begin if src 0 then R false else R true end if return R end i2b function reverse arg std_Logic_vector return std_Logic_vector is variable result std_Logic_vector arg range begin for i in arg range loop result result right i result left arg i end loop return result end reverse 98 IBM Haifa Research Laboratory Provided by special agreement with IBM Appendix A convert an integer to an STD_LOGIC_VECTOR function i2vl1 ARG is INTEG ER SIZE
13. is now necessary only to verify that the counter never exceeds k We can use the same counter to check for an underflow its value should never be less than 0 Some properties might have become easier if one could talk about past events Assume we want to state that if p occurs then at that time q should be active since the last occurrence of r We can define a state machine inside the rule that will help us express this property as follows rule if_p_then_q_since_r var state boolean defining a boolean variable state assign init state 0 initialising the variable assign next state assigning a value to state in the next case cycle q 0 if q is false then next state is false q rill if q and r are true then next state is true FoCs Formal Checkers 49 CHAPTER 5 else state if the above conditions are false then stat esac does not change define q_since_r q amp r q amp state q_since_r means q is active since the last occurance of r formula If p occurs then at that time q should be active since the last occurrence of r always p gt q_since_r 5 5 1 Additional Expressions Used in State Machines State machines may include boolean expressions if then else expressions and case expressions 5 5 1 1 if and case Expressions There are two constructs which express a choice between two or more expressions They are the case and if exp
14. of these statements in detail 5 5 2 1 The var Statement A var statement declares auxiliary variables required for the state machine and the formulas in a rule and has the following format var name name type name name type The type can be one of the following boolean enum1 enum2 numberl number2 range between integers For instance the following are legal var statements var request acknowledge boolean var state idle reading writing hold var counter 0 1 2 3 FoCs Formal Checkers 51 CHAPTER 5 var length 3 15 The first statement declares two variables request and acknowledge to be of type boolean The second statement declares a variable called state which can take on 99 66 39 66 one of four enumerated values idle reading writing or hold The third statement declares a variable called counter which can take on the values 0 1 2 or 3 The fourth statement declares a variable called length which can take on any of the values between 3 and 15 inclusive We can also define arrays using the var statement An array of state variables is defined as follows var name indexl index2 type It actually defines index2 index1 1 state variables named name index1 name index2 where index can be either greater or less than index2 Examples var addr 0 7 boolean 8 bool
15. q_since_r 54 IBM Haifa Research Laboratory Provided by special agreement with IBM The Sugar Specification Language A module statement is used to define a module which can be instantiated a number of times as in hardware description languages It has the following format module module_name inputs outputs statement statement where inputs is a list of formal parameters passed to the module outputs is a list of formal parameters produced by the module and statements is any sequence of var assign define and instance statements The input output parameters can be thought of as input output signals Input parameters are produced elsewhere and they drive the module while output parameters are produced by the module itself and can be used elsewhere A signal that appears as an output parameter of a module must be defined and assigned a value in that module var or define or instance output If a signal that appears as an input parameter of a module is not used in that module FoCs will issue a warning Modules cannot be declared inside rules or other modules but they can be used instantiated by rules and other modules A module statement is only a definition it has no effect until it is instantiated called The instance statement instantiates a module using the following format instance instance_name module_name inputs outputs where instance_name is the name of the specific instance on
16. retry busy until end states that for every request assertion of signal req that is not retried signal retry 1s not retried in the next two cycles signal busy must be asserted until signal end is asserted 5 2 3 2The Construct SERE p before q If we want to describe that a specific signal must be asserted before another signal we can use the before operator For example Always if reg then ack will happen before the next reg req true ack before req SERE a before b expresses the requirement that on the last cycle of all traces that match SERE the first occurrence of a must happen before or together with the first occurrence of b There is no requirement that b eventually happen SERE a before_ b expresses the requirement that on the last cycle of all traces that match SERE the first occurrence of a must happen strictly before or the first occurrence of b There is no requirement that b eventually happen For example e If start is activated it must not be active again before stop is activated start true stop before start The true at the end of the sequence skips one cycle because we want to check the property on the cycle after start 5 3 The Building Blocks of a Sugar Formula 5 3 1 Boolean Expressions The basic building blocks of a Sugar formula are Boolean expressions A Boolean expression consists of signal names of the design
17. under verification numbers constants and operators 38 IBM Haifa Research Laboratory Provided by special agreement with IBM The Sugar Specification Language 5 3 1 1 Signal Names For integers i and j the following are the signal names e asimple name signal_name e A bit of a vector signal_name i bit i of signal signal_name e signal_name i j4 bits i through j of signal signal_name e signal_name b i j bitb of signal signal_name where the range is given by i and j b must be an integer and the relevant signal must be defined in the rules file 5 3 1 2 Numbers e A decimal number has only decimal digits and no suffix e g 1276 e A binary number consists of binary digits and ends with B e g 1011B e A hexadecimal number begins with a decimal digit has hexadecimal digits less than 8 and ends with H e g 7FFFH OFFH A reference to a whole vector should explicitly include its range vec1 0 16 rather than vec1 5 3 1 3 Operators The operators appearing in boolean expressions in decreasing precedence are described below FoCs Formal Checkers 39 CHAPTER 5 TABLE 1 Operators Examples e request is a boolean expressio set parentheses not multiplication and division addition and subtraction relational operators Boolean and Boolean or Boolean xor Boolean implication vector shift the right operand should be an integer n asserting that the enviro
18. with IBM Customizing FoCs Settings lt package 1 gt lt package 2 gt END In VHDL the library section contains libraries which the user wants defined in the final VHDL code by the library clause like ieee while the use section contains the full package names including the appropriate library name for example ieee std_logic_1164 all In the use section in Verilog the user must write Verilog file names which he wants included in the final Verilog code by using the Verilog compiler directive include The library section is ignored in Verilog The main purpose for including external libraries in checker code is to allow the use of functions and variables defined in these libraries If the function was defined in the external package file in Verilog and the package was included the user can use this function in his her report template FoCs does not perform syntactical or semantical checks on the included user packages files so if the package contains errors or if the parameters to the function call in the report template are not checker signals or predefined signals in included packages files FoCs will not report any error but the created checker will fail during the compilation For VHDL users only the only libraries which should not be defined in the library sections are ieee ibm work modelsim_lib and std These libraries are included in the checker automatically The packages which are included
19. 0 7 gt gt shift_amount ee 0 8 O ff 0 7 lt lt 1 Conversion of Bit Vectors to Integers and Vice Versa The following are built in functions for converting bit vectors to integers and vice versa FoCs Formal Checkers 57 CHAPTER 5 Bit vector to integer bvtoi a_vector Integer to bit vector itobv an_integer Example always Addr 0 31 itobv 256 gt bvtoi data 0 3 9 Note that constant integers are converted to bit vectors implicitly There is no need to apply itobv Construction of Bit Vectors from Bits or Sub vectors The concatenation operator is used to make bit vectors out of bits or smaller vectors expr expr Example define wide 0 5 narrow 2 3 bitl bit2 another_narrow 0 1 If expr is a constant it should be either 0 or 1 Wider constant vectors should be split into separate bits define x 0 5 y 0 2 1 0 z allowed define x 0 5 y 0 2 10B z not allowed The concatenation operator can also appear on the left hand side of an assign or define statement For instance the following statement define a b c 0 2 d 1 0 e 0 1 is equivalent to the following four statements define a d b 1 c 0 0 c 1 2 e 0 1 The built in construct rep expr N can help to construct arrays of repeated elements For example defining an array of 8 1 s assign arr 0 7 rep 1 8
20. 58 IBM Haifa Research Laboratory Provided by special agreement with IBM The Sugar Specification Language Shorthands zeroes N is equivalent to rep 0 N ones N is equivalent to rep 1 N 5 5 2 8 Array Notes The exact range must be specified in the operation a b is not equivalent to a 0 3 b 0 3 b 0 3 represents variables b 0 through b 3 while b represents one variable with no index Operands can take any ranges provided that their widths are compatible For example a 0 3 amp b 1 4 is legal but a 0 3 amp b 0 4 is not If one of the operands is a boolean vector and the other is a numeric constant the constant is considered an array of bits For example a 0 1 10B is equivalent to a 0 1 amp a 1 0 and a 1 0 10B is equivalent to a 1 1 amp a 0 0 If you write define N 7 and later a 0 N leave a space around the two dots a 0 N Otherwise the standard preprocessor cpp used by FoCs will identify N as a token and will not replace N by 7 5 5 2 9 More Array Examples var a 0 3 b 0 8 c 0 2 boolean define d 0 3 b 5 8 different sub ranges define e 0 2 b 0 2 amp c 0 2 different directions var x_state 0 2 y_state 0 2 sl s2 s3 define same_state x_state 0 2 y_state 0 2 var nda 0 2 boolean ll fo assign init a 0 2 assign next a 0 2 FoCs For
21. D VARIABLE focs_string_3 STRING 1 TO 1 SHARED VARIABLE focs_string_4 STRING 1 TO 23 COVERAGE EVENT rule SHARED VARIABLE focs_string_5 STRING 1 TO 10 at cycle SHARED VARIABLE focs_string_6 STRING 1 TO 3 We SHARED VARIABLE focs_string_7 STRING 1 TO 1 74 IBM Haifa Research Laboratory Provided by special agreement with IBM Customizing FoCs Settings SHARED VARIABLE focs_checkrule STRING 1 TO 9 checkrule SHARED VARIABLE focs_string_8 STRING 1 TO 27 Values of signals foo i SIGNAL focs_file_handl nable_0 std_logic SIGNAL focs_file_open std_logic 121 1 checker internal signals BEGIN PROCESS Process for files opening closing BEGIN Sr eyes EVENT AND clk WAIT UNTIL clk IF focs_file_open 1 THEN focs_file_open lt 0 file_open cover_file proj simulation_output cover WRITE_MODE focs_file_handl nable_0 lt 1 END IF WAIT UNTIL focs_finish_signal 1 IF focs_file_open 0 THEN focs_file_handl nable_0 lt 0 file_close cover_file END IF END PROCESS 75 FoCs a Formal Checker Tool CHAPTER 6 PROCESS other VARIABL VARIABLE BEGIN focs_formula_type IF IF WRIT command WRITE focs_ process varia E focs_line_1 VHDL checker bo lt formula failure co focs_formula_
22. ERAGE EVENT rule s at time d s rule_name Stime desc end Formula description formula type COVER Values of signals foo lt foo gt formula body Generated code Assuming that the rule name is CheckRule and fool is of type boolean The Verilog code generated by FoCs will be module checker ports foo focs_finish_signal checker signals input foo reg focs_file_handl nable_0 78 IBM Haifa Research Laboratory Provided by special agreement with IBM Customizing FoCs Settings input focs_finish_signal include print v define ERROR 1 define COVER 2 initial begin cover_file fopen proj simulation_log cover if cover _file 0 begin Smonitor Fatal error Can t open file proj simulation_log cover Sfinish end focs_file_handl nable_0O lt 1 dl wait focs_finish_signal focs_file_handl nable_0 lt 1 d0 Sfclose cover_file end checker body if lt formula fail condition gt begin assert0 integer focs_formula_type COVER if focs_formula_type ERROR begin Sdisplay ERROR in CheckRule at time 0d Values of signals fool b Stime foo end else FoCs a Formal Checker Tool 79 CHAPTER 6 if focs_formula_type COVER begin Sfdisplay cover_file COVERAGE EVENT rule CheckRule at time 0d Value
23. SERE can be described in English as If the right side occurs then the left side must occur For example the property If during get tag 1 then in the next get tag 2 and in the next get tag 3 is expressed by get amp tag 1 gt get get amp tag 2 get get amp tag 3 And the property If during get tag 1 and in the next get tag 2 then in the next get tag 3 is expressed by get tag 1 get get amp tag 2 gt get get amp tag 3 When we want to express that a signal p is asserted at least once we can use the event p For example start busy end gt success done states that if signal start is asserted signal busy is asserted for one or more cycles and finally signal end is asserted then success is asserted with end and followed by done Instead of writing true you can write start end gt success states that if signal start is asserted and two or more cycles later signal end is asserted then success is asserted with end followed by done There is a special way to describe an exact number of consecutive repetitions For example writing ready 8 expresses eight consecutive cycles in which ready is asserted start ready 8 gt result ok states that if start is followed by eight consecutive cycles in which ready is asserted then at the eighth ready result ok To say that ready is asserte
24. The Define Statement A define statement is used to give a name to a frequently used expression much like a macro in other programming or hardware description languages The define statement has the following format define name expression For instance the following are legal define statements define adef q r amp t v define bb 0 q amp t cc 3 As with the assign statement the keyword define may be omitted in second and FoCs Formal Checkers 53 CHAPTER 5 following consecutive define statements assign must refer to a variable defined with var define must NOT refer to a variable defined with var 5 5 2 4 The Module and Instance Statements A module statement is used to group together the statements of a state machine Instead of writing them directly inside the rule this module can be instantiated inside the rule using the instance statement For instance the following is a legal module statement module since el e2 el_since_e2 var state boolean assign next state case el 0 el amp e2 1 else state esac defin 1l_since_e2 el amp e2 el amp state This module can be defined in the rules file outside a rule and instantiated and used in arule as follows rule if_p_then_q_since_r instance il since q r q_since_r formula Tf p occurs then at that time q should be active since the last occurrence of r always p gt
25. User s Manual FoCs Formal Checkers a Productivity Tool Version 0 59 Formal Methods and Technologies Group IBM Research Labs in Haifa February 2003 Notices FoCs User s Manual Date modified February 2003 For information regarding FoCs contact Gil Shapir shapir il ibm com Tel 972 4 8296258 International Business Machines Corporation provides this publication as is without warranty of any kind either express or implied Some states do not allow disclaimer of express or implied warranties in certain transactions therefore this statement may not apply to you This publication may contain technical inaccuracies or typographical errors While every precaution has been taken in the preparation of this document the publisher and author assume no responsibility for errors or omissions Nor is any liability assumed for damages resulting from the use of the information contained herein Changes are periodically made to the information herein these changes will be incorporated in new editions of the publication IBM may make improvements and or changes in the product s and or the program s described in this publication at any time It is possible that this publication may contain references to or information about IBM products machines and programs programming or services that are not announced in your country Such references or information must not be construed to mean that IBM intends to announce such IBM pro
26. alias for FoCs The environment variable FOCS_DIR should point to the FoCs installation directory In csh setenv FOCS_DIR the_installation_directory In ksh export FOCS_DIR the_installation_directory FoCs Formal Checkers 8 Installation and Setup Create an alias focs for FOCS_DIR focs as follows or In csh alias focs SFOCS_DIR focs add FOCS_DIR to your search path 2 2 Running FoCs The following sections provide tips on how to begin working with FoCs 2 2 1 Checker Generation Before you begin you should create a working directory from which you run FoCs To begin using the FoCs tool 1 2 Type the command focs If this is your first FoCs session in this directory you have to set up FoCs for your project Click Settings to open the Settings dialog Select the target language VHDL or Verilog the target simulator only for VHDL the clock signal name and the reset signal name unless you ask FoCs to generate an internal reset Select the rules file the file in which you write your rules The language in which you specify rules Sugar is described in Chapter 4 of this guide You can browse through the other Settings tabs and fields if you want to have more control over the generation process Use the tool tips to see short field descriptions When you are done close the Settings dialog and return to the main window Select a rule to be translated into a checker and
27. amp acknowledge amp busy_flag focs_vout_0 0 6 1 d0 focs_v_0 1 amp 1 bl focs_v_0 2 amp request amp acknowledge focs_v_0 3 amp request amp acknowledge focs_v_0 4 amp request amp acknowledge focs_v_0 94 IBM Haifa Research Laboratory Provided by special agreement with IBM Appendix A 5 amp request amp acknowledge focs_v_0O 6 amp request amp acknowledge amp busy_flag focs_v_0 0 6 lt focs_vout_0 0 focs_vout_0 0 focs_vout_0 1 focs_vout_0 0 focs_vout_0 1 focs_vout_0 2 focs_vout_0 3 focs_vout_0 4 focs_vout_0 5 if clk focs_enable_0 focs_ok_0 rst begin Sdisplay formula 1 Sfinish end end endmodule 10 3 Checker Code in VHDL The following is the FoCs checker code in VHDL library ieee library ibm use ieee std_logic_1164 all use ibm std_logic_support all ENTITY check_busy_flag IS PORT clk IN std_logic rst IN std_logic request IN std_logic acknowledge IN std_logic busy_flag IN std_logic END check_busy_flag FoCs a Formal Checker Tool 95 CHAPTER 10 ARCHITECTURE checker OF check_busy_flag IS SIGNAL focs_enable_0 std_logic SIGNAL focs_ok_0 std_logic SIGNAL focs_v_0 std_logic_vector 0 TO 6 function i21 src integer return std_logic is variable R std_logic begin
28. an express properties of multi cycle traces using Sugar Extended Regular Expressions SEREs SEREs can be used to describe sequences of boolean expressions over time For example a SERE describing any occurrence of start ready ready can be written as start ready ready The at the start of the sequence is an event that denotes skip any number of cycles start between two commas start means a cycle in which start is asserted and in the following two cycles ready is asserted So this sequence represents many possible traces For example e traces in which start is asserted at the beginning and then followed by two ready start ready ready 32 IBM Haifa Research Laboratory Provided by special agreement with IBM The Sugar Specification Language e traces in which start happens at the second step and then followed by two ready true start ready ready true represents skip one cycle etc If we omit the sequence would describe only traces that start with start ready ready It is important to write at the beginning of the sequence because we usually want to refer to any occurence of start ready ready in the trace and not just at the beginning of the execution Writing SEREs is an extension to writing regular expressions Regular expressions are simple to write but still very expressive Defining a regular expression is very intuitive when keeping the desired timing diagram in
29. anguage cccccsccssssssccsssssseeees 30 Introducti iiini ia teehee ane EN cities eee tel eients 30 Getting Started with Sugar ee cesecseceeeceeeeneecsaecneeceeeeseeeseesnaeens 31 The Building Blocks of a Sugar Formula 0 ese eeeeeseeeseeeseeeneeeneeees 38 Writing a Rules Elenoire nin Ae eee des 43 State Machines tsi jeccetihiveasivadl onsen a aise flues 49 Customizing FoCs Settings cccccccssssscccsssssscscssssssssssesesees 61 OV ELVICWarssz ica fizsalemeeslemraci reel a a a aaia sche aiaa 61 M in Tabien bins a E EETA AN states cuentas 61 Cl ckand Res t Tabrani neia n E coh aa anibeeragettes 62 Checker Generation Style Tab sseeseesseseessereesrsrrsresressssesresresresrssress 64 Reporting Tabs ssisiccei ei eet eee Sele aie eg AE 66 SisnaleMap ping Tabien a detangviecsesscetedtian ves as 81 CHAPTER 7 Using FoCs for Functional Coverage Analysis sessee 83 7 1 Functional Coverage cece eceesceseesseeeeeceseceaeceaeeeeeeeeeeeeeeaeeseeesseeseeeeaees 83 CHAPTER 8 Defining Bugspray Event ssscccssssscscssssrsccsssssscsssocsees 85 S L Introduction sssini n enei e eE A EEN E EE 85 2 SYDUAK A E E A A 85 Bid EVES oseere AEE EEEREN EEEn 86 CHAPTER 9 FoCs for RuleBase Users seesessessescesorcesoeseesesoescecoscoscescesesceecese 91 9 1 Tips for Users of RuleB ase viisccsiciiiscsgettewent enc siesessiendsaietiesiers 91 CHAPTER 10 Appendix A aissicessscesdesssccsccocssvesssssssend
30. automatically are ieee std_logic_1164 all modelsim_lib util all ibm std_logic_support all and std textio all Each library package is included according to FoCs settings so that not all these packages are included in every checker The use of the libraries section the use section and the files section is optional You can write as many library package file sections as you wants Every new library package file descriptor name should appear on a new line The report template directives LIBRARY USE FILE END should also appear on a new line All text outside these special sections is treated as report template and is copied to the checker Comments Lines which starts with are treated as comments and thus are ignored by FoCs either in the report template or in the special sections FoCs a Formal Checker Tool 71 CHAPTER 6 6 5 2 6 Examples 1 The following is an example for output configuration using the report template file and formula description VHDL example Report template file LIBRARY utilsl Libraries section utils2 D ty Z USE utilsl print_functions_packagel all Use section utils2 print_function_package2 all td Z D FILES cover_file proj simulation_output cover File section m ND Template body IF focs_formula_type ERROR THEN printf ERROR in s at cycle d s rule_name cycle desc cycle is si
31. b occurs the number of times indicated not necessarily consecutively O O O O O Ono O O TABLE 3 Subsequence Operators If Q represents a sequence then the following are possible operators Operator Name Description Q Any repetition Q occurs 0 or more times Q Positive repetition Q occurs one or more times Q i Exact repetition Q occurs exactly i times 42 IBM Haifa Research Laboratory Provided by special agreement with IBM The Sugar Specification Language Operator Name Description OP Range repetition Q occurs at least i times but not more than j times Q i At least repetition Q occurs i or more times Ola At most repetition Q occurs no more than i times 5 3 3 Built in Functions Sugar has several built in functions which are described below fell expr is true if expr is 0 and was 1 on the previous cycle rose expr is true if expr is 1 and was 0 on the previous cycle prev x is true if x was true in the previous cycle next x is true if x is true in the next formula This construct can not be used in rules since rules shouldn t relate to the future It can be used when defining auxiliary variables and behaviors as will be explained in section 4 7 5 4 Writing a Rules File FoCs is rule oriented A rule is the basic component for which FoCs can generate a checker A rule defines a group of related properties represented as Sugar formulas which are translated into one checker I
32. boratory Provided by special agreement with IBM Linking Checkers with your Design content of file mapping dat clk clock rec receive trans transmit Is equivalent to clk design buf clock rec design buf receive trans design buf transmit To map ports to signals that appear in different parts of the design the signals are nested but the path is different from signal to signal the following syntax exists in the file mapping dat path lt path for the signal gt All of the signals that appear after this line and until the next line with the same syntax will receive the string in arrow brackets lt gt as a subpath in addition to the global path defined by a environment variable It is possible to use this syntax without defining a global path Example 1 Design Signals Prefix is defined to design content of file mapping dat path buf_l clk clock rec receive path buf_2 trans transmit Is equivalent to clk design buf_l clock rec design buf_l receive FoCs Formal Checkers 13 CHAPTER 3 trans design buf_2 transmit Example 2 Design signals Prefix is undefined content of file mapping dat path design buf_1l clk clock rec receive path design buf_2 trans transmit Is equivalent to clk design buf_l clock rec design buf_l receive trans design buf_2 transmit 3 2 0 2 Automatic Signal Mapping There is one more possibility to map a port signal If the por
33. click Generate Errors are reported in the Messages window below If generation is successful the checker filename will appear in the Messages window If you wish to translate several rules into one checker file select these rules using control mouse button or shift mouse button or the All button and press Generate You will be asked to provide a name for the checker file and for the entity name if the generated checker is in VHDL FoCs Formal Checkers 9 CHAPTER 2 2 2 2 Batch Mode Checkers can also be generated by the command line without invoking the GUI To generate a checker for a specific rule you must type in the command line focs batch lt rule name gt To generate a checker for all rules in the rules file you must type in the command line focs batch all To generate several rules you must type in the command line focs batch lt rules names gt In this case the settings for the generated checker are those defined in the file focs setup The best way to update this file is by defining the settings through the GUI When exiting FoCs the settings are saved to this file You can also use the following flags in the batch mode focs batch lt rule name or rules names or all gt rule file gt o lt output_file_name gt s lt setup_file_name gt Flag Explanation T This flag reads the rule file from the command line instead of reading the rule file from the setup file O This
34. d at most eight consecutive cycles we write ready 8 start ready 8 ready gt ok states that if start was asserted and starting the next cycle ready was asserted for at most eight cycles until ready was false then ok is asserted with ready The other types of consecutive repetitions are listed in Table 2 Assume we want to write the second ready after start should be accompanied with success Here we want to check also executions in which the start and the ready signals are not necessarily consecutive This can be expressed by start ready ready ready ready gt success IBM Haifa Research Laboratory Provided by special agreement with IBM The Sugar Specification Language The expression ready means zero or more consecutive steps in which ready is false e There is a special shorthand for non consecutive repetition For example the property Whenever we see eight non consecutive data transfers between start_trans and end_trans the signal error is not asserted with end_trans can be described by start_trans data 8 end_trans gt error The event data 8 represents eight non consecutive repetitions of data 5 2 2 2 Subsequences A sequence may contain a subsequence in curly braces e For example the sequence start end describes a trace in which there are zero or more occurrences of the scenario in which start is asserted and in the next
35. ducts programming or services in your country All trademarks and service marks are trademarks of their respective owners Copyright IBM Research Lab in Haifa 2000 2003 All rights reserved Table of Contents 1 1 1 2 CHAPTER 2 2 1 2 2 CHAPTER 3 3 1 3 2 3 3 CHAPTER 4 4 1 4 2 4 3 4 4 4 5 CHAPTER 5 5 1 5 2 33 5 4 5 5 CHAPTER 6 6 1 6 2 6 3 6 4 6 5 6 6 Introduction eeseeseeseseesseseccesoesessossescecsorceeeoeseeseesessesossorcesooseesoeseseeeee 5 OVETVIEW aar sees a E a E E Adan 5 About This Manual aein siei iei en E EEE ET E is 6 Installation and Setup ccccccscssssssssssssssssccsssssscsssssessssssssessoes 8 Installation e jesensenerstisivietedadlraaae caine yeast a eee Eai 8 Runnings FOGS aean nr kna aa ied ai dil ited 9 Linking Checkers with your Design ccssscccssssssccsssssees 11 Introducti oinn chaste sete aes vase EAE E EA E E A aet 11 Signal Mapping iin aen eeii eera neen eei i earo ieaie 12 Linkat zinrnne a a A R A A T tees 17 Tutorial scecesccdsecsnssuesneseescuisotisunonabeenavenseusseasocanavevesasnsoubessssenessot 21 Introd ct onsen n es oak eee a 21 Design Description 4c caiiahieied ana ink Maw nian dian 21 Phe RUSS Files ssvics steered caieeseriecaa an e E E ation 22 Initial Setup for a Working Environment 00 cee ceeeeeeeeeeeneeeneeeeeeeees 25 Generating Checkers iiet Shek telnet teed eaten ede eas 26 The Sugar Specification L
36. e descriptor gt lt file name on disk gt FoCs a Formal Checker Tool 69 CHAPTER 6 END i e every line in the file section consists of the file descriptor which can be used in print commands as described above and the file associated with it For example FILES error_fd proj simout error_file cover_fd proj simout cover_file END FoCs generates the VHDL Verilog code for opening and closing files and connecting them to their descriptors There is no need to predefine standard output stream The commands printf and display create the code which writes output to stdout according to the HDL subset When using implicitly generated opening closing of files FoCs generates the port focs_finish_signal The user must connect this port to the signal which gets the value 1 when the simulation ends The purpose of this port in the checker is to tell the checker when to close the files 6 5 2 5 Including files libraries and packages When describing the use of file descriptors the term file section was mentioned There are three special sections which can be defined in report templates the library section the use section and the file section This paragraph will describe the use of the library section and the use section Syntax library section LIBRARY lt library 1 gt lt library 2 gt END Syntax use section USE 70 IBM Haifa Research Laboratory Provided by special agreement
37. e formulas that can be used with FoCs e Chapter 6 Customizing FoCs Settings describes the settings and tabs that can be customized for your use e Chapter 7 Using FoCs for Functional Coverage explains how to enhance the quality of tests by providing a means for measuring test coverage e Chapter 8 Defining Bugspray Events for users who want to use FoCs with Bugspray instrumentation Explains how to define Bugspray events in the FoCs rules file e Chapter 9 FoCs for RuleBase Users explains the methodology of working with FoCs with properties used for Formal Verification e Appendix A Shows examples of checker code in VHDL and Verilog e Appendix B Documents and explains common error messages FoCs a Formal Checker Tool 7 CHAPTER 2 Installation and Setup 2 1 Installation This section explains how to install the FoCs tool and get it up and running If FoCs is not already installed on your computer or network proceed as follows 1 Create a new directory and copy the installation file focs tar gz into the directory 2 Type the command gzip d focs tar and press Enter 3 Type the command tar xvf focs tar and press Enter 4 Type the command rm focs tar and press Enter This will unzip the tar file and copy the installation files into their appropriate location 2 1 1 Personal Setup To customize FoCs for your individual environment you need to set an environment variable and create an
38. e module can be multiply instantiated module_name is the name of the module being instantiated inputs is a list of expressions passed as inputs to this instance outputs is a list of output parameters actually connecting the instance outputs to real signals of the design An instance name is optional 5 5 2 5 Advanced Operations on Arrays It is often convenient to apply operations to entire arrays or to ranges of indices Boolean arrays are the only arrays supported by FoCs These arrays are commonly FoCs Formal Checkers 55 CHAPTER 5 used for buses and bundles 5 5 2 6 Defining Arrays An array of state variables is defined as follows var name indexl index2 boolean An array can also be defined with a define statement define name indexl index2 lt expr gt For example define masked_sig 0 3 sig 0 3 amp mask 0 3 5 5 2 7 Operations on Arrays Reference The simplest operation on an array is a reference to a bit or a bit range One bit of an array is referenced as array_name N where N is a constant A range of bits is referenced as array_name M N It is always necessary to specify the bit range when referencing an array Other operations that can be used with arrays are l if case amp gt lt gt Example aa 0 7 if bb 0 2 cc 0 2 then dd 0 7 else ee 1 8 endif In boolean operands both operands must be of the same width unless one of them i
39. ean variables addr 0 addr 1l A var statement only declares auxiliary variables The assign and define statements described below define the behavior of these variables FoCs does not allow non determinism the value of a variable at each cycle should be explicitly defined using the assign and define statements 5 5 2 2 The Assign Statement An assign statement assigns a value to a state variable declared with a var statement It has one of the following formats assign init name expression assign next name expression assign name expression The first statement assigns an initial value to an auxiliary variable The second statement defines the value of an auxiliary variable in the next cycle The third statement assigns a value to a variable in the current cycle 52 IBM Haifa Research Laboratory Provided by special agreement with IBM The Sugar Specification Language The following are examples of legal assign statements assign init state idle assign next state case reset idlel state idle amp start idle state idle amp start busy state busy amp done idle else state esac The keyword assign may be omitted for the second and following consecutive assign statements Thus the following assign varl xyz init var2 abc next var2 qrs is equivalent to assign varl xyz assign init var2 abc assign next var2 qrs 5 5 2 3
40. ent with IBM CHAPTER 11 Appendix B 11 1 Common FoCs Error Messages Below are some common error messages and their meanings 11 1 1 Settings Errors Fatal error In Settings clock name must be supplied Defining the Clock in the Settings is obligatory Fatal error In Settings reset name must be supplied Defining the reset signal when reset is defined as External is obligatory Fatal error In Bugspray mode the name of the design must be specified When selecting Target simulator to be Bugspray defining the design entity name is obligatory FoCs Formal Checkers 103 CHAPTER 11 11 1 2 Sugar Errors and Warnings Warning Formula 1 Formula does not begin with always When a formula begins with always or a sequence begins with it is checked at every cycle Otherwise it is checked only at the first cycle Such a message is likely to appear if there is a formula with e1 e2 This formula doesn t start with and therefore will only be checked on the first cycle Warning Formula 1 Operation AF cannot run in Safety on the fly mode Warning Formula 1 Running this formula with OnTheFly No Warning Formula is not safety Translation failed Check if there is no use of AF or ECTL operators in the formula Formula not on the fly If one or more of the above messages appears it means that the Sugar formula is not supported by FoCs Since checkers run during simulation and the
41. es window Generating Done VHDL checker written to checker vhd or Done Verilog checker written to checker v FoCs Formal Checkers 29 CHAPTER 5 The Sugar Specification Language 5 1 Introduction Sugar is the specification language used by FoCs It is used to describe properties that are required to hold in the design under test DUT FoCs can very easily create powerful checkers from Sugar properties using only a small number of Sugar constructs In this document the term property refers to a specification described in informal English that must hold true for the design under simulation The term formula refers to the coded representation of properties in Sugar This chapter introduces Sugar in a way that allows FoCs users to start describing properties in Sugar and generating checkers from those properties simply The chapter is organized as follows Section 5 2 Getting Started with Sugar introduces the basic Sugar constructs This is an informal description of these constructs designed to give you the notion of how to describe the required design behaviors using Sugar Section 5 3 The Building Blocks of a Sugar Formula this is a more precise description of the Sugar properties building blocks Section 5 4 Writing a Rules File describes the notion and structure of the Rules File FoCs Formal Checkers 30 The Sugar Specification Language from which FoCs reads S
42. esponsibility to set x to be 1 and y to be 2 in checker instantiation FoCs Formal Checkers 19 CHAPTER 3 Note two mappings are give the same result under condition x 1 and y 9 ae Mapping file for a without generic ports aa main ul aa bb main u2 bb cc main u2 cc Mapping file for b with generic ports aa main u amp x amp aa bb main u amp y amp bb cc main u amp y amp cc Note x and y appear in mapping file without double quotes so that they are interpreted by FoCs as generic ports For more information about force freeze and signal spy see the MTI documentation The directives are derived from the mapping mechanisms described in the Signal Mapping section above This means that you have to provide a mapping file and or use the Design Signal Prefix option If the mapping method is something other than None the generated entity component and instantiation have an almost empty port map because the actual signal hooking is done through the special directives Only the clock and reset signals are explicitly referenced 20 IBM Haifa Research Laboratory Provided by special agreement with IBM CHAPTER 4 Tutorial 4 1 Introduction This chapter guides you through an example of a simple design and how FoCs can be used to enhance its verification productivity The tutorial presents a small design named BUF and a list of rules which the desi
43. gn must abide by and shows you how to generate checkers from these rules 4 2 Design Description BUF is a design block that buffers a word of data 32 bits sent by a sender to a receiver It has two control inputs two control outputs and a data bus on each side as shown in the block diagram below FoCs Formal Checkers 21 CHAPTER 4 11 t0B REQ BORREQS i tS ACK SB ACK Sender 1 BUF Receiver Ma ots eats DI 0 31 DO 0 31 OE Communication on both sides takes place by means of a four phase handshaking as follows When the sender has data to send to the receiver it initiates a transfer by putting the data on the data bus and asserting StoB_REQ server to buffer request If BUF is free it reads the data and asserts BtoS_ACK buffer to server acknowledge Otherwise the sender waits After seeing BtoS_ACK the sender may release the data bus and deassert StoB_REQ To conclude the transaction BUF deasserts BtoS_ACK When BUF has data it initiates a transfer to the receiver by putting the data on the data bus and asserting BtoR_REOQ buffer to receiver request If the receiver is ready it reads the data and asserts Rt oB_ACK receiver to buffer acknowledge Otherwise BUF waits After seeing RtoB_ACK BUF may release the data bus and deassert BtoR_REQ To conclude the transaction the receiver deasserts RtoB_ACK 4 3 The Rules File For the tutorial a rules file with some rules regardi
44. gnal defined by user in one of the packages error_func error_func is the function written in one of the predefined packages 72 IBM Haifa Research Laboratory Provided by special agreement with IBM Customizing FoCs Settings ELSEIF focs_formula_type COVER fprintf cover_file COVERAGE EVENT rule s at cycle d s rule_name cycle desc END IF Formula description formula type COVER Values of signals foo lt foo gt formula body Generated code Assuming that the rule name is CheckRule and foo is of type std_logic the VHDL code generated by FoCs will be other libraries library utils1 Library section library utils2 other packages use utilsl print_functions_packagel all Use section use utils2 print_function_package2 all FoCs a Formal Checker Tool 73 CHAPTER 6 ENTITY PORT checker ports foo IN std_logic focs_finish_signal file commands IN std_logic Special port added for END ARCHITECTURE TYPE focs_ftype is ERROR COVER checker internal signals FILE cover_file TEXT SHARED VARIABLE focs_string_0 STRING 1 TO 10 ERROR in SHARED VARIABLE focs_string_l STRING 1 TO 10 at cycle SHARED VARIABLE focs_string_2 STRING 1 TO 3 SHARE
45. he Bugspray definition A Bugspray definition is separated from a standard description by at the beginning and a 66 09 semicolon at the end formula lt Event type fail count harvest gt lt Special flags gt standard formula description Sugar formulation FoCs Formal checkers 85 CHAPTER 8 If no bugspray definition is used the formula will be a fail event The following are special flags used by Bugspray All special flags are optional Explanation In count events this flag defines a trigger signal a signal that says when to increase a counter for event If no signal name is defined in this case there is no need for writing t in special flags the keyword no_trigger is used as the trigger signal This flag denotes whether to use the keyword TracePoint for a count event This flag allows you to specify a variable name for count and harvest events This flag allows you to specify a class name for count events This flag denotes whether to use the keyword Cycle for a harvest event 8 3 Events 8 3 1 Fail Events Syntax formula fail standard formula description Sugar formulation will be translated in checker to fail outputs 86 IBM Haifa Research Laboratory Provided by special agreement with IBM Defining Bugspray Events SeNi de al i standard formula description
46. ierarchical signal names when writing Sugar formulas For such signals FoCs will automatically create a unique non hierarchal signal name and map it to the hierarchical name For example it is possible to write the formula formula always ul u2 aa In this case FoCs will generate a checker signal named focs_u1_u2_aa and a mapping between it and ul u 2 aa If a design signal prefix is defined it will be added to the signals mapping In the previous example if we had design signal prefix set to main we would get the mapping focs_ul_u2_aa gt main ul u2 aa For this kind of mapping Automatic Mapping should be chosen i e Warn Incomplete Mapping should be set to No It is possible to override the default mapping that is created by defining a different mapping for the signal name that was created in the mapping dat file In the above example it is possible to define in the file mapping dat the following mapping focs_ul_u2_aa design my_block aa 3 2 0 4 Mapping Vectors When a checker port is a vector the signal that will be mapped to it should also be a vector In the file mapping dat the syntax for vector is vector_name indexl index2 16 IBM Haifa Research Laboratory Provided by special agreement with IBM Linking Checkers with your Design This is a syntax only for design signals because the range of a checker port is known the size of design vector has to correspond t
47. ing simulation e Rising edge e Falling edge e Both edges 6 3 3 Simulation Delay Verilog only This option allows you to add a delay of n nano seconds between the active edge of the clock and the sampling of signals e No e Yes 6 3 4 Reset Mode This option allows you to provide an external reset to the checker or ask for an internally generated reset e External the reset signal will be provided as an input to the checker e Internal the reset signal will be generated internally It is mandatory to either define the external reset signal name or to choose the option of an internal reset signal 6 3 5 Checker Reset Name External Only If you choose External for the Reset Mode option you should provide the reset signal name mandatory 6 3 6 Number of Reset Cycles Internal Only If you choose Internal for the Reset Mode option you may select the number of cycles during which the internal reset signal remains active at the beginning of FoCs a Formal Checker Tool 63 CHAPTER 6 simulation The default is one cycle 6 3 7 Reset Polarity e Active high e Active low 6 4 Checker Generation Style Tab The following sections describe the options available within the Checker Generation Style tab 6 4 1 Checker Entity Name VHDL Only This is the entity name of the resulting checkers By default the rule name is used You can select User Defined and provide a name e Use rule name
48. inistic signal definitions The RuleBase rules file may include non FoCs Formal Checkers 91 CHAPTER 9 deterministic definitions that are relevant for environment definitions These definitions are irrelevant for the generated checker which receives its input from the simulation inputs For FoCs to ignore such definitions you must set the Interface Filename in Settings under Generation Style to your VIM DEF file located in your vimdbase DEF directory Using this file FoCs knows what signals are actual design inputs 92 IBM Haifa Research Laboratory Provided by special agreement with IBM CHAPTER 10 Appendix A 10 1 Examples of Checker Code in Verilog and VHDL Below is the checker code generated by FoCs for the Sugar rule vunit check_busy_flag assert request amp acknowledge 5 gt busy_flag 10 2 Checker Code in Verilog The following is the FoCs checker code in Verilog module check_busy_flag clk rst request acknowledge FoCs Formal Checkers 93 CHAPTER 10 busy_flag input clk input rst input request input acknowledge input busy_flag reg focs_enable_0 reg focs_ok_0 reg 0 6 focs_v_0 reg 0 6 focs_vout_0 initial begin end always posedge clk if rst begin focs_enable_0 lt 1 dl1 focs_ok_0 lt 1 dl1 focs_v_0 0 6 lt 7 b1110000 end else if focs_enable_0 begin focs_ok_0 lt focs_v_O 6 amp request
49. ional operators appears in Table 2 e Tf busy is true then working is also true always busy gt working gt denotes implies At most one of the signals x y or z is 1 mutual exclusion FoCs Formal Checkers 31 CHAPTER 5 always xt ty z lt 1 A list of mathematical operators appears in Section 5 3 1 on page 38 e Tf the head pointer of a queue is equal to the tail pointer quaeue_empty must be true always head 0 3 tail 0 3 gt queue_empty Both head and tail are 4 bit arrays and the expression head 0 3 tail 0 3 denotes equality of arrays The symbol denotes a range of array bits head 0 3 denotes bits 0 through 3 in the array head You can refer either to a range of entries of an array head 0 3 or to one entry of an array e g head 2 A reference to a whole vector should explicitly include its range vec1 0 16 rather than vec1 e The bitwise and of vectors vec 0 7 and mask 0 7 has at least one bit set always vec 0 7 amp mask 0 7 00000000b We need the parentheses around vec 0 7 amp mask 0 7 because has a higher precedence than Table 1 shows the operators precedence 5 2 2 Sugar Extended Regular Expression SERE The construct always p can refer only to an expression that spans one cycle Sometimes we want to check events that span over a period of time and not just one cycle To this end we c
50. ite a report template file In this file write the VHDL Verilog commands you want executed when the formula fails report template You can define different sets of commands for different formula types You can write the report template file in the following style 66 IBM Haifa Research Laboratory Provided by special agreement with IBM Customizing FoCs Settings VHDL Verilog IF focs_formula_type ERROR THEN if focs_formula_type ERROR lt VHDL code gt lt Verilog code gt ELSEIF focs_formula_type COVER THEN lt VHDL code gt else if focs_formula_type COVER END IF lt Verilog code gt This style is only a recommendation Every legal VHDL Verilog code is allowed because this code is simply copied to the checker Note that there is no previous syntactical or semantical checking done on this code so that every error in it will be determined only when compiling the checker with the VHDL Verilog compiler Both in VHDL and Verilog two additional commands with special treatment can be used printf and fprintf Their semantics and usage in the report template file are defined later in this document Verilog commands display and fdisplay have the same treatment as printf and fprintf and can be used for checkers generated in VHDL as well as Verilog FoCs will create equivalent code in the checker s language The content of the report template file is copied to the checker inside the IF statement used i
51. l agreement with IBM Defining Bugspray Events tend count outputs formula count Tp Sugar formulation will be translated to count outputs 1 i count_class_chkr count_chkr_i no_trigger TracePoint end count outputs 8 3 3 Harvest Events Syntax formula lharvest lt c gt lt vn variable name gt standard formula description Sugar formulation Note lt xxx gt is used for optional values supplied by the user For each harvest event if the variable name is not defined by the user the checker automatically produces a variable name using the name of checker s entity variable name harvest_ lt checker entity name gt _i Examples for possible definitions assuming checker entity name is chkr formula FoCs Formal checkers 89 CHAPTER 8 harvest standard formula description Sugar formulation will be translated to harvest outputs Sak os i harvest_chkr_i standard formula description end harvest outputs formula harvest c vn user_var_name standard formula description Sugar formulation will be translated to harvest outputs Sek 1z i user_var_name standard formula description Cycle end harvest outputs In all types of events indexes are assigned automatically 90 IBM Haifa Research Laboratory Provided by
52. mal Checkers 59 CHAPTER 5 var counter 0 7 boolean assign 0 counter 0 7 1 init counter 0 7 next counter 0 7 60 IBM Haifa Research Laboratory Provided by special agreement with IBM CHAPTER 6 Customizing FoCs Settings 6 1 Overview FoCs can be customized using the Settings dialog box The Settings dialog box consists of several tabs Main Clock and Reset Checker Generation Style Reporting and Signal Mapping each of which contains several options When you give an option a new value the new value is active as soon as you set it The value remains active for the rest of the session When you quit FoCs your settings are saved and used the next time you run FoCs The options are written to the file focs setup 6 2 Main Tab The following sections describe the options available within the Main tab 6 2 1 Rules File In this file you write the specification the properties to be checked For information on the specification language see CHAPTER 5 The Sugar Specification Language FoCs Formal Checkers 61 CHAPTER 6 6 2 2 Target Language This option allows you to select the target language for the automatically generated checkers e VHDL e Verilog Future versions of FoCs may include more target languages e g C and or C 6 2 3 Target Simulator VHDL only Some simulation environments only support a subset of the VHDL language Some environments include
53. mapping checker signals to design signals e Signal spy e None 6 6 3 Design Signals Prefix If design signals are nested and there is a common path for all signals it is possible to define the common path here In the mapping of checker ports to design signals this path will be added as a prefix to the names of design signals See examples in CHAPTER 3 Linking Checkers with your Design 6 6 4 Checker Signals Prefix MTI force freeze only When using force freeze specify the location of the checker relative to the monitor file 6 6 5 Warn Incomplete Mapping FoCs can supply warnings about checker ports that do not have a mapping defined in FoCs a Formal Checker Tool 81 CHAPTER 6 the mapping file or complete these values itself by mapping such checker signals to signals with the same name with the design signals prefix if such was defined e Yes FoCs will warn about signals that do not have a mapping defined for them No FoCs will create a default mapping for signals that do not have a mapping defined for them 82 IBM Haifa Research Laboratory Provided by special agreement with IBM chapter Using FoCs for Functional Coverage Analysis 7 1 Functional Coverage FoCs can be easily used to automatically generate monitors for tracking user defined coverage events The only difference between a functional checker and a coverage checker is in the interpretation of the error message in si
54. mind 5 2 2 1 The constructs SERE gt SERE and SERE gt SERE SERE s can be used to described properties that span several cycles For example the property whenever the sequence start ready ready appears the second ready after start is accompanied by result ok and followed by done can be written as start ready ready gt result ok done The meaning of this construct is as follows if the sequence on the left side is encountered during simulation then the right side should be true starting at the last cycle of this sequence It is possible to use two kinds of implication operators Using gt between the two sequences means that the right hand sequence must begin at the last cycle of the left hand side Using gt means that the right hand side sequence must begin one cycle after the left hand side The following are examples of properties that can be expressed using SEREs implication e start busy end gt success done states that if signal start is asserted at the next cycle or later in the future signal end is asserted and in the interim signal busy holds then success is asserted with end and at the next cycle done is asserted e request gt request grant states that if there is a request than it must remain active until grant FoCs Formal Checkers 33 CHAPTER 5 All properties in the form of SERE gt SERE and SERE gt
55. mulation For coverage purposes the message is a positive indication that the desired event happened We recommend using the following formula styles for coverage analysis with FoCs l always b The boolean expression b can never be true 2 never eventl event2 eventn The sequence of events can never happen In the checker which FoCs generates a message indicates that the event or sequence of events did happen Examples rule requestWithFullQueue formula a request comes when the queue is full FoCs Formal Checkers 83 CHAPTER 7 always request amp queue_full rule coverRWR formula read and later write and later read again never read write read assert read and later write and later read again and there was no other read between the two reads never read read read amp write read read More coverage options such as event counting will be added to FoCs in the future 84 IBM Haifa Research Laboratory Provided by special agreement with IBM cuaptens Defining Bugspray Events For IBM users only 8 1 Introduction When using Bugspray it is possible to define events of type fail count and harvest It is possible to associate a Bugspray event to every Sugar formula The definition is made in the description of the formula 8 2 Syntax The description of the Sugar formula starts with t
56. ng the BUF design has already been created and can be found at FOCS_DIR tutorial rules The rules are written in Sugar See CHAPTER 5 The Sugar Specification Language for more details The rules file contains the following rules rule ack_interleaving btor_reqstob_reqbtos_ackbtos_ack formula 22 IBM Haifa Research Laboratory Provided by special agreement with IBM Tutorial No overflow rtob_ack is asserted between any two btos_ack assertions RST amp rose btos_ackbtos_ack true rose rtob_ack before rose btos_ack formula No underflow btos_ack is asserted between any two rtob_ack assertions RST amp rose rtob_ack true rose btos_ack before rose rtob_ack rule four_phase_handshake_left formula T A request can not be raised when ack is high stob_req amp btos_ack stob_req false formula A request can not be lowered when ack is low stob_req amp btos_ack stob_req false formula An acknowledge can not be raised when req is low FoCs Formal Checkers 23 CHAPTER 4 btos_ack amp stob_req btos_ack false formula An acknowledge can not be lowered when req is high btos_ack amp stob_req btos_ack false rule four_phase_handshake_right formula A request can not be raised when ack is high btor_req amp rtob_ack b
57. nment signal request is e op READ op WRITE is a boolean expression asserting that the design signal op currently has either the value RI EAD or the value WRITE e counter gt 32 lt gt queue_is_full is a boolean expression asserting that the user defined signal counter has a value greater than 32 if and only if the design signal queue_is_ful1 is asserted 5 3 2 Temporal Properties 5 3 2 1 Temporal Constructs The temporal constructs of Sugar used by FoCs are summarized below These 40 IBM Haifa Research Laboratory Provided by special agreement with IBM The Sugar Specification Language constructs provide for the definition of temporal behavior across multiple cycles always p p is true on every cycle SERE gt SERE if the left side sequence occurs the right side sequence must hold starting from its last cycle SERE gt SERE if the left hand side sequence occurs the right hand side sequence must hold starting from the following cycle never SERE The sequence may never occur SERE p until q Starting at the last cycle of the sequence p must hold until q occurs not including the cycle q is asserted The formula does not require that q must eventually occur in that case p must be true forever SERE p until_ q Starting at the last cycle of the sequence p must hold until q occurs including the cycle q is asserted The formula does not require that
58. nstead of assertion as shown in the pseudo code example below IF formula failed THEN focs_formula_type lt ERROR COVER report template file content END IF 6 5 2 2 Formula type definition You can define the type of every formula as follows type ERROR COVER If no type is defined the default type value is ERROR Example formula type COVER Standard formula description FoCs a Formal Checker Tool 67 CHAPTER 6 formula body When generating checker code FoCs adds a variable named focs_formula_type for every formula that contains the value ERROR or COVER according to the type defined in the formula description ERROR and COVER are integer constants whose definition is implicitly generated by FoCs You may choose not to use this mechanism by means of not mentioning the formula type in the report template file The only side effect of this mechanism is the definition of the variables ERROR and COVER in the checker which implies that redefining these variables is forbidden 6 5 2 3 Usage and semantics of printf display and fprintf fdisplay The syntax and semantics of the display and fdisplay commands are similar to those of printf and fprintf respectively Syntax printf format parameters or fprintf fp format parameters The explanation for fp file pointer appears below The purpose of these commands is to configu
59. o the appropriate checker port Example content of file mapping dat path buf_l clk clock rec receive path buf_2 trans transmit bus vector 10 41 Where bus is the port in the checker which is vector 0 31 the above is equivalent to clk buf_l clock rec buf_l receive trans buf_2 transmit bus buf_2 vector 10 41 If the range of the vector is not defined the range of the checker port will be used All the options that were discussed in the previous subsections are relevant for both vectors and signals 3 3 Linkage The following sections discuss linkage which describes how to link the generated checkers with the design for several simulation environments 3 3 1 Verilog By default two files are generated the checker module and a file that contains a call to this module You should embed the call statement in the design The actual parameters in the call statement are the design signal names mentioned in the FoCs Formal Checkers 17 CHAPTER 3 formulas If a name is mapped as described in the Signal Mapping section above the post mapping name will be used as an actual parameter in the call statement You can choose to generate a bare Verilog by using Settings GenerationStyle GenerateModule NO In this case the checker will not be encapsulated in a module and you will have to embed its body in the design 3 3 2 Pure VHDL By default three files are generated the checker entity archi
60. of coverage monitors for coverage analysis When FoCs is used for this purpose the user specifies combinations and or sequences of events which he or she wants covered in simulation FoCs then automatically generates a checker to track the occurrence of these events during simulation For further information on FoCs see the FoCs website at www haifa il ibm com projects verification focs index html 1 2 About This Manual This manual is intended to serve as a guide for using FoCs including the definition of design properties using Sugar The manual is organized as follows e Chapter 1 Introduction introduces the FoCs tool e Chapter 2 Installation and Setup explains how to install and set up the FoCs tool The checker produced by FoCs for the above Sugar property is included for reference in Appendix A 6 IBM Haifa Research Laboratory Provided by special agreement with IBM Introduction e Chapter 3 Linking the Checkers with your Design explains how to link the checkers with the design you are testing e Chapter 4 Tutorial guides you through a short example where you can get hands on experience in creating checkers using FoCs e Chapter 5 Sugar provides details on how to start using the Sugar and EDL spec ification languages to specify the design properties including the structure of the rules file creating formulas expressions and satellites This chapter also presents examples of real lif
61. om one rule FoCs Formal Checkers 27 CHAPTER 4 1 Select rule ack_interleaving The Formulas window displays two formulas Click Generate One of the following messages according to the target language appears in the Message window Generating Done VHDL checker written to ack_interleaving vhd or Done Verilog checker written to ack_interleaving v You can open the file ack_interleaving vhd or ack_interleaving v created in your current directory and see the checker that was generated To generate a checker from several rules 1 2 Select rule ack_interleaving Press the Ctrl button and select rule checking data The Formulas window displays all of the formulas for these two rules Click Generate The Choose an output filename window will open Enter the name of the desired checker checker vhd or checker v and click OK The following message appears in the Messages window Generating Done VHDL checker written to checker vhd or Done Verilog checker written to checker v To generate a checker from all rules 1 Click All from the Rules window This selects all rules in this window 2 Click Generate The Choose an output filename window opens 28 IBM Haifa Research Laboratory Provided by special agreement with IBM Tutorial 3 Enter the name of the desired checker all vhd or all v and click OK The following message appears in the Messag
62. oop variable value can be substituted into the text as follows Suppose the loop variable is called ii Then the current value of the loop variable can be accessed from the loop body using the following three methods The current value of the loop variable can be accessed using simply ii if ii isa separate token in the text For instance Sfor ii in 0 3 do define aa ii Send BISTA is equivalent to define aa 0 define aa 1 define aa 2 define aa 3 oll WNnNrR OO Ne Ne oN VVNV NV ND MN LN If ii is part of an identifier it can be accessed using ii as follows for ii in 0 3 do define aas ii ii gt 2 Send is equivalent to define aa0 0 define aal 1 define aa2 2 define aa3 3 NNN NY VVNV NV If ii needs to be used as part of an expression it can be accessed using lt expr gt as follows Sfor ii in 1 4 do FoCs Formal Checkers 47 CHAPTER 5 define aat ii 1 ii 1 gt 2 Send is equivalent to define aa0 define aal define aa2 define aa3 wne oOo VVV V NM NM NM LN The following operators can be used in pre processor expressions l lt gt lt gt In the current version operators work only on numeric values i e it s OK to write the following Sfor i in 0 3 do i Sif i 3 Sthen end send But it is not possible to write Sfor command in read
63. properties are checked at each cycle only properties that can be verified at each cycle can be written Such properties are called Safety properties Properties that refer to sometime in the future such as liveness properties that ensure the occurrence of some event can not be verified during simulation and therefore cannot be used in FoCs See Sugar_v1 4 with FoCs notes for further explanation on unsupported Sugar operators Fatal error Nondeterministic operator is used Since the Sugar properties are translated to HDL code it is forbidden to use non determinism in the formulas and state machines Such a message may mean that there is a variable that has received a non deterministic value Fatal error Environment is nondeterministic behaviour of signal x is undefined In this case there must be some variable that was defined but not assigned 104 IBM Haifa Research Laboratory Provided by special agreement with IBM Appendix B Fatal error Environment is nondeterministic in signal x next state is defined without init state This means that there is an assign statement for variable x but no init statement This is forbidden because behaviour must be deterministic Fatal error Nondeterministic environment case without else in file A case statement must always contain an else part even if all cases are covered Otherwise the behaviour is considered as non deterministic FoCs a Formal
64. q must eventually occur in that case p must be true forever SERE p before_ q Starting at the last cycle of the sequence p must happen before the first q The formula does not require that q eventually happen SERE p before q Starting at the last cycle of the sequence p must happen before or together with the first q The formula does not require that q eventually happen The above formulas are enough for expressing most desired properties For a description of all Sugar formulas see the Sugar v1 4 document 5 3 2 2 Sequence Operators The building blocks of sequences are boolean expressions and operations on them The following tables summarize the possible operators Using b to represent a boolean expression Table 2 lists legal operators and their meaning FoCs Formal Checkers 41 CHAPTER 5 TABLE 2 Simple Operators 2 b occurs in 0 or more consecutive cycles b b b b i b occurs in one or more consecutive cycles i b occurs in exactly i consecutive cycles 29 b occurs in at least i consecutive cycles but inno more than j cycles b occurs in i or more consecutive cycles Paral b occurs in no more than i consecutive cycles Zero or more cycles are skipped One or more cycles are skipped i cycles are skipped Jd at least i cycles but no more than j cycles are skipped xd At least i cycles are skipped sA At most i cycles are skipped A sub sequence in which
65. rbiter which must abide by the following property upon the completion of five consecutive cycles where the request Sugar is an industry standard language for assertion based verification It was selected as a basis for an IEEE standard by Accellera on April 22 2002 In the future FoCs will also generate checkers in C C FoCs Formal Checkers 5 CHAPTER 1 signal is asserted and the acknowledge signal not asserted the busy signal should be asserted The Sugar formulation for this property is e request amp acknowledge 5 gt busy_flag Once this property is fed into FoCs the tool produces a corresponding VHDL or Verilog checker that can be integrated into a simulation environment and monitor the design behavior on a cycle by cycle basis for violation of the property It is often the case that a 1 line or 2 line Sugar property is automatically translated by FoCs to a checker which spans hundreds of lines of HDL code The benefit in terms of programmer time that would have otherwise been spent in manually coding the checker is evident There are other benefits to using FoCs such as reduced debugging time portability and reuse of properties The checking code produced by FoCs is synthesizable so this code can be used in emulation as well By virtue of these advantages FoCs increases engineering productivity in a very notable manner A complimentary application of FoCs is the generation
66. re the output which is written during the simulation to the log file or stdout The semantics are like the C semantics of these commands FoCs will identify these commands and generate VHDL Verilog code which will write output to the output stream defined in print command The syntax of the format is like C syntax every parameter should be defined in format by its prototype d s etc and every string can be written in the format The only difference from C is that there is no need to add a backslash before special characters like quotation marks and the use of double quotation marks and Allowed prototypes inside the format string are s string d integer b boolean and l1 std_logic Print commands should start at the new line cannot be broken by the new line in the middle and must not end with a semi colon Among the parameters there are two parameter names with special semantics rule_name and desc description both of which are strings When FoCs finds these parameters in the printf command the following is performed 1 rule_name will be replaced in the format string by the appropriate rule name 68 IBM Haifa Research Laboratory Provided by special agreement with IBM Customizing FoCs Settings 2 desc will be replaced in the format string by the description of the appropriate formula In the formula description you can define signals whose values you want outputted when the
67. ressions described below The case expression has the following format case conditionl exprl condition2 expr2 else exprn esac A case expression is evaluated as follows condition is evaluated first If it is true expr1 is returned Otherwise condition2 is evaluated If it is true expr2 is returned and so forth The else part is essential FoCs in order to define the behavior as deterministic it is advisable to the behavior as the default entry if you are not certain that the other conditions cover all the cases Falling through the end of a case statement may have unpredictable results Notice that from the description of the case expression above it follows that an earlier condition takes precedence over a later 50 IBM Haifa Research Laboratory Provided by special agreement with IBM The Sugar Specification Language one That is if two conditions are true the first takes precedence The if expression is shorthand for a case with two entries and it has the following format if condition then exprA els xprB endif In the above if expression exprA is returned if condition is true and exprB is returned if condition is false 5 5 2 Statements for State Machines FSM Statements The following statements are required for defining auxiliary variables writing state machines var define assign next assign init module instance The order of the statements is unimportant We now describe each
68. rule file select rule file from the settings window e Formulas window displays all formulas from the selected rules in the rules win dow e Messages window displays all relevant messages from FoCs The following is a screenshot from the tutorial 26 IBM Haifa Research Laboratory Provided by special agreement with IBM Tutorial FoCs 0 59 Beta 2 C copyright IBM corp 2001 2003 four phase handshake left four_phase_handshake_right checking_data Generating Formula 1 of rule ack_interleaving No overfiow RTOB_ACK Is asserted between arty two BTOS_ACK assertions l IRST amp rose BTOS_ACK true rose RTOB_ACK before rose BTOS_ACK Formula 2 of rule ack_interleaving No underflow BTOS_ACK is assented between ary two RTOB_ACK assertions P IRST amp rose RTOB_ACK true rose BTOS_ACK before rose RTOB_ACK Done VHDL checker written to ack_interleaving vhd To display the Settings window 1 Click Settings 2 Update the Clock Name and Reset Name in the Clock Reset Tab You can browse through the other Settings tabs and fields if you want to have more control over the generation process Use the tool tips to see short field descriptions 3 Choose the target language VHDL Verilog When you open FoCS for the first time all settings are set to their default values 4 Click OK This saves your settings and closes the Settings window To generate a checker fr
69. s constant The result will have the same width as the vector operands Example v 0 7 x 0 7 amp y 0 7 z 0 7 Relational lt gt lt gt Both operands must be of the same width unless one of them is constant The result will be a scalar boolean value 56 IBM Haifa Research Laboratory Provided by special agreement with IBM The Sugar Specification Language Examples c v 0 7 gt x 0 7 d v 0 7 lt 16 Arithmetic unsigned Both operands must be of the same width unless one of them is constant The result will have the same width as the vector operands Examples define ccl 0 7 aa 0 7 bb 0 7 cc2 0 7 aa 0 7 1 cc3 0 7 10 aa 0 7 In order not to lose the most significant bits of the result pad the operands with zeroes on the left For example define aa 0 7 zeroes 4 bb 0 3 zeroes 4 cc 0 3 cot sum 0 7 O ta 0 7 O b 0 7 is the concatenation operator described below zeroes 4 is a vector of four zeroes Shift gt gt lt lt The first operand must be a boolean vector and the second operand must be an integer constant or variable The result is a boolean vector of the same width as the first operand These operations perform the logical shift i e vacated bit positions are filled with zeroes Examples define cc 0 7 aa 0 7 lt lt 2 var shift_amount 0 5 define dd 0 7 bb
70. s of signals foo b Stime foo end end endmodule 2 VHDL Example counting events and stopping the simulation using report template file Report template file library utils end fuse utils countevents all Package utils countevents contains definition of integer counter with initial value 0 and the definition of constant STOP_VALUE end T IF focs_formula_type ERROR THEN counter lt counter 1 IF counter STOP_VALUE THE lt stop the simulation gt END IF END IF 80 IBM Haifa Research Laboratory Provided by special agreement with IBM Customizing FoCs Settings 6 5 3 Maximal Number of Fails This option allows you to limit the number of reported errors for one formula during run time inactivating the relevant part of the checker Moreover the formula will be disabled after the defined number of fails This option depends on setting Create Enable Signals to Yes because the enable signals are used to disable the formula 6 6 Signal Mapping Tab The following sections describe the options available within the Signal Mapping tab 6 6 1 Mapping File It is possible to define a mapping file that defines a mapping between checker ports and the actual design signals For more details see Section 3 2 on page 12 6 6 2 Mapping Method VHDL MTI Simulator only Selecting a Mapping Method allows you to select which method to use for
71. special agreement with IBM CHAPTER 9 FoCs for RuleBase Users 9 1 Tips for Users of RuleBase RuleBase is an industrial strength formal verification FV tool developed by the IBM Haifa Research Laboratory RuleBase is especially applicable for verifying the control logic of hardware designs and uses Sugar for design specification There are several advantages to using FoCs generated checkers in the simulation of designs which were formally verified against the same Sugar properties e Often the input constraints a k a the environment model defined for formal verification are more restricted than the real environment modeled in simulation Thus in simulation one can exercise the design against inputs whose effect on the design has not been explored by FV It follows that the enhanced checking capabil ity of FoCs provides better coverage and confidence in verification quality e FoCs checkers can help find problems in the input constraints defined for FV For example if the results of FV and simulation telative to the same properties do not agree it is likely that the input constraints have not been defined correctly e Using FoCs one can validate the assumptions made in the FV process These assumptions can be formulated as Sugar properties translated by FoCs into check ers and checked during simulation It is possible to use the same rules file for both RuleBase and for FoCs however FoCs only allows determ
72. special instrumentation for linking the checkers with the unit under test UUT If your simulation environment appears below select it Otherwise use Pure VHDL and tailor the checkers with the UUT to suit your needs e Pure VHDL e MTI FoCs generates a spy file used for linking checker names with UUT names See Section 3 2 on page 12 e Mvlsim Bugspray FoCs generates the checkers in a Bugspray file that are to be included in the simulation build process 6 2 4 Output File Name This is the name of the resulting checker file By default the rule name is used with the extension v verilog or vhd VHDL If you select User Defined you will be asked to provide a name each time a checker is generated e Use rule name the rule name will be used as the file name e Use entity name VHDL only the entity name will be used as the file name e Use module name Verilog only the module name will be used as the file name e User defined you will be asked to provide a name during translation 6 3 Clock and Reset Tab The following sections describe the options available within the Clock and Reset tab 62 IBM Haifa Research Laboratory Provided by special agreement with IBM Customizing FoCs Settings 6 3 1 Clock Name This is the design clock that drives the checker s clock mandatory Currently only a single clock is supported 6 3 2 Clock Polarity This is the clock edge in which signals are sampled dur
73. ssssestessicssesccsassancasssesscnsiss 93 10 1 Examples of Checker Code in Verilog and VHDL eee eee 93 10 2 Checker Code in Verilog seseeeseeseeeeeesreseesessrsrrssrsrieresresrrsreereseesesst 93 10 3 Checker Code in VHDL essseessesssesssesssssrsssssrsssrrssresreesressssseesssssses 95 CHAPTER 11 Appendix B seoosssocesseocesssosesscssecessscosessoossssoecesssecssssosesssosee 103 11 1 Common FoCs Error Messages cceseeseceseceseceseeeeeseeeseeeenaeenaeeaes 103 CHAPTER 1 Introduction 1 1 Overview FoCs short for Formal Checkers pronounced fox is a productivity tool that greatly aids design and verification engineers in the complex costly task of developing simulation test benches FoCs automatically generates simulation checkers also known as monitors from properties specified in the language Sugar These properties also called rules or assertions describe the legal behaviors of the design under test Typically the user of FoCs derives properties from the design specification documents where they are written informally in English and writes them as Sugar formulas Using FoCs these properties are translated into checker code in the desired target language Verilog or VHDL The checker code is then connected to the simulation environment During simulation the checkers track and report violations of the properties As an example of the power of FoCs consider an a
74. t and meaningful signal names You can then map these simple names to the real signal names FoCs will map those signals to real ports if an instantiation statement was created when a mapping for MTI is defined or when Bugspray is used For example use the name request rather than BXX_ARB_REQ You can create a mapping file in your working directory and let FoCs map the aliases to the real names The basic format of the mapping file is a list of pairs of signal names one pair in each line aliasl realnamel alias2 realname2 For example request BXX_ARB_REQ signall MY_DESIGN BLOCK1 BLOCK11 SIGNAL1 You should define the deliminators according to your mapping option for example dots for port mapping or slashes for MTI Signal Spy The mapping file should be pointed to by Settings SignalMapping MappingFile 3 2 0 1 Nested Design Signals If design signals are nested and all signals are declared in the same entity it is possible to define the Design Signals Prefix parameter in the settings options under Signal Mapping The value of this field is added to every design signal that appears in the mapping file In case of Automatic Mapping where the port name is considered to be the corresponding design signal name the Design Signals Prefix is added to all port names that appear in the checkers entity see Section 3 2 0 2 on page 14 For example Design Signals Prefix is defined to design buf 12 IBM Haifa Research La
75. t is possible to translate multiple rules into one checker It is also possible to define auxiliary variables and state machines by defining Finite State Machines FSMs as explained in section 5 5 and to include macro definitions as explained in Section 5 4 3 5 4 1 The Structure of the Rules File Before beginning you should plan the hierarchical structure of the rules files and how it will best represent the design properties A tules file consists of a set of rules where each rule may include one or more formulas at least one formula macros and FSM statements A formula describes a property of the design at hand Macros and FSM statements can be used to define auxiliary variables and state machines that ease expressing properties The structure of the rules file is FoCs Formal Checkers 43 CHAPTER 5 rule rulenamel lt Macro definitions define tif for gt lt FSM statements var assign define module instance gt formula textual description formal description formula textual description formal description rule rulename2 The rule names are any meaningful names that begin with a letter and consist of letters digits or underscores The textual description is text delimited within double quotes that describes the property in informal English The formal description is a Sugar expression The syntax of the Sugar language FSM statements and macros are defined in the follo
76. t signals have the same names as the signals in the design and are not nested or have the common path they can be mapped by defining Warn Incomplete Mapping to No in the Settings options under Signal Mapping and defining Design Signals Prefix to the path needed In this case every port name in the checker that does not appear in the mapping file or if a mapping file does not exist at all will be mapped to the signal with the same name and with the path defined by Design Signals Prefix A mapping that is defined in a mapping file overrides the Automatic Mapping As before defining the path is optional Example 1 Warn Incomplete Mapping No Design Signals Prefix design content of mapping dat path buf clk clock 14 IBM Haifa Research Laboratory Provided by special agreement with IBM Linking Checkers with your Design checker ports clk rec Is equivalent to clk design buf clock rec design rec trans design trans Example 2 Warn Incomplete Mapping No Design signals Prefix is undefined file mapping dat doesn t exist checker ports clk rec trans Is equivalent to clk clk rec rec trans trans Example 3 File mapping dat doesn t exist Warn Incomplete Mapping No Design signals Prefix design Is equivalent to clk design clk rec design rec trans design trans trans FoCs Formal Checkers 15 CHAPTER 3 3 2 0 3 Using Hierarchical Signal Names It is possible to use h
77. t you are checking If you have an English documentation of the rules use the same description for both and write the rule names in the relevant places in the documentation as well e Keep your rules file as readable and simple as possible you ll return to them when you don t expect it Using advanced mechanisms such as module and for is not always the most readable approach e Write your rules short as well A long complex rule can be easily fragmented It s good for generic reasons and also for readability e Partitioning your rules into several files will make it easier to work with when you have dozens of them e Use special naming conventions for auxiliary variables defined by FSM statements to distinguish them from signals of the design 5 4 3 Comments Macros and Preprocessing Directing There are two types of comments in environment description files FoCs Formal Checkers 45 CHAPTER 5 1 Text beginning with and ending at the end of line 2 Text beginning with and ending with Comment text is ignored by FoCs A comment can be inserted anywhere a space is legal except in text strings Before processing the environment description files FoCs calls a standard preprocessor cpp to filter these files The mechanisms provided by cpp can be used to facilitate the development of environment models The most useful mechanisms are macros conditional compilation ifdef
78. tecture a file that contains a component statement and a file that contains an instantiation statement You should embed the latter two statements in the design automatically if possible The actual parameters in the port map of the instantiation statement are the design signal names mentioned in the formulas If a name is mapped as described in the Signal Mapping section above the post mapping name will be used in the instantiation 3 3 3 Bugspray IBM only The generated checker contains instrumentation directives that help Bugspray link the checker to the design and connect the checker signals to the design signals The component and instantiation statements are not required and are not generated Settings GenerationStyle DesignEntityName must specify the design entity to which the checkers refer Port mapping names are used in Bugspray inputs section 3 3 4 Model Sim Three files are generated the checker entity architecture a file that contains a component statement and a file that contains an instantiation statement You should embed the latter two statements in the design There are three possible signal mapping methods controlled by Settings SignalMapping MappingMethod If you choose None the generated checker will be regarded as a Pure VHDL checker and linked to the design as such see above We recommend that you choose None If force freeze or signal spy is used appropriate mapping directives will be added
79. to the generated checker In the case of force freeze the directives are written to a separate file with the extension mon shortcut for monitor When using signal spy every design signal name must be double quoted 18 IBM Haifa Research Laboratory Provided by special agreement with IBM Linking Checkers with your Design except for generic ports described in the next section This is because signal spy mapping deals with strings 3 3 4 1 Signal Spy Mapping Using Generic Ports It is possible to define a mapping from signals to generic ports To map a signal to a generic port simply write the name of the generic port in the mapping file without double quotes It is also possible to use a concatenation of strings using generic ports exactly as you do when applying signal spy on your VHDL For example aa bb cc are checker ports main ul aa main u2 bb main u2 cc are design under test signals to which we want to map checker ports correspondingly Two examples of possible mappings FoCs can generate a without generic ports init_signal_spy aa main ul aa init_signal_spy bb main u2 bb init_signal_spy cc main u2 cc b with generic ports generic x STRING wi T y STRING we init_signal_spy aa main u amp x amp aa init_signal_spy bb main u amp y amp bb init_signal_spy cc main u amp y amp cc It is the user s r
80. tor_req false formula A request can not be lowered when ack is low btor_req amp rtob_ack btor_req false formula An acknowledge can not be raised when req is low rtob_ack amp btor_req rtob_ack false formula 24 IBM Haifa Research Laboratory Provided by special agreement with IBM Tutorial An acknowledge can not be lowered when req is high rtob_ack amp btor_req rtob_ack false VAR tmp 0 31 boolean ASSIGN init tmp 0 31 0 ASSIGN next tmp 0 31 IF rose btos_ack THEN DI 0 31 ELSE tmp 0 31 ea NDIF rule checking_data The data sent to the receiver is the same data received from the sender in the last write formula RST amp rose rtob_ack DO 0 31 tmp 0 31 4 4 Initial Setup for a Working Environment If you are running FoCs for the first time 1 Add the following setting to your cshrc file or the shell with which you are work ing setenv FOCS_DIR location_of_focs_executable FoCs Formal Checkers 25 CHAPTER 4 alias focs FOCS_DIR focs 2 Create a directory called focs_tutorial 3 Copy FOCS_DIR tutorial rules into your focs_tutorial directory The rules file includes four rules about BUF 4 Invoke the FoCs GUI by typing focs 4 5 Generating Checkers The FoCS GUI has three different windows e Rules window displays a list of rule names from the
81. type E focs_line_1 foc focs_formula_type COV bles LIN dy focs_ftype ER ndition gt THEN Report templat ERROR THEN s_string_0 Translation of print line_1 focs_checkrule tring_l T tring_2 tring_8 foo ne_l WRITE focs_line_1 focs_s WRITE focs_line_1l cycle WRITE focs_line_1 focs_s WRITE focs_line_1 focs_s WRITE focs_line_1 to_bit WRITELINE OUTPUT focs_li error_func ELSEIF focs_formula_type COVER WRITE focs_line_1 focs_string_4 WRITE focs_line_1 focs_checkrule WRITE focs_line_1 focs_string_5 WRITE focs_line_1 cycle 76 IBM Haifa Research Laboratory Provided by special agreement with IBM Customizing FoCs Settings WRITE focs_line_1 focs_string_6 WRITE focs_line_1 focs_string_8 WRITE focs_line_1 to_bit foo WRITELINE cover_file focs_line_1 END IF END IF END PROCESS END Verilog example Report template file USE print v END FILES cover_file proj simulation_log cover END if focs_formula_type ERROR begin Sdisplay ERROR in s at time d s rule_name time desc end else FoCs a Formal Checker Tool 77 CHAPTER 6 if focs_formula_type COVER begin Sfdisplay cover_file COV
82. ugar Specification Language never grant retry busy 5 2 2 5 Counting Boolean events It is possible to count boolean events that are not necessarily consecutive This is particularly useful when combined with amp amp Examples e Request will be serviced within the 5 coming acknowledges never req ack 5 amp amp serv 0 e Itis forbidden to have 15 writes during which there are less then 2 reads never write 15 amp amp read lt 2 5 2 3 Suffix Implication SERE It is possible to combine SEREs with temporal properties This form of writing means that starting from the last cycle of the sequence the temporal property must hold 5 2 3 1 SERE p until q Using this construct it is possible to check that some signal holds until another signal is asserted For example Between a request and its acknowledge the busy signal must remain asserted can be described by req true busy until ack SERE a until b means a should be true on the last cycle of the sequence and continue to be true until but not including when b is true a and b are boolean expressions and b may never happen SERE a until_ b means a should be true on the last cycle of the sequence and continue to be true until and including when b is true a and b are boolean expressions and b may never happen For example FoCs Formal Checkers 37 CHAPTER 5 e req retry
83. ugar properties to create checkers Section 5 5 State Machines this section describes how to use a larger subset of the Sugar language and gain further expressive power for defining complex properties 5 2 Getting Started with Sugar The Sugar specification language lets you describe properties to which the design under simulation must adhere Many properties can be easily described using the following constructs 5 2 1 Always p This Sugar construct enables you to assert that some property p is true on every cycle of the simulation P can be any boolean expression composed of signal names constants and operators For example you may want to check that signals grant1 and grant2 are not asserted together This property can be expressed in Sugar by the following formula always grantl amp grant2 which states that at every cycle of a simulation it is never the case that both grant 1 and grant2 are asserted The following are more examples of properties that can be expressed using always p e The property Whenever ack is asserted req was asserted in the previous cycle can be expressed as always ack gt prev rew prev x is a built in function which is true if x was true in the previous cycle A list of built in functions you can use appears in Section 5 3 3 on page 43 e Variables state1 and state2 never have the same value always statel state2 denotes inequality A list of relat
84. wing sections of this chapter The rule syntax is as follows rule name lt Macro definitions define if for gt optional lt FSM statements var assign define module instance gt optional formula textual description Sugar formula formula textual description Sugar formula 44 IBM Haifa Research Laboratory Provided by special agreement with IBM The Sugar Specification Language A rule must contain at least one formula All the other parts are optional The order of statements in a rule is unimportant and each type of a statement may appear several times It is important to fill in the textual description of formulas It is possible to have this description displayed when the checker generated from this formula detects an error during simulation 5 4 2 A Methodology for Writing Rules Files When designing a rules file you should consider both readability and efficiency issues e Go over the block outputs one by one and write in English all the things you can check on that signal its shape its valid values its relations with other signals etc e From a methodological standpoint it is useful to divide rules into 3 levels Level 1 Every signal to itself e g pulse constant zero Level 2 Relations between signals at the same interface e g request ack Level 3 Cross design signals or very complex rules e Write an English explanation for every rule specifying exactly wha
85. write do Sif command read then doesn t work Sif The if construct is similar to the if construct of the cpp preprocessor However if must be used when lt expr gt refers to variables defined in an encapsulating for The syntax of the if construct is as follows Sif lt expr gt Sthen Send or Sif lt expr gt Sthen 48 IBM Haifa Research Laboratory Provided by special agreement with IBM The Sugar Specification Language Selse Send 5 5 State Machines Although Sugar increases expressiveness capabilities there are still properties that cannot be expressed and others that are too complicated to formulate State machines may provide solutions in many of these cases The state machine records events that occur in the design under verification Formulas can then refer to these events by accessing the state machine s internal state State machines do not affect the design because information flows only from the design to the state machine In this section we describe the special statements for writing state machines For example assume that a queue of depth k reads data on one side and writes it on the other side Assume that we want to prove that the queue never contains more than k data items Formulation of this property in Sugar is difficult but it becomes easy with a satellite An up down counter is defined with a range of 0 to k and which is incremented on reads and decremented on writes It

User`s Manual Formal Checkers - a Productivity Tool

Contents

Download Pdf Manuals

Related Search

Related Contents