Home

Hands-On Manual to Formal Check (V2.3)

1. Ackn gt 1 THIS IS A NEVER PROPERTY Page 50 Property Never_Multiple_Acks Type Never Never Multi Acks Options None Clock Constraint ck Signal arb ck Extract No Default Yes Start Low 1st Duration 1 2nd Duration 1 Reset Constraint reset Signal arb reset Default Yes Start High Transition Duration Value Start 2 1 forever 0 RUN OPTIONS Reduction Technique 1 Step Reduction Seed Empty Verification Query Only One Ack VERIFIED Wed May 10 01 16 29 2000 on server richards Query Data 1 32e3 combinational variables 1 02e3 Possible input combinations per state 20 State variables 2 1e 06 states Verification Data 1 11e 04 states reached Page 51 State variable coverage 20 variables 97 50 average coverage Search Depth 20 Real time 0 minutes 17 seconds Memory Usage 5 99654 megabytes Query 3 ery AckA_ Width Checking if the AckA is minimum of 2 clocks wide We can later check for AckB AckC and AckD Which can be easily done in command line version Property Min_Width_AckA_2clks Type Always After arb ack 0 rising Always arb ack 0 Options Fulfill Delay 0 Duration 2 counts of CkRising Constant Constraint Dont bypassA Signal arb byp_req 0 Default No Value 0 Group Constraint RegA Constraints RegA cant occur ReqA persists Default Yes Clock Constraint ck Signal arb ck Extract No Default Yes Start Low 1st Duration
2. rot amp D_ge_A amp D_ge_B Il rot amp B It D amp A It D assign selD pri3 2 lastGrant GrantB amp reqB amp rot amp C It D amp D_ge_A rot amp A It D D ge C assign selD pri3 3 lastGrant GrantA z reqA z rot B It D amp C It D Il rot amp D ge C amp D ge B assign selD pri3 regD z aged amp selD pri3 1 selD pri3 2 selD pri3 3 assign selA selA priO selA_pril selA pri2 selA pri3 assign selB selB prit selB pril selB pri2 selB pri3 assign selC selC_pri0 selC_pril selC_pri2 selC_pri3 assign selD selD priO selD pril selD pri2 selD_pri3 endmodule dpath age v H ok 3 3 R Sik 33 R S S R S Si SR S Si 3 S SS R S S SR S S SR OR S S Ri ee SR sk sk ok sk ok k ok ok ok kk k kk k k File age v Description Determines the Age of a Request Il H ie 3 3 R S SR 3 Si 3 R Sik Si SOR SR S SR SR SSSR SR S SR e S S R R S S Ri S S S ik 3 33 S S SSR SR k SR SR ae ok module age ck reset req ack AgeA AgeB AgeC AgeD inputck reset input 3 0 req ack output 2 0 AgeA AgeB AgeC AgeD wireReqA ReqB ReqC ReqD wireAckA AckB AckC AckD wireAwon Bwon Cwon Dwon reg 2 0 AgeA AgeB AgeC AgeD assign Awon req 0 amp amp ack 0 assign Bwon req 1 amp amp ack 1 assign Cwon req 2 amp amp ack 2 assign Dwon req 3 amp amp ack 3 always posedge ck Pag
3. state lt GrantB else if reqC state lt GrantC else if reqD state lt GrantD end end GrantB begin if reqA reqB reqC regD 1 b0 state lt IDLE else begin if reqA state lt GrantA else if reqC state lt GrantC else if reqD state lt GrantD end end GrantC begin if reqA reqB reqC regD 1 b0 state lt IDLE else begin if reqA state lt GrantA else if reqB state lt GrantB else if reqD Page 42 state lt GrantD end end GrantD begin if reqA reqB reqC regD 1 b0 state lt IDLE else begin if reqA state lt GrantA else if reqB state lt GrantB else if reqC state lt GrantC end end endcase end end endmodule fsm dpath v H k k 3 SR kK S R S SR S S SSR S SS R SR SSSR SR S SR OR S SR oko SS S oK S S S k E k k E k E k k E k k k k k k k k kk k kk k k File dpath v Description Datapath with Grant s Selection Logic Il LLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLDLLLLLLILLLLI include arb h module dpath AgeA AgeB AgeC AgeD rot aged req lastGrant selA selB selC selD input 2 0 AgeA AgeB AgeC AgeD inputrot aged input 3 0 req lastGrant outputselA selB selC selD LLLLLILLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLL Internal wire
4. 1 2nd Duration 1 Reset Constraint reset Page 52 Signal arb reset Default Yes Start High Transition Duration Value Start 2 1 forever 0 RUN OPTIONS Reduction Technique 1 Step Reduction Seed Empty Verification Query AckA_Width VERIFIED Wed May 10 01 17 03 2000 on server richards Query Data 1 32e3 combinational variables 512 Possible input combinations per state 25 State variables 1e 08 states Verification Data 1 54e 04 states reached State variable coverage 25 variables 96 00 average coverage Search Depth 42 Real time 0 minutes 24 seconds Memory Usage 6 0375 megabytes Query 4 Query Acka This query includes a liveness property and fairness constraint It says that eventually there will be an acknowledgment for the request from A Page 53 Property Eventually_AckA Type Eventually After ResetDone amp amp ReqA amp amp CkRising Eventually AckA Options None Constant Constraint Dont_bypassA Signal arb byp_req 0 Default No Value 0 Group Constraint ReqA Constraints ReqA_cant_occur ReqA persists Default Yes Group Constraint ReqB Constraints RegB cant occur RegB persists Default Yes Group Constraint ReqC Constraints RegC cant occur ReqC persists Default Yes Group Constraint ReqD Constraints RegD cant occur ReqD persists Default Yes Constraint Stable Rotation Type Always After ResetDone amp amp CkRising Assu
5. req 1 assign regC byp_req 2 amp reql21 assign reqD byp req 3 amp req 3 assign requests reqD reqC reqB reqA fsm FSM ck ck reset reset reqA selA reqB selB regC selC reqD selD state ack dpath DP AgeA AgeA AgeB AgeB AgeC AgeC AgeD AgeD rot rot aged aged req requests lastGrant ack selA selA selB selB selC selC selD selD age AGE ck ck reset reset req requests ack ack AgeA AgeA AgeB AgeB AgeC AgeC AgeD AgeD endmodule arb sin v H k kkk kk S S SR S SSSR S S SR S S SR SR SSR SR SS SR SR S S R S S S ee ee ee k k k k ok ok k kk k k k k k File fsm v Description Arbiter s Finite State Machine Il H o 3 3 R Sik SR S S SR S S 3 R S S SR SR S SR S S SR SR S SR S S SR Si S oko ko Ke k kk k k modulefsm ek reset reqA reqB reqC reqD state inputck reset reqA reqB reqC reqD output 3 0 state reg 3 0 state always posedge ck begin if reset state lt IDLE Page 41 else begin case state IDLE Waiting for Requests begin if reqA reqC regD 1 b1 begin if reqA state lt GrantA else if reqB state lt GrantB else if reqC state lt GrantC else if reqD state lt GrantD end end GrantA begin if reqA reqB reqC regD 1 b0 state lt IDLE else begin if reqB
6. Constraints Symbolic BDD Explicit State Enumeration Run Options Reduction Options Auto Restrict 1 Step Iterated FIG 3 4 The Query Panel and Its Features for Step 6 Page 20 Four main steps in the Query panel to remember 1 Name of the property 2 Type of property 3 Insertion of logic in Enabling Condition Fulfilling Condition and or Dis charging Condition 4 Taking care of Constraints Fulfill Delay A delay can be added between the Enabling Condition and the checking of the Fulfilling Condition This delay is specified as an integer that counts the occurrences of an event which is again specified by a boolean expression written into the Of Edge field please refer to Figure 3 3 Property panel Duration The verification windows terminates after a given duration of the Discharg ing condition becomes true whichever comes first The duration is measured by an integer same way as the Fulfill Delay Query Manager Description New VERIFIED Failed Edit Report Result Signals Waveform Missing Reduction Verify ET Copy to Delete Schedule Dismiss Fic 3 5 The Query Manager panel for Step 7 Step 7 Verify Query Before starting to verify the query the user has to save the query as well as the project Step 2 QUERY QUERY MANAGER Verify The user
7. environment H14 road H4 B environment H14 road HS 14 A fi status 1 A A A A A A environment H14 road A H6 I5 B B B B B B B B B status 0 status 1 fi VD5 state 0 1 0 fi VD5 state 01 1 environment H15 road fi status 0 environment H15 road fi status 1 environment H15 road status 0 environment H15 road status 1 environment H15 road fi VD5 state 1 0 environment H15 road fii VD5 state 0 1 I environment H15 road H4 B environment H15 road HS 14 environment H15 road H6 I5 environment H16 col environment H17_starv_ environment H18 112 environment H19 113 environment H20 114 environment H21 115 FCHECK C B reset active FCHECK P collision bcy0 free environment H14 road A VDS state environment H14 road A VDS state environment H15 road B VDS state environment H15 road B VDS state 0 1 free choices 1 1 free choices 0 1 free choices 1 1 free choices product of free choices 1 free environment_1x1x1x1 1 free choices product of free choices 1 looking for 400486bde2e4888a96a0765ca3de8bc06f34d7426b004e4b0394012c88d522073c4344bc5dd17fdb12a43dd391da3ae8bd3b78a0eb6 ad72a55f955107 FCkillMonitor 9771 PIDS is 9773 Page 33 Contents of the file ve
8. hotunroot hotback Msuperset reduc tion pthreshold 1e3 50 flow disconnect slowdisconnect 4 Status Begin parsing at 0 01 sec 0 megabytes query rf Wed Sep 22 14 31 28 1999 environment_ sr Wed Sep 22 14 31 31 1999 environment__ENV sr Wed Sep 22 14 31 31 1999 query sr Wed Sep 22 14 31 29 1999 CMC tools formalcheck2 1 SOLARIS include QRY h Wed Jul 29 14 17 28 1998 CMC tools formalcheck2 1 SOLARIS nclude QRY h Wed Jul 29 14 17 27 1998 CMC tools formalcheck2 1 SOLARIS include gui h Wed Jul 29 14 17 28 1998 Status Begin checks and tree rewrites at 0 15 sec 1 37626 megabytes query rf list entry count unM 2 M 2 M_o 4 568 pruned 1 active 4 freed by reduction 284 data variables declared or with width gt databits 4 4 selection local variables 1 bounded state variables 2 states 0 unbounded state variables 1 boolean cysets 0 boolean recurs 0 free selection local variables 1 selections state 2 kill free optimization actions 2 variable assignments driven by kills 886 variable reference clippings 655 expression clippings 2 vector bitwise comparisons expanded 0 pausing processes 0 non deterministic non free selection local variables 1 selections state maximum 1 total selections state maximum sr_E Equivalent reduction Task performed older run exit 3 FormalCheck Verification Finished Wed Sep 22 14 31 53 EDT 1999 Page 34 Contents of the file query c static char WHAT qu
9. 2 86e 03 states 2 86e 03 states reached State variable coverage 30 variables 93 33 average coverage Search Depth 42 Real time 0 minutes 12 seconds Memory Usage 2 32653 megabytes AckA arb ack 0 AckB arb ack 1 AckC arb ack 2 AckD arb ack 3 O AH Reqs arb reg 15 CkRising arb ck rising Multi Acks arb ack 3 arb ack 2 arb ack 1 arb ack 0 gt 1 RegA arb req 0 ReqB arb req 1 ReqC arb req 2 ReqD arb req 3 ResetDone arb reset finished 1 Page 58
10. 4 31 14 31 14 31 14 31 14 31 beng beng beng beng beng beng beng beng beng beng beng beng beng beng beng Sep Sep Sep Sep Sep Sep Sep Sep Sep Sep Sep Sep Sep Sep Sep DOTU environment sr environment ENV sr query M query U query U last query an query c query lines query rf query sr verify out verify stdout mi_khan dea Query_1 gt Fic 2 SnapShot of the Directory Query_1 Contents of the file verify stdout model M FCHECK bcy0 model unM FCHECK C B clk FCHECK C B reset model M p model M o environment H15 road B VD5 state 0 1 1 M or environment H15 road B VD5 state 0 1 0 or environment_ H14 road A VD5 state 0 1 I or environment_ H14 road A VD5 state 0 1 0 pruned environment ENV environment fi status A 0 environment fi status A 1 environment status A 0 environment status A 1 environment fi test environment test environment fi VDO T161 0 2 0 environment fi VDO T161 2 I environment fi VDO T161 2 2 environment VDO T161 2 TO environment VDO T161 2 I environment VDO T161 0 2 2 environment H13 police environment H14 road A fi status 0 Page 32 environment H14 road environment H14 road environment H14 road environment H14 road environment H14 road
11. Hands on Manual to FormalCheck Hardware Verification Group m y Harari udam Write Tc 2 Frl Fal 27 15 25 4 EST 1998 real E as ry tra fic light WEKIFITE Eat 4 p AT 177 en vermir ire mou les lesi n fata 46 cable yarime Beyin maitina ME ersten ina primary inge sri la n FormalCheck Concordia University Department of Electrical and Computer Engineering Montreal Quebec Canada May 2000 Page 1 1 2 3 4 5 TABLE OF CONTENTS Preface Audience Introduction Verifying Techniques used in FormalCheck Project FormalCheck Queries properties constraints Pros and Cons of using Constraints Checking for Overconstraint Stepwise Procedure of Verifying a Design in FormalCheck Step 1 Initializing Step Step 2 Saving the Project Step 3 Opening a file optional Step 4 Compiling the Verilo Step 5 Adding a Constraint Step 6 Create Edit Query Step 7 Verify Query Post Processing Analysis Advanced Options New Features AutoCheck Macro HDL design BUILD Page No Page 2 16 16 17 17 18 18 18 19 20 21 22 24 25 25 25 Page No Clock Extraction Script Interface IMPORTANT BUILD OPTIONS ADVANCED QUERY RUN OPTIONS THREE VERIFICATION ALGORITHMS A Recommended Procedure for Verification References APPENDICES APPENDIX A The System Settings to Run FormalCheck Running Forma
12. ReqB Constraints RegB cant occur RegB persists Default Yes Group Constraint ReqC Constraints RegC cant occur ReqC persists Default Yes Group Constraint ReqD Constraints RegD cant occur ReqD persists Default Yes Constant Constraint am high Page 56 Signal arb am Default No Value 1 Constant Constraint byp_req_low Signal arb byp_req Default No Value 0 Clock Constraint ck Signal arb ck Extract No Default Yes Start Low 1st Duration 1 2nd Duration 1 Reset Constraint reset Signal arb reset Default Yes Start High Transition Duration Value Start 2 1 forever 0 Constant Constraint rot_high Signal arb rot Default No Value 1 Seq Range 0 to 4 Initial 0 if Seq 0 amp amp AckA amp amp CkRising Seq 1 else if Seq 1 amp amp AckB amp amp CkRising Seq 2 else if Seq 2 amp amp AckC amp amp CkRising Seq 3 else if Seq 3 amp amp AckD amp amp CkRising Seq 4 else if Seq 4 amp amp CkRising Seq 0 else Seq Seq Page 57 RUN OPTIONS Reduction Technique 1 Step Reduction Seed Empty Verification Query Seq_ClockwiseAged VERIFIED Wed May 10 01 18 12 2000 on server richards Query Data 925 combinational variables 16 Possible input combinations per state 28 State variables 6 71e8 states Same as prior verification Wed May 10 00 48 10 2000 Verification Data Reachable space
13. VHDL Formal Check File Edit Project Query Window test define RED 1 b define GREEN 1 bl define WAITING 1 b define PASSING 1 bl module traffic_light ars reset initval direction input 1 0 cars input reset input initval output 1 0 direction reg 1 0 direction Iprojecthvg mi khan MY formalCheck EXAMPLES ilc v Post processing Netlist For Network traffic light Processing behavioral descriptions Processing network traffic light Build completed successfully Build completed successfully Fic 3 2 Running the Build option on an example for Step 4 Step 4 Compiling the Verilog VHDL design BUILD PROJECT BUILD Build option is the first main step towards verification Whenever any change in the design is made BUILD is necessary so as FILE SAVE The following three actions are performed implicitly by Build 1 Compilation of the design Verilog or VHDL ii Post Processing of the netlist 11 Processing of the behavioral description Page 18 Compilation errors are highlighted in the Diagnostic region and then are hyper links Clicking on an error will highlight the source line in the edit region that caused the error Note At the end of this Step 4 the project has to be saved once more repetition of Step 2 Formal Check He Edit Project Query Window Query define RED 1 define GREEN Query Na
14. alcheck2 3 SOLARIS setenv FCCC opt SUNWspro bin cc setenv NL_DIRECTORY usr local etc license cadence license dat setenv MANPATH FCHECKDIR syscad man MANPATH setenv FCATHOME no set path FCHECKDIR path alias formalreadthemanual CMC tools formalcheck2 3 tools sun4v bin openbook Or one can make a file called formalcheck env or any name env and source it everytime he wants to run formalcheck as follows source forrmalcheck env 3 FormalCheck comes with an example done as a tutorial for the new users Before run ning the tutorial from the help menu Getting Started necessary files should be copied to the current directory by exeuting the following command on the UNIX prompt gt cp r CMC tools formalcheck2 3 SOLARIS examples The online tutorial is the guickest way to learn formalcheck 4 The tools comes with very useful sets of documents The access to different documents can be done in following ways SOURCE 1 By typing formalreadthemanual without colons in the command prompt The prerequisite of this command is sourcing the env file explained before This is the most extensive source of information one can get about for malcheck The command formalreadthemanual will invoke openbook utility of unix and the user can read on just by clicking the mouse SOURCE 2 The other documents are accessible after running the tool from the help menu These documents contain comparatively short de
15. awn Il Il modulearb ck reset req byp_req rot am ack input reset input 3 0 req byp_req input rot am output 3 0 ack LLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLDLLLLLLLLLLLLLLLLLLLLLLLLI Brief Description on I O signals LLLLLLLLLLLLLLLLLLLLLLLLELLLLLLLLLLLLLLLLLLLLLLLLLLLELLLLLLLLLLLLLLI Il Inputs cksystem clock resetsynchronous reset Active high reqbus requests from clients byp_reqcommand to bypass requests from clients rotarbiter s rotation direction rot Value Polling Direction CounterClockwise 1 Clockwise amarbitration mode scheme am Value Arbitration Scheme Round Robin 1 lAged based Page 40 Il Outputs ackacknowledgement of bus grants back to clients Il LLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLDLLLLLLLLDLDLLLLLLLLLLLLLLLLEL Internal wires Sk k k ohe k sk sk k sk K k sk KK sk ohe k sk ok k K KK ok sk odk ke OK kK ECCE ole k ke ole k ke ohe OK s k k 3 K k ok ohe ok ok sk ok ke K ok ok K k ok ok K wireselA selB selC selD aged wire 2 0 AgeA AgeB AgeC AgeD wire 3 0 requests ack wirereqA reqB reqC reqD assign aged am assign regA byp req 0 amp req 0 assign reqB byp_req 1 amp
16. bypass requests The above picture shows the block diagram of the circuit The state diagram of the circuit s functionality is depicted on the next page Page 37 ReqDReqA Rot ReqA ReqB ReqC ReqD ReqAReqB Rot ReqA ReqBReqC ReqA ReqBReqC Rot Off ReqA ReqB ReqC ReqD Fic 4 Arbiter State Diagram Table 1 Arbiter s I O Specification SIGNAL POLARITY BRIEF DESCRIPTION Req 3 0 1 Client s Request Active High Byp Reql3 0 1 Command to Bypass Requests Active High Rot 0 1 0 Counter clockwise Rotation 1 Clockwise Rotation Am 0 1 Arbitration Mode 0 Round Robin 1 Age Based Ck Posedge System Clock Reset 1 Reset Signal Active High Ack 3 0 1 Acknowledgement Active High Page 38 Arbiter Basic Specification e Request inputs Req 3 0 are required to be deasserted a minimum of one clock cycle after the request is acknpwledged e Acknowledge outputs Ack 3 0 will remain stable one clock cycle after the corresponding Request Req 3 0 input goes low The following are all the necessary verilog files of the RTL design RTL design arb h Il File arb h Description Global Mnemonic Assignments in arbiter Il LLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLDLLLLLLILLLI define IDLE4 b0000 define GrantA4 b0001 define GrantB4 b0010 define GrantC4 b0100 define GrantD4 b1000 arb v 7i File arb v De
17. ck of vectors It is common to wait for the test bench to be completed before starting simulation and a complete test bench is only created at the chip level With FormalCheck verification can be started as soon as the first block is designed and the first query is written This speeds up the design cycle by catching the bugs at an earlier stage and also reduce the verification effort In short Formal Check model checker can be used when the design is fluid or only partially defined 3 ACTIVE free fence PRUNED FIG 1 2 Localization Reduction algorithm 3 It is of paramount importance that the tool be able to reduce the model automatically relative to the property under check to the greatest extent possible 3 FormalCheck uses two approaches of reduction algorithm step and iterative Most of the reductions tend to be property depen dent ocalization reductions 5 in which the part of the design model that are irrelevant to the property being checked are abstracted away In FormalCheck localization reduction is applied dynamically At each step of the algorithm the model is adjusted by advancing its free fence Page 7 please refer to the Figure 1 2 of induced primary inputs in order to discard spurious counter examples to the stated query 5 1 step reduction looks at the dependency graph and removes any portion of the design from the verification proof that cannot affect the outcome of the query Thi
18. ctory for each failed query and ODAN uses those files to offer the following capabilities nteractively select a subset to the signals for display Zoom in on critical areas Select a specific time region to view signal activity in detail Group signals under one label If the result is Vacuous then there may be a possibility that it was over constraint please refer to Chapter 2 of this manual Page 23 5 Advanced Options Reduction Options Run Options Algorithm 4 Symbolic BDD Reduction 1 Step Explicit State Iterated Auto Restrict Deadlocks _ Treat as errors Reduction Seed gt Empty 4 Continue Run Time _ Limited x New Reduction Manager Advanced Options FO Fic 5 1 Reduction Options panel amp Run Options panel FormalCheck uses a patented localized reduction algorithm to reduce the size of the design model relative to the property being tested 6 Among the two algorithms 1 step is used by default and the iterated algorithm is used for complex designs because it takes less memory more time to verify the design This reduction technique finds a portion of the design model on which it is sufficient to run the verification TIT REDI Bee Start As Input FiG 5 2 Reduction Manager panel Page 24 A reduction seed can be provided by the user to further speed up the verification process The user designates a candidate portion of the des
19. d Each state in which the selected signal matches the specified waveform is excluded from the verification This constraint can wisely be used for the initialization of all the input signals But to do that one should always remember that it is going to be needed to add some lines code to the original design model Example The following is a Verilog example portion of a design The reset repeat constrain can be applied to the signal reset_elevator please refer to the Figure 2 6 to initialize the signals direction and movement initialization block always reset_elevator begin if reset_elevator begin direction UP movement STOPPED end end Reset Repeat Signal main reset Select Name reset Start High m Default Transition Duration Value Start 2 1 Add forever 0 Delete Last Cycle Set Clear Duration Clear FIG 2 6 The usage of Reset Repeat Constraint Page 15 The settings on Figure 2 6 will produce a main_reset signal passed as a parameter while instantiating another module instance and thus is equivalent to reset_elevator which is high logic value 1 for 2 cranks unit of time and low logic value 0 for the rest of the verification period As the block is active only at positive values of the sig nal reset_elevator all the input signals in the block are initialized to the desired values Cranks This is the term FormalCheck uses for unit o
20. ded Reduction Manager should be employed Verification should be re run with Auto restrict or Explicit State Enumeration Note Missing Values Show the design elements signals that are irrelevant to the specific query Page 27 References 1 A J Hu Formal Hardware Verification with BDDs An Introduction IEEE Pacific Rim Con ference on Communications Computers and Signal Processing PACRIM pp 677 682 1997 2 E M Clarke and J M Wing Formal Methods State of Art and Future Directions CMU Com puter Science Technical Report CMU CS 96 178 August 1996 3 R P Kurshan Formal Verification In a Commercial Setting Bell laboratories Murry Hill NJ In Design Automation Conference June 1997 4 R H Hardin Z Har EL R P Kurshan COSPAN Springer LNCS 1102 1996 pp 61 67 5 R P Kurshan Computer Aided Verification of Coordinating Processes Princeton Univ Press 1994 6 FormalCheck User s Guide Cadence Design Systems V2 3 August 1999 Page 28 APPENDIX A System Settings to Run FormalCheck 1 To work on a UNIX machine the system administrator has to activate user s privilege to the tool FormalCheck 2 The following lines had to be added to the cshrc startup file setenv LM_LICENSE_FILE usr local etc license cadence license dat setenv CDS_INST_DIR CMC tools formalcheck2 3 setenv CDS_LIC_FILE usr local etc license cadence license dat setenv FCHECKDIR CMC tools form
21. e 46 begin if reset begin AgeA 3 d0 AgeB lt 3 d0 AgeC lt 3 d0 AgeD lt 3 d0 end else if Awon begin AgeA lt 3 d0 if reg 1 begin if AgeB lt 6 AgeB AgeB 3 dl else AgeB lt AgeB end if req 2 begin if AgeC lt 6 AgeC lt AgeC 3 d1 else AgeC lt AgeC end if reg 3 begin if AgeD lt 6 AgeD lt AgeD 3 dl else AgeD lt AgeD end end if Bwon begin AgeB lt 3 d0 if req 0 begin if AgeA lt 6 AgeA lt AgeA 3 dl else AgeA lt AgeA end if req 2 begin if AgeC lt 6 AgeC AgeC 3 d1 else AgeC lt AgeC end if req 3 begin if AgeD lt 6 AgeD lt AgeD 3 dl else AgeD lt AgeD end end Page 47 if Cwon begin AgeC lt 3 d0 if req 0 begin if AgeA lt 6 AgeA lt AgeA 3 dl else AgeA lt AgeA end if req 1 begin if AgeB lt 6 AgeB lt AgeB 3 d1 else AgeB lt AgeB end if req 3 begin if AgeD lt 6 AgeD lt AgeD 3 dl else AgeD lt AgeD end end if Dwon begin AgeD 3 d0 if req 0 begin if AgeA lt 6 AgeA lt AgeA 3 dl else AgeA lt AgeA end if reg 1 begin if AgeB lt 6 AgeB lt AgeB 3 dl else AgeB lt AgeB end if req 2 begin if AgeC lt 6 AgeC lt AgeC 3 d1 else AgeC lt AgeC end end end endmodule age VERIFICATION RESULTS Page 48 Query 1 Query NoAck_Unless_Req Property NoAc
22. e GUI version of FormalCheck tool Note If anyone already has some experience with FormalCheck can skip this chapter and can have a look at the chapter 4 stepwise procedure in order to just remind him herself of the tool FormalCheck Project A FormalCheck project is a container directory structure that holds all information relevant to the verification 6 One may start the tool either by opening an existing project or by creating a new one A project fpj file contains the following information pointer to the model design necessary information to compile the design i e HDL language top level entity module name hierarchical dependencies etc data structure built for the verification queries properties constraints result of the verification of the queries Queries properties constraints Existing model checkers use some form of CTL Computation Tree Logic to define properties 3 The idea of using a logic was discarded my FormalCheck because this approach is some times hard to be defined for the general users In FormalCheck each property is defined using one of a small set of templates each with a clear intuitive and simple semantics and correctly as impressive as the class of omega automata Of course what is gained in simplicity is lost in flexibility 3 A property is verified if and only if no failures are found after exploring all reachable states and possible input combina
23. eA assign C It A C ge A assign C ge B AgeC gt AgeB assign C It B C ge B assign C ge D AgeC gt AgeD assign C It D C ge D assign D ge A AgeD gt AgeA assign D lt A D ge A assign D ge B AgeD gt AgeB assign D It B D ge B assign D ge C AgeD gt AgeC assign D It C D ge C Vbl Vbl Vbl Vbl Vbl Vbl Vbl Vbl Vbl Vbl Vbl Vbl 1760 1760 1760 1760 1760 1760 1760 1760 150 1760 150 1760 Page 44 Il Default Selections Il assign selA pri0 lastGrant IDLE amp reqA assign selB priO lastGrant IDLE z reqA z reqB assign selC pri0 lastGrant IDLE z reqA z reqB amp reqC assign selD pri0 lastGrant IDLE 6 reqA amp reqB z reqC amp reqD Ownership Selections assign selA_pril lastGrant GrantA amp reqA assign selB_pril lastGrant GrantB amp reqB assign selC_pril lastGrant GrantC amp reqC assign selD_pril lastGrant GrantD amp reqD Il Round Robin Selections Il assign selA pri2 1 lastGrant GrantB z reqB amp rot Il reqC z reqD assign selA pri2 2 lastGrant GrantC amp reqC z rot amp reqB l rot amp reqD assign selA pri2 3 lastGrant GrantD amp reqD amp rot l reqC z reqB assign selA pri2
24. ery c Wed Sep 22 05 49 05 1999 ifndef Int define Int int endif define String int define BYTESIZE 8 ifdef HDR extern endif struct struct struct Int clk unsigned char U clk 2 Int reset unsigned char U reset 2 struct Int _prev0 1 91179 cik environment struct Int fi U2r state Int fi U3 r state struct Int 9983 fi VDS state 1 Int 9982 fi VDS state 1 Int _9985__VD5_state__0__1__0 Int _9984__VD5_state__0__1 1 struct Int 9923 fi SR_OUT_state__0 Int 9922 fi SR OUT state 1 Int 9925 SR OUT state 0 Int 9924 SR OUT state 1 Int 9911 fi SR ST state 0 Int 9910 fi SR ST state 1 struct Int stO 9913 SR ST state 0 struct Int stl 9912 SR ST state 1 It fi T90 Int T90 unsigned char U T90 2 Int 9926 fi Zl state 1 Int 9928 Z1 state 1 H6 I5 HIA road A struct FILE CONTINUES Page 35 APPENDIX C Design Tips for verification purpose One may remember the following One should not use two signals to activate the events in an always block correct always posedge clk incorrect always posedge clk amp amp reset nitialization is not supported by FormalCheck We used another extra signal reset propagated through all the modules The reset signal is made active high for only 2 cranks of time and low for ever Reset Repeat constraint The always block activated by the positive res
25. es Both Enabling and Fulfilling Condition are required for Strong Liveness property The Enabling Condition need not be satis fied along the failure cycles The Enabling Condition may be satisfied before the fail ure cycle is entered When Enabling Condition is absent the Fulfilling Condition is active until it is dis charged if ever Computationally not simple Computationally simpler Constraint In FormalCheck design constraints are defined using a companion set of templates property templates and constraint templates are paired and each check on a design model is performed in the context of a set of properties and constraints termed query 3 All the constraints belonging to the project are listed in the Constraint Library panel please refer to Figure 3 3 Constraints limit the state space of a design model Fic 2 4 The Effect of Constraints in the Reachable State Space 6 Page 13 Let us assume that the Figure 2 4 is the total reachable space of a variable X for some design model The constraint to be added as X is true always The area with the thick boundary is then excluded from verification as it belongs to negative X If we put constraints to some signals which includes a feature of the design then that will not be verified and this situation is called Overcon strained WARNING We should be careful about the model being not OVERCONSTRAINED There are 2 types of general co
26. et signal contains the assignments for the initialization Note that while specifying the above reset signal one is going to introduce another always block concurrent block With two always blocks in the same module one should be careful to avoid reassignment of the same signal in the 2 concurrent blocks This may greatly affect the verification f design contains internal nondeterministic signals they should be converted to primary input of that module because FormalCheck does not support nondeterministic internal signals FormalCheck does not support real enumerated data types for Verilog code But it is possible to use the key word define For example define no cars 0 define car waiting 1 define cars passing 2 define traffic status no cars car waiting cars passing Note that the above piece of Verilog code is used just outside the modules please refer to the Verilog example in Appendix D Page 36 APPENDIX D The Arbiter Example Courtesy of Cadence for educational purposes only Description of the Arbiter to be verified Req 8 0 Rot Ack 3 0 Ck Reset RegB 0 FiG 3 Arbiter Circuit Block Diagram The circuit arbitrates a shared resource among 4 clients It features a selectable clockwise or coun ter clockwise polling direction for either a round robin or an aged based arbitration scheme The circuit also features the ability to
27. f time Pros and Cons of using Constraints Constraints limit the state space of a design to be verified Constraints can significantly reduce the run time One can limit the input by using constraint on it and thus restrict the design Any error in the restricted design is also an error for the total design So running a severely restricted design can give a good early warning concerning the computational com plexity of the unrestricted design Mutually inconsistent constraints can compromise the verification by preventing an important design flaw being exposed Mutually inconsistent While individually taken works fine But simultaneous use impose contradictory results Checking for Overconstraint When the properties are overconstraint the verification result comes as Vacuous It means the Enabling Condition of the property was never satisfied Because 1 The Enabling Condition was wrongly formed 2 The verification engine could not reach a state where the Enabling Condition was satisfied 3 Inconsistent definitions while forming constraints Like X21 amp amp X 0 The following are some procedures to solve problems with constraints The only conclusive way to check that a design is not overconstraint is to convert all con straints to their corresponding properties and verify these properties on the model that derives the inputs of the given design If DVACCHECK please refer to page 8 8 on For
28. has to select the desired query from the Name column Figure 3 5 and press the verify button FormalCheck will do the rest about verification Page 21 4 Post Processing Analysis The Result column of the Query Manager may contain eight possible outcomes The follow ing is the short description 1 New Indicates a new query no attempt has been taken to verify it 2 Failed Error has been found in the design and an error track is available for debugging 3 Verified The query was previously verified 4 Running A verification procedure is currently being processed 5 Terminated The verification process is incomplete user or some other intervention 6 Scheduled The verification is scheduled by the Schedule Manager refer to the Query pull down menu 7 No Error No failures have been found but this is not same as verification It sometimes happens while using the auto restrict algorithm to quickly verify the design 8 Vacuous The Enabling condition is never satisfied the reason why the Fulfilling condition was never checked vurslon H Y 0 Fri Fob 27 1626 EST 1931 Select Signals Fad Files Help FIG 4 1 The Wave Form Window ODAN If the result is Failed then the waveform viewer the Output Display Analysis Tool ODAN is very useful to finish the post verification analysis FormalCheck creates 2 files Page 22 HDR and REC in the query dire
29. ign model by marking its boundary signals Start As Input This option disconnects all signals marked as Start As Input from the driving ex pressions and turns them into primary inputs If some driving expressions really in need of some of these signals the algorithm will reinstate them cutting the design model signals at an alternate point instead 6 Note Iterated reduction does not support Auto Restrict verification algorithm Reduction Seed is recommended when Iterated Algorithm is used Through the Make Input option some signals can be disconnected almost permanently from their driving expressions and thus treated as primary inputs This is the way to isolate a portion of the design model In such a condition if FormalCheck verifies a query it means that the same query would also be verified in the full design model Note Make Input sometimes creates problems in error tracing if FormalCheck returns failure Through the option Keep Active one can make sure that the signal is not going to be exclud ed from the verification no matter what Note If Keep Alive is used it increases the computational cost Clear option removes any reduction designation from a design element New Features AutoCheck AutoCheck is applied as a preverification procedure It is used in the early design stages to quickly run on queries in order to find early design bugs AutoCheck is not a complete verification pr
30. is the list of files created in the directory called lt priject_name gt the name used for the project DIRECTORY crd_project fpj E ea ece concordia ca projec vg mi HY formalCheck EXAHPLES TEST cr ne mi khanGdea crd project fpj BSS gt 1s Eventualities Query 1 README build stderr environment __ENY sr Query 3 build out environment sr fcheck mi khanGdea crd_project fpj BST gt Fic 1 SnapShot of the Directory crd_project fp Contents of the file README All the file contained in this directory and below are considered part of the FormalCheck project Changing anything in this directory or its children could result in corrupting your verification results Page 31 ece concord ia ca DIRECTORY Query_1 project hvg mi ormalCheck EXAHPLES TEST cr raj mi_khan dea Ouery 1 ls DOTU environment_ sr environment ENV sr q q query U last mi_khan dea Query_1 gt 1s all total 479 druxr x druxr x druxr x ru r mi khan mi khan mi khan mi khan mi_khan mi_khan mi_khan mi_khan mi_khan mi_khan mi_khan mi_khan mi_khan mi_khan mi_khan 3 7 2 1 1 1 1 1 1 1 1 1 1 1 1 query an query c query lines query rf query sr verify out verify stdout 512 512 1024 24307 288 1811 25 25 354900 50802 1658 28500 740 2833 2337 14 31 14 39 07 09 14 31 14 31 14 31 14 31 07 09 05 48 05 48 1
31. ks Type Always Always arb ack 0 Unless After arb req gt 1 amp amp arb ck rising Options Fulfill at discharge Clock Constraint ck Signal arb ck Extract No Default Yes Start Low 1st Duration 1 2nd Duration 1 Reset Constraint reset Signal arb reset Default Yes Start High Transition Duration Value Start 2 1 forever 0 RUN OPTIONS Reduction Technique 1 Step Reduction Seed Empty Page 49 Verification Query NoAck_Unless_Req VERIFIED Wed May 10 01 15 50 2000 on server richards Query Data 1 32e3 combinational variables 1 02e3 Possible input combinations per state 20 State variables 2 1e 06 states Verification Data 5 states reached State variable coverage 20 variables 57 50 average coverage Search Depth 5 Real time 0 minutes 23 seconds Memory Usage 5 99654 megabytes EXPRESSION MACROS AckA arb ack 0 1 AckB arb ack 1 1 AckC arb ack 2 1 AckD arb ack 3 O AH Reqs arb reg 15 CkRising arb ck rising Multi Acks arb ack 3 arb ack 2 arb ack 1 arb ack 0 gt 1 RegA arb req 0 1 ReqB arb req 1 ReqC arb req 2 1 ReqD arb req 3 ResetDone arb reset finished Query 2 Query Only_One_Ack There are 4 request inputs and 4 acknowledge outputs in this design We want to verify that the arbiter never acknowledges more than one request at a time Ensure P1 NEVER Ack1 Ack2
32. lCheck on NCD terminals APPENDIX B FormalCheck File Description Contents of the file README Contents of the file verify stdout Contents of the file verify out Contents of the file query c APPENDIX C Design Tips for verification purpose APPENDIX D The arbiter example Description of the Arbiter to be verified Arbiter Basic Specification RTL design Page 3 25 25 26 26 26 27 28 29 29 29 30 31 31 31 32 34 35 36 36 37 37 37 39 39 Page No VERIFICATION RESULTS 49 Query 1 49 Query 2 50 Query 3 52 Query 4 53 Query 5 56 Page 4 Preface Audience This guide is written for research students and design engineers who will use FormalCheck as a tool of hardware verification for the first time It summarizes the available material FormalCheck User Guide FormalCheck on line Manual etc that the manufacturer has provided with the tool Page 5 1 Introduction Formal verification means a mathematical proof which assures that a property holds of a design model The need for correct designs in safety critical applications coupled with the major cost associated with products delivered late are the two of the main reasons behind the recent popular ity of formal hardware verification The verification methods require considerable time and expertise to verify even fairly simple systems As a result practical application has been limited to a few domains such as security and safety critical sy
33. lways Liveness 4 Eventually Ev lways Strong Liveness ENSURE After trafic_light direction 0 Eventually traffic light direction D 1 Unless Options Fulfill Delay a Duration Of Edge FiG 2 3 Property panel with an Eventual Property a Eventually The Fulfilling Condition must eventually become true However it does not have to remain true all the time The above eventual liveness property can be written in words as follows After direction 0 GREEN Eventually direction 0 RED b Eventually Always This is like steady state Eventually property The Fulfilling Con dition must remain true Steady State at the time of discharging It does not have to reach steady state within any time limit and may become true and then false several times before it reaches the steady state 6 c Strong Liveness Strong liveness differs from the other liveness property by its Enabling Condition Here the Enabling Condition is allowed to be checked repeatedly upon the failure of fulfilling condition Page 12 Table 2 The Difference Between Strong Liveness and Eventually Strong Liveness Eventually Format If Repeatedly event A Enabling Condition Eventually event B Fulfilling Condition Format After event A Enabling Condition Eventually event B Fulfilling Condition The Enabling Condition need to be satis fied along the failure cycl
34. malCheck User s Guide reference no 6 fails one can apply DVACCHECK run option Query panel to successive sub sets of the constraints until a small mutually inconsistent subset is identified One can check Missing value Report for values some signals never attain Page 16 3 Stepwise Procedure of Verifying a Design in FormalCheck Step 1 Initializing Step Forma Ghack FIG 3 1 Design Model Panel for Step 1 PROJECT NEW OPEN This will invoke Design Model Panel Name of the project has to be provided Title Design language has to be chosen VHDL or Verilog For VHDL vhd vhdl Root Entity mandatory Architecture mandatory For Verilog v Root Module mandatory Build Option optional ADD This will invoke Select Design File Panel A design file same language chosen before has to be selected Option SAVE LIST This will create a text file that contains a list of file names of the design model files that are currently displayed on the panel Option NOTES This will allow to write notes about the project Page 17 Step 2 Saving the Project PROJECT SAVE SAVE AS FormalCheck uses the extension fpj for the files containing the project The user has to enter a name for the file Step 3 Opening a file optional FILE OPEN This is not a mandatory step for the verification process But it allows to debug syntax error edit the design Verilog
35. me traffic_light2 define WAITING define PASSING Properties waiting car eventually module traffic 1 cars reset initval directio 1 0 ca Constraints reset Constraints Query Mew 38 Edit Delete Default FiG 3 3 The Constraint Library Panel for Step 5 Step 5 Adding a Constraint PROJECT CONSTRAINT LIBRARY This will invoke Constraint Library panel Figure 3 3 Constraints limits the state place of a design model that is verified 6 Note Please refer to the previous chapter for more details on CONSTRAINTS Page 19 Step 6 Create Edit Query QUERY NEW EDIT A query must contain one or more properties The procedure to write properties are explained in the previous chapter A new query also automatically contains any constraints marked as default in the constraint library Additional constraints can be added or removed manually Default Constraint A default constraint is a constraint that will be automatically applied to all new queries in a project A constraint marked as default will not be applied to any pre existing queries unless specified manually A non default con straint can be manually added to any query 6 Allows to keep notes on Project Query Constraints and State Variab Query Query Name ElevatorDoor List of Properties tor the query named gt Properties DoorCloseWhileMove always ElevatorDoor Constraints cik List of
36. me Always arb rot stable Options None Constant Constraint am zero Signal arb am Default No Value 0 To make the arbitration mode non age based Page 54 Clock Constraint ck Signal arb ck Extract No Default Yes Start Low 1st Duration 1 2nd Duration 1 Reset Constraint reset Signal arb reset Default Yes Start High Transition Duration Value Start 2 1 forever 0 RUN OPTIONS Reduction Technique 1 Step Reduction Seed Empty Verification Query Acka VERIFIED Wed May 10 01 17 44 2000 on server richards Query Data 557 combinational variables 256 Possible input combinations per state 16 State variables 6 55e4 states Same as prior verification Wed May 10 00 10 16 2000 Verification Data Reachable space 495 states 495 states reached State variable coverage 19 variables 100 0096 average coverage Search Depth 10 Real time 0 minutes 11 seconds Memory Usage 2 32653 megabytes Page 55 Query 5 uery Seq Clockvvise A ged This is a Liveness property To verify that the sequence for Clockwise Aged arbitration is AckA gt AckB gt AckC gt AckD Also note the use of state variable called Seq Property ClockwiseAged Type Eventually After All_Reqs amp amp Seq 0 amp amp CkRising amp amp arb ack 0 Eventually Seq Options None Group Constraint ReqA Constraints ReqA_cant_occur ReqA persists Default Yes Group Constraint
37. nstraints 1 Safety never always ii Fairness eventually strong fairness Safety constraints are the constraints applied with the safety property and the fairness con straints are applied with the liveness property of the query Constraint SHORTCUTS Constraint Shortcuts are provided by the tool to use as ready made constraints There is also general constraint in order to define any other kind of constraints Shortcuts are only allowed for the primary inputs 1 Assignment ii Clock iii Constant iv Reset Repeat 1 Assignment An input signal always takes the value of an expression The expression may contain internal signals but the signal must be a primary input il Clock This is a very important constraint It is an oscillating signal and FormalCheck detects the rising and falling edge of the signal Example design CLK rising Verilog Root module signal name Signal main clk Select Name cik Start Low 1st Duration 1 end Duration 1 m Default Fic 2 5 The usage of Clock Constraint Page 14 During the verification this constraint can simulate the behavior of the clock ticks iii Constant It assumes a signal to have a constant value iv Reset Repeat This a very useful constraint It is used to constrain a signal to a user defined waveform The waveform may be an one shot waveform or a repeat periodic one A signal is first selected then a waveform is specifie
38. ocedure as it does not cover the entire state space further reference page 5 9 in user s manual command formalreadthemanual Macro Macro is the shorthand version of any expression It is done by the expression editor The procedure is to type or insert any expression and give it a name after pressing MakeMac ro Clock Extraction While imposing clock constraints the feature Clock Extraction can be used to reduce verification time in some cases This option should be tried if the design is syn chronous with respect to a single clock edge Script Interface FormalCheck supports user defined UNIX script to perform tasks like automatically generating constraints see page 8 7 in users manual Page 25 IMPORTANT BUILD OPTIONS D lt parameter gt lt value gt Allows the value of a Verilog parameter to be set to a different smaller value to reduce the state space This is necessary for parenthesized RAMs ROMs FIFOs and queues W lt path gt Specifies a single directory to which all the files will be created by FormalCheck ADVANCED OUERY RUN OPTIONS L lt mb gt Specifies a limit on memory used mb is memory in megabyte represented in floating point notation 80 limit of user accessible memory is recommended The verification be gins a wrap up sequence time consuming when the memory is finished to generate re ports hardlimit lt mb gt Stops verification without the warp up
39. p reqC amp rot amp D t A amp A_ge_B Il rot amp B lt A amp A_ge_D assign selA pri3 3 lastGrant GrantB amp reqB amp rot amp C It A amp D It A ll rot amp A ge DZ A ge C assign selA pri3 reqA z aged amp selA pri3 1 selA pri3 2 selA_pri3_3 assign selB pri3 1 lastGrant GrantA amp reqA amp rot amp B ge C amp B_ge_D Il rot amp D It B amp C It B assign selB pri3 2 lastGrant GrantD amp reqD amp rot amp A It B amp B ge C Il Page 45 rot amp C It B amp B_ge_A assign selB_pri3_3 lastGrant GrantC z reqC z rot amp D It B amp A_It_B ll rot amp B ge A amp B ge D assign selB_pri3 reqB amp aged amp selB_pri3_1 selB pri3 2 selB pri3 3 Fix assign selC_pri3_1 lastGrant GrantB amp reqB amp rot amp C_ge_D amp C_ge_A Il assign selC_pri3_1 lastGrant GrantB amp reqB amp rot amp C_ge_D amp C_ge_A Il rot amp A It C amp D_It_C assign selC pri3 2 lastGrant GrantA amp reqA amp rot amp B It C amp C ge D Il rot amp D It CEC ge B assign selC pri3 3 lastGrant GrantD amp reqD amp rot z A It C amp B It C Il rot amp C ge B amp C ge A assign selC_pri3 reqC amp aged amp selC_pri3_1 selC_pri3_2 selC_pri3_3 assign selD_pri3_1 lastGrant GrantC amp reqC amp
40. reqA amp aged amp selA_pri2_1 selA_pri2_2 selA_pri2_3 assign selB_pri2_1 lastGrant GrantC amp reqC amp rot reqD z reqA assign selB_pri2_2 lastGrant GrantD z reqD z rot z reqC rot amp reqA Fix assign selB_pri2_3 lastGrant GrantA amp reqA amp rot Il reqD amp reqC assign selB_pri2_3 lastGrant GrantA z reqA z rot assign selB_pri2 reqB amp aged amp selB_pri2_1 selB_pri2_2 selB_pri2_3 assign selC_pri2_1 lastGrant GrantD amp reqD amp rot l reqA amp reqB assign selC_pri2_2 lastGrant GrantA z reqA z rot z reqD l rot amp reqB assign selC_pri2_3 lastGrant GrantB amp reqB amp rot l reqA z reqD assign selC_pri2 reqC amp aged amp selC_pri2_1 selC_pri2_2 selC_pri2_3 assign selD pri2 1 lastGrant GrantA amp reqA z rot l reqB amp reqC assign selD pri2 2 lastGrant GrantB amp reqB z rot amp reqA Il rot amp reqC assign selD pri2 3 lastGrant GrantC amp reqC amp rot Il reqB amp reqA assign selD_pri2 reqD z aged amp selD pri2 1 selD_pri2_2 selD pri2 3 Age Based Selections assign selA pri3 1 lastGrant GrantD z reqD z rot amp A ge B amp A_ge_C ll rot amp C It A amp B_It_A assign selA pri3 2 lastGrant GrantC am
41. rify out 9771 Verification Server enterprise ece concordia ca 9771 SunOS enterprise ece concordia ca 5 5 1 Generic sun4u sparc cospan I CMC tools formalcheck2 1 SOLARIS include environment sr Ks caseonedfit varlines nmi missin gasgn nocaseonedfiterr shortfloat 3 status dupstvars hotunroot hotback Msuperset b q csplit pthreshold 1e3 50 rmc flow disconnect slowdisconnect 4 query sr cospan Version 8 23 24 Bell Laboratories 27 May 1998 Iterative run for option q Iteration 0 4 4 cospan Version 8 23 24 Bell Laboratories 27 May 1998 sr E I CMC tools formalcheck2 1 SOLARIS cospan caseonedfit varlines nmi missingasgn nocaseonedfl terr shortfloat 3 status dupstvars hotunroot hotback Msuperset pthreshold 1e3 50 flow disconnect slowdisconnect 4 I CMC tools formalcheck2 1 SOLARIS cospan I CMC tools formalcheck2 1 SOLARIS include environment_ sr Ks caseonedfit varlines nmi missingasgn nocaseonedfiterr shortfloat 3 status dupst vars hotunroot hotback Msuperset b reduction pthreshold 1e3 50 flow disconnect slowdisconnect 4 query sr caseonedfit varlines nmi missingasgn nocaseonedfiterr shortfloat 3 status dupstvars hotun root hotback Msuperset pthreshold 1e3 50 flow disconnect slowdisconnect 4 caseonedfit varlines nmi missingasgn nocaseonedfiterr shortfloat 3 status dupstvars
42. s LLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLII wire A ge B A It B ge C A It C A ge D A It D wire B ge A B It A B ge C B It C B ge D B It D Page 43 wire C_ge_A C lt A C ge B C It B C ge D C It D wire D ge A D It A D ge B D It B D ge C D It C wire selA priO selA pril selA_pri2 selA pri3 wire selB pri selB_pril selB_pri2 selB_pri3 wire selC priO selC_pril selC_pri2 selC_pri3 wire 5610 priO selD_pril selD_pri2 selD pri3 wire selA_pri2_1 selA_pri2_2 selA_pri2_3 wire selB_pri2_1 selB_pri2_2 selB_pri2_3 wire selC_pri2_1 selC_pri2_2 selC_pri2_3 wire selD_pri2_1 selD_pri2_2 selD_pri2_3 wire selA_pri3_1 selA_pri3_2 selA_pri3_3 wire selB_pri3_1 selB_pri3_2 selB_pri3_3 wire selC_pri3_1 selC_pri3_2 selC_pri3_3 wire selD_pri3_1 selD_pri3_2 selD_pri3_3 wire reqA reqB reqC reqD wire selA selB selC selD assign reqA req 0 assign reqB req 1 assign reqC req 2 assign reqD req 3 assign A_ge_B AgeA gt AgeB assign A It B A ge B assign A ge C AgeA gt AgeC assign A It C A ge C assign A ge D AgeA gt AgeD assign A It D A ge D assign B ge A AgeB gt AgeA assign B_It_A B_ge_A assign B_ge_C AgeB gt AgeC assign B_It_C B_ge_C assign B ge D AgeB gt AgeD assign B_It_D B_ge_D assign C ge A AgeC gt Ag
43. s algorithm propagates constants contained in the design or in the input assumptions to further reduce the design An additional level of reduction can be achieved by Iterative Reduction algorithm It takes an attempt to find a small portion of the design that can be used to verify the current query This tech nique guarantees that queries proven to be true on the small portion of the design would also be true for the entire design This algorithm can be run with or without a user supplied starting point reduction seed and can reduce the state space of the design by several orders of magnitude allowing larger designs to be verified This tool checks if a change by the user could affect the outcome of the verification If not it marks the query as proven by the previous runs This unique capability reduces the regression time Through FormalCheck s Back Reference utility a click on an error in the waveform pops up the source with the cursor on the line that caused the error HDL Code gt Automatic Back Reference to error FormalCheck Design Verified FIG 1 3 FormalCheck Verification Cyde 6 Page 8 2 Verifying Techniques used in FormalCheck To use either the Graphical User Interface GUI or the Command Line Version one must aware of the functionality of the each step to wisely use the different advanced options provided by FormalCheck The following literature refers to th
44. scription Top RTL Level for arbiter eee eere ik ib 3 ii 33 3 SR E SR E SR I K K K K SR kk SR SR o K k ok sk sk ok ok ok kK K K K K K K K LLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLELLLLELLLII 7i circuitarb v Description Arbiter for 4 clients H kkk kokk ke ik ik ib 3 3333 SR SR E SR E SR c K K K K SR R R SR SR o ok k ok ok sk sk ok ok k K ok K K K K K 7i Files arb h include arb h Page 39 dpath v Decision logic in a small datapath fsm v_ FSM for arbiter llage v State to compute the age of a client s request arb v Top RTL level for arbiter arb fpj Project file arb fpj ascii gt text mode project file Il LLLLLLLLLLLLLLLLLLLLLLLLELLLLLLLLLLLLLLLLLDLLLLLLLLLLELLLLELLLLLLLLLLI Il Brief Functional Description Il X EEE E EE E ee E E E E E E E E E E E E E E E E K E E KE E K K oK SR S kk ik ke k sk sk ok ok ok ok ok ok ok KK KK K K K K Arb v arbitrates a shared resource among 4 clients Il A Request Reg j is eventually acknowledged Asserting Ack j after a request is issued may take as little as 1 clock cycle or as many as X clock cycles It is expected from the environment that each Req_ j asserted is eventually withdrawn Removing Req j after the acknowledment is issued may take as little as 1 clock cycle or as many as Y clock cycles Each Ack_ j goes away 1 clock cycle after Req_ j is withdr
45. scription of what explained in source 1 5 At last the command formalcheck will invoke the graphical user interface of the tool Page 29 Running FormalCheck on NCD terminal Before proceeding with the following steps one should remember that it is not a complete solution concerning the problem of FormalCheck about executing on the NCD terminals But it allows one to run the tool for a certain amount of time or certain amount of activity by removing the file called formalcheck created by the tool on the current directory which is done in step 2 1 Place the appropriate lines paths mentioned in the previous topic at point 2 Setting the environment in the cshrc which is located under the main directory ex home user name cshrc Note make sure to source cshrc before proceeding if anyone wants to run the applica tion before login again as follows source cshrc 2 Create a new file with any desired name for example runFC and place these lines in it bin sh rm rf formalcheck CMC tools formalcheck2 3 SOLARIS formalcheck 3 Make sure that the file in Step 2 has Execute permission by doing the following command chmod 755 file name 4 Now youcan run the program by running the FormalCheck executable or by creating an Alias for that file in the cshrc as follows alias any name u like home user name file name in step 2 Page 30 APPENDIX B FormalCheck Files Description The following
46. seguence DVACCHECK This option verifies if really a query is vacuous If the result with this option is verified then the query is vacuous If a bad cycle is found then the query is not vacuous THREE VERIFICATION ALGORITHMS e Symbolic State Enumeration Ordered Binary Decision Diagrams Symbolic BDD Explicit State Enumeration Auto Restrict Symbolic BDD is generally useful for verifying models with a very large set of States But BDDs become extremely large for the design models with arithmetic expres sions Explicit State Enumeration is recommended for designs with fewer than 1000 pri mary inputs state and which contain a large number of arithmetic expressions It can find error in the design faster than the symbolic BDD This algorithm is preferable for liveness property Auto Restrict attempts to narrow down the portion of the design where a failure is likely to be found It speeds up the verification But if may give the result No Errors In this case the verification has to be performed again with any of the previous two algo rithms Page 26 A Recommended Procedure for Verification At first Symbolic BDD should be used with a time limit The verification can stop for three reasons An error can be found the time limit can be expired or the verification can be complete For the first two reasons one can do the following Missing value report should be checked Restriction should be ad
47. stems where ethical or legal requirements demand the highest assurance of correctness regardless of the cost 1 Two well established approaches to verification are model checking and theorem proving Theo rem proving means that given a set of axioms and a theorem formulated in some logic there exists a proof generated by the inference system On the other hand model checking is a tech nique that relies on building a finite model of a system and checking that a desired user defined property holds in the model 2 FormalCheck is a model checker designed to help alleviate the functional verification bottleneck Queries Properties Constraints Model Checking Engine Pass or Fail FIG 1 1 FormalCheck Verification procedure 3 FormalCheck supports the synthesizable subsets of Verilog and VHDL hardware design lan guages The source code does not need to be modified for the sake of verification The user sup Page 6 plies FormalCheck with a set of queries to be verified on the design model The queries are simply statements formalizations of important behaviors described in the specification FormalCheck aids the user by automatically back referencing each error to the offending line to the source code The errors can be fixed and the source recompiled without leaving the tool The tool explores all possible input scenarios guaranteeing that no bugs are missed for la
48. tions 6 Page 9 Query Name traffic_light2 Property ENABLING CONDITION Property Name test Type Safety v Never Always Liveness 4 Eventually iz EvAlways ENSURE FULFILLING After traffic light cars 1 CONDITION Eventually traffic light direction 1 Unless traffic lightinitval 1 Options _ Fulfill Delay Duration of Edge DISCHARGING CONDITION FiG 2 1 Property Panel showing essential features The above figure defines a property which checks that after each time the designated enabling condition is enabled the designated fulfilling condition holds continuously unless the discharging condition becomes true 3 Fulfill at Discharge option is used when it is necessary to require the Fulfilling Condition con currently with the Discharging Condition Table 1 Explanation of the option Fulfill at Discharge Regular Fulfil and Discharge condition With option Fulfill at Discharge Figure 2 1 Example Always A fulfilling Condition Example Always A Fulfilling Condition Unless B 1 Discharging Condition Unless After B 1 Discharging Condition Explanation The Fulfilling Condition will Explanation The Fulfilling Condition will discharge when B 1 discharge when B becomes equal to 1 while A still holds Page 10 Property safety liveness 1 Safety This kind of property ensures that nothing bad happens The Safety proper
49. ty fails if the undesired behavior is exhibited in any state which is reachable with the phase state active 6 There are two kinds of Safety property in FormalCheck a Never b Always Name of the Signal 0 is equvalent to green according to the design traffic_light direction 0 0 amp amp traffic_light direction 1 0 d Relation Operator Root Module Name FiG 2 2 A property in FormalCheck Light is never green in both directions a Never FormalCheck will explore all possible inputs and reachable states to verify that the condition can NEVER occur 6 Figure 2 2 shows how one can specify a property in FormalCheck This can be done either my writing manually or with the help of buttons signal selection b Always FormalCheck will explore all possible inputs and reachable states to verify that the condition can NEVER be false 6 2 Liveness This type of property guarantees that eventually something good happens A Liveness property fails if there exists a sequence of inputs which can postpone the required behavior indefinitely Since all designs are finite state a liveness failure amounts to finding a cycle of reachable states where the required behavior does not occur 6 FormalCheck defines three kinds of liveness property a Eventually b Eventually Always c Strong Liveness Page 11 Property Property Name Evantuality Test Type Safety v Never A

Hands-On Manual to Formal Check (V2.3)

Contents

Download Pdf Manuals

Related Search

Related Contents