( ESNUG 550 Item 2 ) -------------------------------------------- [05/05/15]
Subject: User on Logic Refinery RuleSmith vs. JasperGold/0-in/BugScope/UVM
> Then we made the switch from the Cadence IEV formal verification tool to
> the Jasper JasperGold (this was before the acquisition) as we saw some
> advantage in debug analysis with JasperGold instead of IEV.
>
> What I liked about the waveform debugger, Jasper Visualize, is that you
> can manipulate the waveform to expore your design. It can generate
> on-the-fly covers, change signal values on any clock, and then generate
> a new trace. Once that trace is displayed, you still have traditional
> waveform debug features -- like tracing the source of a value change.
>
> - Normando Montecillo of Broadcom
> http://www.deepchip.com/items/0544-02.html
From: [ My Name Is Ozymandias ]
Hi, John,
Our verification group did an internal first look at a new semi-formal tool
"RuleSmith" from Logic Refinery. From what we've found, it has 7 use modes
but it essentially is a Same Model Tool. That is, RuleSmith produces
stimulus, checking and coverage from the same model.
We evaled how RuleSmith worked with our existing simulators, formal tools,
and test benches. We evaluated its stimulus and checking aspects, but less
so its coverage aspects.
WHAT RULESMITH IS AND IS NOT
In a nutshell, RuleSmith is a one model standalone simulation rules engine.
It plugs into VCS/NC-sim/Questa, and it interacts with them through the
Verilog-PLI. It also talks to testbenches (at the transactional level)
through the DPI.
RuleSmith is like JasperGold in that it's driven by a precise model of the
specification, but ESM is more compact. You don't have to write a Verilog
checker with RuleSmith like how you do with JasperGold.
You don't use UVM with RuleSmith. Also RuleSmith is nothing like 0-in,
which is an extended model checker. RuleSmith is not like Atrenta BugScope,
an assertion synthesis tool.
Also it's not an "intelligent testbench" like Mentor InFact or Breker Trek
or Cadence Perspec.
RULESMITH IS USED 7 WAYS
These are 7 main ways to use RuleSmith:
1. Write one model and having RuleSmith generate stimulus, checkers,
and measure coverage.
2. Take one specification property and model it with RuleSmith to use
it as a checker. If you later discover you need stimulus to
exercise the space around the check, RuleSmith can automatically
generate the stimulus using your same model.
3. You can write your stimulus first, and then you can later attach
RuleSmith as a checker. Because you get stimulus and checking
from the same model, the RuleSmith engine turns into an
observation checking point. It converts stimulus to check only
when you change your hierarchy. For example:
- When you do stimulus generation at a lower level, and want
to capture knowledge so your top level stimulus (like your
software) isn't doing something illegal at the lower level.
They call this "sim promotion".
- If certain low level stimulus was developed using intelligent
modeling, you may want to ensure that the top level stimulus
is also doing the same. An example of low level stimulus
modeling might be a cache address model that uses certain
cache address collisions more often.
4. You can use RuleSmith as your stimulus source to your testbenches
in VCS/NC-Sim/Questa
5. RuleSmith is also good at checking stimulus from other external
sources -- like a hand-coded UVM testbench or traces from real SW.
You just replay your existing stimulus from these other sources
with RuleSmith, and the tool will show errors if it detects bad
observations.
6. You can use RuleSmith measure and collect coverage from your
VCS/NC-sim/Questa simulation.
In addition RuleSmith could be used as an Instruction Set Simulator like
ARMulator (or ARM Fast Models) -- but the LRF people do NOT recommend that
you use RuleSmith as an ISS because it's a lot slower in that mode.
WE DID NOT NEED TO LEARN A NEW LANGUAGE
With RuleSmith, you write rules of what should happen. It uses a compact
proprietary expression language (called ESM) similar to System Verilog
constraints, but it's more powerful. Essentially any declarative or
"English-style" rule can be written in this ESM language. Most of our
instruction set rules were easily converted from English into ESM through
a script LRF provided -- letting us use the .XML structure we like. The
script's internal name is Processor_Modeling.pl. It did 95% of the
converting -- we did have to manually add some custom ESM rules for
certain sequential constraints.
Here's some sample custom ESM that we hand wrote:
// LS_Collision is a pattern of two instructions.
// Any number of other instructions may fall between i1 and i2.
point LS_Collision; {
EXEC i1; // symbol that points to some instr
EXEC i2; // symbol that points to another instr
TAG_CATEGORY_ST(i1); // i1 must be a store instr
TAG_CATEGORY_LD(i2); // i2 must be a load instr
~OVERLAP_SCOPE(i1,i2); // different threads
OVERLAP_MEMORY(i1,i2); // to overlapping addresses
NEEDS_SYNC(i1,i2); // no synchronizing instrs between them
} endpoint
// Call_Return is a pattern of two instructions.
// Any number of other instructions may fall between i1 and i2.
point Call_Return; {
EXEC_BLR iC; // a branch-and-link instruction
EXEC_RET iR; // return (branch-to-link-reg) instr
BEFORE(iC,iR); // call instr executed before return instr
OVERLAP_SCOPE(iC,iR); // both instrs execute on the same thread
PRESERVE_LR(iC,iR); // no instruction can overwrite
// link register between iC and iR
} endpoint
Although I'd like to show you the whole output ESM, I can't. Like Breker
Trek and Mentor InFact, LRF also doesn't let anyone publish the exact code
used to drive their tools.
Basically, Processor_Modeling.pl can take in:
- Instruction sets
- Meta sets, i.e. rules controlling sequences and
interactions across threads.
- Coherent networks/fabrics
and converts it all to their proprietary ESM which RuleSmith runs on.
RULESMITH VS. GRAPH-BASED INTELLIGENT TESTBENCHES
Unfortunately, with graph-based intelligent testbench generators, such as
Mentor InFact and Breker Trek, you only have a graph instead of standalone
rules. The problem is that some real-life complex sequences simply cannot
be represented with a graph -- so it's easy to accidentally over constrain
the problem space.
Also, when I last looked at Mentor InFact some time ago, they had punted on
checking -- it didn't build a checker. InFact can help solve our stimulus
problem somewhat, but not our checking problem.
RULESMITH VS. STIMULUS FORMAL TOOLS
Formal tools such as JasperGold and Incisive Formal can't scale beyond the
block level. They make you sacrifice completeness for scale. JasperGold
can only handle blocks of about 100,000 to 200,000 gates without sacrificing
the completeness of the proof as long as JasperGold doesn't run into a
multiplier inside that block. Hit one multiplier and the JasperGold proof
loops infinitely.
Also JasperGold and Incisive Formal are not interpretable as a simulation
source for Verilog. You can't use a JasperGold model as stimulus for your
Verilog/VHDL simulation. For checking and coverage, yes. But NOT for
stimulus.
RuleSmith's rule creation, being 100% declarative, is done in a similar way
to these formal tools, but it can scale much larger - the full SoC which can
be 100 million gates. RuleSmith basically adds a level of formalization to
your checker and stimulus sources. But you do have to provide some steering
or wait 10,000 years for a pure random random approach to seek out those
interesting corner cases.
RULESMITH VS. SYSTEM VERILOG TESTBENCHES
Stated simply if you use SystemVerilog testbenches, combining stimulus and
checking is flawed.
Theoretically, you could do both stimulus and constraint checking using a
SystemVerilog testbench, but it is not one model. Instead, you must write
a separate stimulus and constraint checker.
On our project we do hierarchical design. We could be running real software
at our top/system level -- and also running aggressive testbenches at the
lower level (e.g. pin level or simple protocol constraints). Not only is
writing separate models for stimulus and constraint checking twice the work,
but you risk introducing errors due to being out of sync.
When creating a SystemVerilog testbench, you typically write declarative
constraints with a lot of procedural code. When you combine the two
different representations into one, you often introduce over- or under-
constrained conditions. Types of modeling errors:
1. You over-constrain your stimulus. When you write your stimulus for
the lower-level you can exclude a possible stimulus that could be
observed at the full-system level. Then when you run your checker
at a higher-level, you risk missing common bugs. (I have seen this
many times.) Examples:
- You miss a hang condition that doesn't catch which exact
instruction that caused the entire processor to hang.
- The engineer who wrote the low-level stimulus for the IP
thinks a corner case is illegal, but the SoC team uses it.
2. You under-constrain your stimulus, leading to false failures.
Example:
- Violating instruction ordering (e.g. Instruction "Alpha"
from a stimulus generator must come 3 instructions before
instruction "Beta").
Often some verification engineers think it's OK to under-constrain an
environment at lower-level. However, this can mean a boatload of false
Verilog/VHDL RTL fixes done that weren't really needed.
Also, under-constraining can lead to a lot of unnecessary debugging. You
are literally wasting engineering man-hours chasing phantom bugs.
Using RuleSmith in "coverage mode" can help check if your top-level stimulus
is hitting certain cases. This ensures that your top-level stimulus is
witnessing key coverage points. In addition, specific coverage holes can
be excluded from your low-level once your top-level knows that it is an
under-constraint at the lower-level.
WHERE RULESMITH RULES
The one big differentiating strength RuleSmith has is from one model it lets
verification engineers simultaneously combine stimulus along with constraint
checking.
Second, RuleSmith solves all constraints together. Unlike SystemVerilog,
which cannot solve constraint problems together if your code was not
originally partitioned correctly -- RuleSmith does this automatically.
For example, you can have the two sets of unit-level rules:
- Instruction generation: instruction Alpha must always finish
before instruction Bravo can start.
- Cache instruction: You must have a barrier instruction after
a non-cache write.
With SystemVerilog testbenches, the verification engineer must try to stitch
these two unit-level rules together manually -- which is time consuming and
error prone.
On the other hand, RuleSmith will automatically marry these unit-level rule
sets together to create the correct top-level stimulus that does both rules.
That is, with RuleSmith you can use one model for different hierarchical
verification purposes. With SystemVerilog testbenches, you can't.
- [ My Name Is Ozymandias ]
P.S. And although we didn't test it, we've heard that RuleSmith can also
with one model combine coverage with stimulus and constraints, too.
---- ---- ---- ---- ---- ---- ----
Related Articles:
How I unwittingly started BRCM's Formal Verification Users Group
Formal users share 8 upsides, 6 downsides, and 13 best practices
Mark Wallace of Cavium's Jasper User Group (JUG'13) Trip Report
Join
Index
Next->Item
|
|
