( ESNUG 478 Item 9 ) -------------------------------------------- [12/18/08]
Subject: ( ESNUG 477 #3 ) Using Calypto SLEC in a CatapultC design flow
> After C code is actually synthesized to Verilog RTL code. Here we can
> automatically verify the RTL against the original algorithm source.
From: Duncan Mackay <dmackay=user domain=calypto not calm>
Hi, John,
In addition to CatapultC's built-in SystemC simulation flow (which is
called "SCVerify" that runs in QuestSim or NC-Sim), for the formal part
you can use Calypto's Sequential-Logic Equivalency Checking SLEC tool.
Both are automated "push-button" processes inside CatC.
Here are step-by-step on the Catapult-Calypto verification process:
1. At any time during your Catapult C design cycle, you can enable the SLEC
integrated flow by double-clicking on the SLEC icon in the Flow Manager
pane of the Catapult GUI or typing "flow package require /SLEC" at the
command line. This will bring up a window asking if you want to enable
the flow. Click Yes.
2. Once you have enabled the flow, Catapult will bring up an options dialog
to help configure how Catapult will generate the files necessary for
formal verification with SLEC. More on these options later - just click
OK for now.
3. When CatC generates the final RTL netlist, it will also automatically
generate three files necessary for SLEC:
- a SystemC wrapper around the original C++ code that was used
as the input to Catapult Synthesis,
- a VHDL or Verilog wrapper for the Catapult generated RTL netlist,
- and a TCL command script for SLEC.
You will see these files show up in the Catapult GUI under the folder
named Project Files -> Solution -> Verification -> SLEC.
4. Next, invoke SLEC on the design by double-clicking on the appropriate
"SLEC verification of ... RTL output" TCL script icon (there is one for
each netlist format, VHDL and Verilog) or by typing (for VHDL):
"flow run /SLEC/launch_cmds SLEC_compile_rtl_vhdl.tcl . -batch"
or (for Verilog)
"flow run /SLEC/launch_cmds SLEC_compile_rtl_v.tcl . -batch"
You will see SLEC running in the Catapult transcript window.
5. When SLEC finishes, it'll report the number of proofs and falsifications
in the transcript window. All of the reports and logfiles created by
SLEC are also placed in the Catapult GUI under the TCL script icon that
you double-clicked in step 4.
6. Double-click on the "SLEC VHDL Verification Logfile" (or "SLEC Verilog
Verification Logfile" if you use Verilog) in the Catapult GUI to view
the results.
If a falsification is reported by SLEC, the tool generates VCD waveforms and
makefiles/testbenches to run on ModelSim/NC-Sim/VCS to demonstrate the
falsification. From the Catapult GUI you can double-click on the waveforms
to launch the waveform viewer in ModelSim.
SLEC also produces consistency check reports on both the C++ and the RTL
which the user can use to make your code cleaner. In particular, SLEC helps
to identify cases where the semantics of the input design were ambiguous for
synthesis (such as an uninitialized variable, shifting by a negative number
or out of bounds array access) resulting in C and RTL that do not match. If
you are new to designing hardware with C++ you might fall into some of these
cases. SLEC helps find such ambiguities for a more fully specified design.
- Duncan Mackay
Calypto Santa Clara, CA
Index
Next->Item
|
|
