This is the fourth article in this series (click here for the series index) describing the IBM PowerPC™ 405 synthesizable core and peripherals and will cover functionally and formally verifying the synthesized gate-level structural Verilog netlist.
Firstly let us look at the two main classes of verification:
- Formal Verification
- Functional Verification
Luckily for us the coreKit provides scripts and support for automating both activities. The completed netlist (with scan chains, more on their importance later) can be put into the same simulation framework that verifies the RTL is fully functional. The completed netlist can also be formally verified against the source RTL by using Synopsys Formality™.
Formal Verification
The relevant part of the instruction manual (docs/405_ivug.pdf) is:
Chapter 9: Gate-Level Verification
So for the following process assume you have used this series of articles to synthesize a PowerPC™ 405-S core with scan chains using the Artisan PDK and the files in the list below are in their correct locations.
You will need the following:
- A synthesized gate level netlist in structural verilog (typically ./dc/netlist/PPC405F5V1_dft.v)
- Your technology library in Synopsys DB form (if you are following the supplied Artisan flow with SRAMs it is ./tech_lib/artisan_13lvfsg/syn/slow.db)
- Synopsys Formality™, Synopsys' premier formal equivalence checker
From the ./fm directory in the current workspace:
./run_fm.gate ../src/ ../tech_lib/artisan_13lvfsg/syn/slow.db ../dc/netlist/PPC405F5V1_dft.v $SYNOPSYS
Output:
Assuming you entered the command correctly Formality™ should start and the process will begin by synthesising the original RTL. This will produce a large number of warnings but in this case this is normal and expected.
It then sets a few constants disabling the scan mode in the design:
set_constant ref:/WORK/$MODULE/TESTC405SCANENABLE -type port 0 Set 'ref:/WORK/PPC405F5V1/TESTC405SCANENABLE' to constant 0 1 set_constant impl:/WORK/$MODULE/TESTC405SCANENABLE -type port 0 Set 'impl:/WORK/PPC405F5V1/TESTC405SCANENABLE' to constant 0 1
It now checks the designs and issues warnings for the RAM models.
[A “black box” is the term for a section or module of the circuit that is not visible to the tool so it is warning that it cannot verify the contents.]
Status: Checking designs...
Warning: Design ref:/DATARAM_64X34/dataram_64X34 is a black box and there are cells referencing it (FM-160)
Warning: Design ref:/SRAM256X46/sram256x46 is a black box and there are cells referencing it (FM-160)
Warning: Design ref:/SRAMBYTWR512X128/sramBytWr512x128 is a black box and there are cells referencing it (FM-160)
Warning: Design ref:/SRAM512X8/sram512x8 is a black box and there are cells referencing it (FM-160)
And finally compares the design at the matching points, producing this worrying looking output:
Status: Verifying...
....
Compare point C405TESTSCANOUT0 failed (is not equivalent)
Compare point C405TESTSCANOUT1 failed (is not equivalent)
Compare point C405TESTSCANOUT2 failed (is not equivalent)
Compare point C405TESTSCANOUT3 failed (is not equivalent)
Compare point C405TESTSCANOUT4 failed (is not equivalent)
Compare point C405TESTSCANOUT5 failed (is not equivalent)
Compare point C405TESTSCANOUT6 failed (is not equivalent)
.
Compare point C405TESTSCANOUT7 failed (is not equivalent)
.
********************************* Verification Results *********************************
Verification FAILED
ATTENTION: RTL interpretation messages were produced during link
of reference design.
Verification results may disagree with a logic simulator.
ATTENTION: 8 failing compare points have unmatched undriven signals in their
reference fan-in. To report such failing points, use
"report_failing_points -inputs unmatched -inputs undriven".
8 such failing compare points are directly undriven primary output ports.
To report directly undriven failing primary output ports, use
"report_failing_points -point_type directly_undriven_output".
To suppress verification of directly undriven primary output ports, use
"set_dont_verify_point -directly_undriven_output".
To read about undriven signal handling, use
"man verification_set_undriven_signals".
----------------------------------------------------------------------------------------
Reference design: ref:/WORK/PPC405F5V1
Implementation design: impl:/WORK/PPC405F5V1
16662 Passing compare points
8 Failing compare points
0 Aborted compare points
0 Unverified compare points
----------------------------------------------------------------------------------------
Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL
----------------------------------------------------------------------------------------
Passing (equivalent) 1204 0 0 0 578 14679 201 16662
Failing (not equivalent) 0 0 0 0 8 0 0 8
Not Compared
Clock-gate LAT 1 1
****************************************************************************************
Info: Formality Guide Files (SVF) can improve verification success by automating setup.
0 However, don't be downhearted! All Formality™ has done is its job and spotted a difference: the scan chains you inserted during the compile are not present in the source RTL. So ignoring the scan chains, as far as the tool can tell, this is the design you wanted the synthesis tool to manufacture!
Functional Verification
This is described in the same section of the manual as Formal Verification. The prerequisite is a fully functioning RTL verification environment - if it didn't work on the RTL it isn't going to on the netlist.
The relevant files are:
- sim/testbench/p405s_test_top.v - this is the Verilog file containing the top level testbench. It contains a very useful parameter: parameter simulation_cycle = 100; near the top of the file which sets the whole simulation speed in terms of the clock applied to the CPU (not the PLB). It is also sensitive to a parameter called GATE_SIM. This changes the behavior of the testbench to accommodate the gate-level netlist
- sim/scripts/run405.config - this file contains the parameters of the simulation "run" about to take place and needs editing to support the gate-level netlist simulation
This is the key script which needs a couple of modifications to simulate the netlist and not the RTL. It is a list of parameters organised into blocks which are read by the Perl script scripts/runTB. scripts/runTB then builds and executes the correct command line to run a particular simulation in your chosen simulator.
Open the script scripts/run405.config in your favourite text editor and look for the second block:
searchpath ./../src/rtl ./../src/mem_models $SYNOPSYS/packages/gtech/src_ver $SYNOPSYS/dw/sim_ver ./testbench ./vera/ver_shell end
As you can see a 'block' has a header identifying it and is closed by an end keyword. The modification to this block is to comment out the ./../src/rtl by adding a # in front of the line like so:
searchpath #./../src/rtl ./../src/mem_models $SYNOPSYS/packages/gtech/src_ver $SYNOPSYS/dw/sim_ver ./testbench ./vera/ver_shell end
By doing this we exclude the unsynthesised RTL from being discovered by the simulator which is what we want. The netlist should contain the complete circuit.
Take a look at the third block:
differentfile ./../src/rtl/p405s_params.v end
In this block we need to explicitly tell the simulator to compile the simulation models for the Artisan PDK cells from the technology library, the synthesised netlist itself and a wrapper called PPC405F5V1_soft.v:
differentfile ./../src/rtl/p405s_params.v ./../src/rtl/PPC405F5V1_soft.v ./../dc/netlist/PPC405F5V1_dft.v ./../tech_lib/artisan_13lvfsg/verilog/tsmc13_hs_modified_new.v end
and finally we need to add the GATE_SIM variable already mentioned above. This makes the testbench behave slightly differently. When simulating the RTL the testbench forces the state of certain internal registers to 0 at the start of every run. With a gate-level netlist those registers may no longer exist, and certainly may not exist with the same name or hierarchy. To achieve the same effect when the GATE_SIM variable is defined at the start of each run the testbench places the chip into scan mode and clocks 0's through the scan chains forcing all flops to have a starting value of 0.
The correct place to set GATE_SIM depends on your simulator so have a look at the blocks in the bottom of this file:
# This is a string appended to the MTI invocations mtioptions +define+UNITSIM +nospecify +define+GATE_SIM end # This is a string appended to the NC invocations ncoptions +define+UNITSIM +define+SYN_RTL +nospecify end
These two example blocks (there are others) refer to Mentor Graphic's ModelSim (mtioptions) and Cadence's NC Verilog (ncoptions). To add the define change the line to read as follows:
# This is a string appended to the NC invocations ncoptions +define+UNITSIM +define+SYN_RTL +nospecify +define+GATE_SIM end
You should now be ready to fire up coreConsultant and begin.
[Note: You can run the tests outside of coreConsultant but it won't generate the nice, navigable HTML reports. To do this use the command runtest from the sim directory.]
Changes in coreConsultant
1) Run core consultant by running the command coreConsultant in a terminal window.
2) Open the workspace you created to run the RTL functional verification from the previous article and you should see the window below:
3) Ensure the settings are correct in the 'Simulator' selection before moving on to 'Select Test Options'
4) In 'Select Test Options' choose Run_Gate_Sims. Move onto 'Select Testsuite'.
5) In 'Select Testsuite' set the path to the Netlist and the simulation library:
6) You are all done. Click 'Apply' to start the simulations
The results of the running simulations are visible in the test.log file which can be monitored in realtime by executing the following command in a terminal window from the sim directory:
tail -f test.log
Studying this file you should see the following (for NC Verilog but each simulator will issue warnings of this kind):
During the compilation you will get a lot of complaints about unconnected nets. This is only sensible as the individual cells from the cell library have a fixed number of outputs, especially the flops, that cannot be removed. They come with the cell:
TLATNX8HS LOCKUP1 ( .D(dp_scReg_icuStatus1_regL2[5]), .GN(sc), .Q(scan_out2)
|
ncelab: *W,CUVWSP (../dc/netlist/PPC405F5V1_dft.v,123147|18): 1 output port was not connected:
ncelab: (../tech_lib/artisan_13lvfsg/verilog/tsmc13_hs_modified_new.v,28144): QN
After the compilation things should settle down into a format similar to this, one per test:
ncsim: 08.10-s006: (c) Copyright 1995-2008 Cadence Design Systems, Inc.
Loading snapshot worklib.p405s_test_top:v .................... Done
=== Verilog with Synopsys Vera ===
ncsim> source /home/esdcad/software/cadence/linux/ius81/tools/inca/files/ncsimrc
ncsim> run
++---------------------------------------------------------------------++
|| VERA System Verifier (TM) ||
|| Version: A-2007.12 () -- Wed Dec 9 17:15:27 2009 ||
|| Copyright (c) 1995-2004 by Synopsys, Inc. ||
|| All Rights Reserved ||
|| ||
|| For support, send email to vera-support@synopsys.com ||
|| ||
|| This software and the associated documentation are confidential ||
|| and proprietary to Synopsys Inc. Your use or disclosure of this ||
|| software is subject to the terms and conditions of a written ||
|| license agreement between you, or your company, and Synopsys, Inc. ||
++---------------------------------------------------------------------++
Vera: Loading main "p405s_top_vera" (path = "p405s_test_top.top_vera")
Vera: Loading ../../vera/lib/p405s_top.vro..
Vera: Loading ../../vera/lib/p405s_memory.vro..
Vera: Loading ../../vera/lib/p405s_slave.vro..
Vera: Loading main "p405s_dcrmon" (path = "p405s_test_top.dcrmon_model")
Vera: Loading ../../vera/lib/p405s_dcrmon.vro..
Vera: Loading main "p405s_dcr" (path = "p405s_test_top.dcr_model")
Vera: Loading ../../vera/lib/p405s_dcr.vro..
Vera: Loading main "p405s_isocm" (path = "p405s_test_top.isocm_model")
Vera: Loading ../../vera/lib/p405s_isocm.vro..
Vera: Loading main "p405s_dsocm" (path = "p405s_test_top.dsocm_model")
Vera: Loading ../../vera/lib/p405s_dsocm.vro..
Vera: Loading main "p405s_intr_ctrl" (path = "p405s_test_top.intr_controller")
Vera: Loading ../../vera/lib/p405s_intr_ctrl.vro..
Vera: Loading main "p405s_jtag" (path = "p405s_test_top.jtag_controller")
Vera: Loading ../../vera/lib/p405s_jtag.vro..
Vera: Loading main "p405s_monitor" (path = "p405s_test_top.monitor_slave_side")
Vera: Loading ../../vera/lib/p405s_monitor.vro..
>> Setting TEST_c405ScanEnable = 1 <<
Entering the PLB Initialization sequence time=0
Entering Reset delay sequence time=1000
Completing Reset delay sequence time=2999000
>> Setting TEST_c405ScanEnable = 0 <<
>> Forcing Reset of D-CACHE Tags <<
3002000 info: Slave0: is in Reset
3003000 info: Slave0: is in Reset
3004000 info: Slave0: is in Reset
3005000 info: Slave0: is in Reset
3006000 info: Slave0: is in Reset
3007000 info: Slave0: is in Reset
3008000 info: Slave0: is in Reset
3009000 info: Slave0: is in Reset
3010000 info: Slave0: is in Reset
3011000 info: Slave0: is in Reset
3012000 info: Slave0: is in Reset
3013000 info: Slave0: is in Reset
>> Forcing Reset of D-CACHE Tags <<
DCRMON (3797000): DCR Write : Addr = 44 WData = bfff0000
DCRMON (3907000): DCR Write : Addr = 0 WData = 0
DCRMON (3922000): DCR Write : Addr = 11 WData = 0
DCRMON (3977000): DCR Write : Addr = 8 WData = 0
DCRMON (3997000): DCR Write : Addr = 1 WData = 0
DCRMON (4001000): DCR Write : Addr = 9 WData = 0
DCRMON (4005000): DCR Write : Addr = a WData = 0
DCRMON (4014000): DCR Write : Addr = 20 WData = 0
DCRMON (4028000): DCR Write : Addr = 3 WData = 0
DCRMON (4109000): DCR Write : Addr = b WData = 0
DCRMON (4113000): DCR Write : Addr = c WData = 0
6488000 info: Slave0: MasterId=1 Request for Write addr=00000010
6488000 info: Slave0: 1 to MultiByte Write
TESTCASE took 3474 Clocks
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
TESTCASE "addfvt" PASSED
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Vera: finish encountered at time 6493000 cycle 6494
total mismatch: 0
vca_error: 0
fail(expected): 0
drive: 10739
expect: 0
sample: 49891
sync: 16493
Vera: finish encountered at time 6494000 cycle 6495
total mismatch: 0
vca_error: 0
fail(expected): 0
drive: 6493
expect: 0
sample: 3199836
sync: 607518
Vera: finish encountered at time 6494000 cycle 6495
total mismatch: 0
vca_error: 0
fail(expected): 0
drive: 19494
expect: 0
sample: 64898
sync: 32462
Vera: finish encountered at time 6494000 cycle 6495
total mismatch: 0
vca_error: 0
fail(expected): 0
drive: 6517
expect: 0
sample: 32469
sync: 19482
Vera: finish encountered at time 6494000 cycle 6495
total mismatch: 0
vca_error: 0
fail(expected): 0
drive: 3882
expect: 0
sample: 56947
sync: 12987
Vera: finish encountered at time 6494000 cycle 6495
total mismatch: 0
vca_error: 0
fail(expected): 0
drive: 11903
expect: 0
sample: 43549
sync: 12987
Vera: finish encountered at time 6494000 cycle 6495
total mismatch: 0
vca_error: 0
fail(expected): 0
drive: 6737
expect: 0
sample: 33265
sync: 13564
Vera: finish encountered at time 6494000 cycle 6495
total mismatch: 0
vca_error: 0
fail(expected): 0
drive: 1
expect: 0
sample: 140
sync: 108
TESTCASE "addfvt" PASSED
You can see the Vera banner at the top, the individual Vera modules loading. The only difference to the RTL simulations are the following two lines: >> Setting TEST_c405ScanEnable = 1 <<and
>> Setting TEST_c405ScanEnable = 0 <<
which are found after the last Vera module loads at the start of the simulation. This is the effect of the GATE_SIM define added earlier and is showing the activation of the scan chains to zero the flops internally.
And finally you should be greeted with a report in coreConsultant that looks like this:
There, you have now formally and functionally verified your very own PowerPC™ 405-S netlist. All it needs is to be placed and routed (and finally functionally and formally verified again) and you are good to go!
Published with permission from IBM and Synopsys
