Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.arch.embedded > #20015 > unrolled thread

processor core validation

Back to article view | Back to comp.arch.embedded

Contents

  processor core validation al.basili@gmail.com (alb) - 2015-02-08 22:02 +0000
    Re: processor core validation Tim Wescott <tim@seemywebsite.com> - 2015-02-08 18:13 -0600
      Re: processor core validation al.basili@gmail.com (alb) - 2015-02-09 17:03 +0000
        Re: processor core validation Tim Wescott <seemywebsite@myfooter.really> - 2015-02-09 13:37 -0600
          Re: processor core validation al.basili@gmail.com (alb) - 2015-02-11 22:12 +0000
            Re: processor core validation rickman <gnuarm@gmail.com> - 2015-02-11 20:18 -0500
              Re: processor core validation al.basili@gmail.com (alb) - 2015-02-12 08:08 +0000
    Re: processor core validation HT-Lab <hans64@htminuslab.com> - 2015-02-09 09:04 +0000
      Re: processor core validation Paul E Bennett <Paul_E.Bennett@topmail.co.uk> - 2015-02-09 09:41 +0000
        Re: processor core validation HT-Lab <hans64@htminuslab.com> - 2015-02-09 11:35 +0000
        Re: processor core validation Tom Gardner <spamjunk@blueyonder.co.uk> - 2015-02-09 12:19 +0000
      Re: processor core validation al.basili@gmail.com (alb) - 2015-02-09 17:16 +0000

#20015 — processor core validation

Hi everyone,

I was wondering if anyone can point me to some formal method to validate 
a soft processor core. 

We have the source code (vhdl) and a simulation environment to load 
programs and execute them, but I'm not sure in this case code coeverage 
will be sufficient. What about cases like interrupt handling?

I can run Dhrystone or CoreMark, but will it be sufficient?

Any idea/pointer/comment is appreciated,

Al

-- 
A: Because it messes up the order in which people normally read text.
Q: Why is top-posting such a bad thing?
A: Top-posting.
Q: What is the most annoying thing on usenet and in e-mail?

[toc] | [next] | [standalone]

#20016

On Sun, 08 Feb 2015 22:02:31 +0000, alb wrote:

> Hi everyone,
> 
> I was wondering if anyone can point me to some formal method to validate
> a soft processor core.
> 
> We have the source code (vhdl) and a simulation environment to load
> programs and execute them, but I'm not sure in this case code coeverage
> will be sufficient. What about cases like interrupt handling?
> 
> I can run Dhrystone or CoreMark, but will it be sufficient?
> 
> Any idea/pointer/comment is appreciated,

Ooh!  What a good application for test driven design!  You're too late, 
though.

Testing software for quality assurance is like closing your eyes and 
waving a butterfly net around -- if you find a bug, you know there was 
one, but if you don't find a bug, you can't be sure there aren't a lot 
out there still.

I'd advocate for an app that's custom-designed for the core that makes 
sure that every bit of the thing gets exercised.  This is going to mean a 
lot of assembly code, and some of it oddball.

-- 
www.wescottdesign.com

[toc] | [prev] | [next] | [standalone]

#20024

Hi Tim,

Tim Wescott <tim@seemywebsite.com> wrote:
[]
>> We have the source code (vhdl) and a simulation environment to load
>> programs and execute them, but I'm not sure in this case code coeverage
>> will be sufficient. What about cases like interrupt handling?
[]
> Ooh!  What a good application for test driven design!  You're too late, 
> though.

Sure, taking a piece of stuff and wanting to validate it without 
thinking it verifiable from day one is certainly a big effort, but maybe 
less important than having to redesign it from scratch.

Instrumenting the code with appropriate 'test points' is certainly 
awkward but still doable.

> Testing software for quality assurance is like closing your eyes and 
> waving a butterfly net around -- if you find a bug, you know there was 
> one, but if you don't find a bug, you can't be sure there aren't a lot 
> out there still.

That's the very basic principle of verification, you cannot guarantee 
anything else except what you verified it working. Testing has it's own 
limits and that is why software development in hirel apps is not as 
straight forward as for commercial/industrial applications.

> I'd advocate for an app that's custom-designed for the core that makes 
> sure that every bit of the thing gets exercised.  This is going to mean a 
> lot of assembly code, and some of it oddball.

I believe this is only the trivial stuff, verifying instruction 
correctness should be not that complex. More critical would be interrupt 
handling according to code execution. Is the interrupt always served? 
Are there any specific instances where the interrupt can be masked by a 
certain combination of instructions in the pipeline?

Still I have more questions than answers at this point! :-/

Al

[toc] | [prev] | [next] | [standalone]

#20032

On Mon, 09 Feb 2015 17:03:23 +0000, alb wrote:

> Hi Tim,
> 
> Tim Wescott <tim@seemywebsite.com> wrote:
> []
>>> We have the source code (vhdl) and a simulation environment to load
>>> programs and execute them, but I'm not sure in this case code
>>> coeverage will be sufficient. What about cases like interrupt
>>> handling?
> []
>> Ooh!  What a good application for test driven design!  You're too late,
>> though.
> 
> Sure, taking a piece of stuff and wanting to validate it without
> thinking it verifiable from day one is certainly a big effort, but maybe
> less important than having to redesign it from scratch.
> 
> Instrumenting the code with appropriate 'test points' is certainly
> awkward but still doable.
> 
>> Testing software for quality assurance is like closing your eyes and
>> waving a butterfly net around -- if you find a bug, you know there was
>> one, but if you don't find a bug, you can't be sure there aren't a lot
>> out there still.
> 
> That's the very basic principle of verification, you cannot guarantee
> anything else except what you verified it working. Testing has it's own
> limits and that is why software development in hirel apps is not as
> straight forward as for commercial/industrial applications.
> 
>> I'd advocate for an app that's custom-designed for the core that makes
>> sure that every bit of the thing gets exercised.  This is going to mean
>> a lot of assembly code, and some of it oddball.
> 
> I believe this is only the trivial stuff, verifying instruction
> correctness should be not that complex. More critical would be interrupt
> handling according to code execution. Is the interrupt always served?
> Are there any specific instances where the interrupt can be masked by a
> certain combination of instructions in the pipeline?
> 
> Still I have more questions than answers at this point! :-/

You could have a combination hardware/software test harness, where you 
have a full test app (or perhaps an app that loops through the processor 
states that are of most interest) while at the same time the processor is 
getting interrupted by an asynchronous source that either has a different 
period from the processor's, or which is intentionally random.

Just going through the thing step-by-step and, positing problem modes, and 
examining the code to ask "how am I going to test for this?" will force 
you to think in depth about everything -- one of the frequent ways that 
TDD helps me to find bugs is by forcing me to discover them in the test 
design, before I even get to the point of throwing software at the test.

-- 

Tim Wescott
Wescott Design Services
http://www.wescottdesign.com

[toc] | [prev] | [next] | [standalone]

#20059

Hi Tim,

Tim Wescott <seemywebsite@myfooter.really> wrote:
[]
> You could have a combination hardware/software test harness, where you 
> have a full test app (or perhaps an app that loops through the processor 
> states that are of most interest) while at the same time the processor is 
> getting interrupted by an asynchronous source that either has a different 
> period from the processor's, or which is intentionally random.

This test harness could effectively be running on a simulator, where I 
could use a golden model and crosscheck that throwing random interrupts 
does not cause any deviation from the golden model behavior.

The main difficulty I see would be the functional coverage model I need 
to put in place to tell me I'm done.

There might be corner cases where the only solution would be crafting a 
special purpose test program to generate stimuli (or sequences of 
stimuli) which might be very difficult to achieve otherwise (some sort 
of direct testing and random testing).

> Just going through the thing step-by-step and, positing problem modes, and 
> examining the code to ask "how am I going to test for this?" will force 
> you to think in depth about everything -- one of the frequent ways that 
> TDD helps me to find bugs is by forcing me to discover them in the test 
> design, before I even get to the point of throwing software at the test.

I can simply get the spec of the processor and start to classify the 
requirements and then go one by one trying to build my functional 
coverage model. It is possible that going through the code would not be 
needed, even though it might help us discovering corner cases.

Assuming the golden model is provided (I've found one on OVP, yet not 
sure whether it is the right one!) I'll just verify compliance to the 
golden model and maybe present some usecases where some high level 
software is able to run and work without crashing.

The black box approach has some advantages:

1. no need to know the details (unless we need a fix) 
2. bfm for processor's interface are /available/ (write_mem, read_mem) 
3. heuristic approach (let's see if it breaks!)

OTOH we might face the need to open the box and go deeper with our 
verification, where interactions between internal elements have to be 
analyzed.

With the hypothesis that the processor 'state' does not depend on 
previous instructions (there's no cache), the order of the instructions 
does not necessarily matter. Should this be the case I'll probably can 
simply live with throwing random instructions at it.

Al

[toc] | [prev] | [next] | [standalone]

#20061

On 2/11/2015 5:12 PM, alb wrote:
> Hi Tim,
>
> Tim Wescott <seemywebsite@myfooter.really> wrote:
> []
>> You could have a combination hardware/software test harness, where you
>> have a full test app (or perhaps an app that loops through the processor
>> states that are of most interest) while at the same time the processor is
>> getting interrupted by an asynchronous source that either has a different
>> period from the processor's, or which is intentionally random.
>
> This test harness could effectively be running on a simulator, where I
> could use a golden model and crosscheck that throwing random interrupts
> does not cause any deviation from the golden model behavior.
>
> The main difficulty I see would be the functional coverage model I need
> to put in place to tell me I'm done.
>
> There might be corner cases where the only solution would be crafting a
> special purpose test program to generate stimuli (or sequences of
> stimuli) which might be very difficult to achieve otherwise (some sort
> of direct testing and random testing).

I wouldn't put much faith in using random interrupts other than to help 
your thinking to see if they cause any problems you don't think of.  I 
would say it would much more important to analyze the circuitry and 
generate stimuli that test the corner cases.

The problem with random stimuli is just that, it is random... well 
pseudo random and so you don't really know how well it tested things. 
Testing can't prove something works other than the specific things that 
are being tested.


>> Just going through the thing step-by-step and, positing problem modes, and
>> examining the code to ask "how am I going to test for this?" will force
>> you to think in depth about everything -- one of the frequent ways that
>> TDD helps me to find bugs is by forcing me to discover them in the test
>> design, before I even get to the point of throwing software at the test.
>
> I can simply get the spec of the processor and start to classify the
> requirements and then go one by one trying to build my functional
> coverage model. It is possible that going through the code would not be
> needed, even though it might help us discovering corner cases.
>
> Assuming the golden model is provided (I've found one on OVP, yet not
> sure whether it is the right one!) I'll just verify compliance to the
> golden model and maybe present some usecases where some high level
> software is able to run and work without crashing.
>
> The black box approach has some advantages:
>
> 1. no need to know the details (unless we need a fix)
> 2. bfm for processor's interface are /available/ (write_mem, read_mem)
> 3. heuristic approach (let's see if it breaks!)
>
> OTOH we might face the need to open the box and go deeper with our
> verification, where interactions between internal elements have to be
> analyzed.
>
> With the hypothesis that the processor 'state' does not depend on
> previous instructions (there's no cache), the order of the instructions
> does not necessarily matter. Should this be the case I'll probably can
> simply live with throwing random instructions at it.

What about other aspects of the processor?  Surely it has registers and 
very likely the processor *does* have state, flags, status registers, 
control registers, pipelining...

-- 

Rick

[toc] | [prev] | [next] | [standalone]

#20066

Hi Rick,

rickman <gnuarm@gmail.com> wrote:
[]
>> This test harness could effectively be running on a simulator, where I
>> could use a golden model and crosscheck that throwing random interrupts
>> does not cause any deviation from the golden model behavior.
>>
>> The main difficulty I see would be the functional coverage model I need
>> to put in place to tell me I'm done.
>>
>> There might be corner cases where the only solution would be crafting a
>> special purpose test program to generate stimuli (or sequences of
>> stimuli) which might be very difficult to achieve otherwise (some sort
>> of direct testing and random testing).
> 
> I wouldn't put much faith in using random interrupts other than to help 
> your thinking to see if they cause any problems you don't think of.  I 
> would say it would much more important to analyze the circuitry and 
> generate stimuli that test the corner cases.

I agree with the analysis approach, but I would defer it to analyze 
corner cases instead of the whole design. The reason being that 
analyzing the code may take an effort that is much bigger than its added 
value. If I can get away with testing the 'majority' of the cases with 
contrained random stimuli I'd be much more efficient and focus only on 
coverage holes.

> The problem with random stimuli is just that, it is random... well 
> pseudo random and so you don't really know how well it tested things. 

When I'm talking about random generation is always 'constrained random'. 
I do not simply throw interrupts at random frequency, but try to do it 
when a certain set of instructions are used (like interrupting while 
branching or the like).

> Testing can't prove something works other than the specific things that 
> are being tested.

that is always correct, that's why every circuit is faulty unless proven 
otherwise.

[]
>> With the hypothesis that the processor 'state' does not depend on
>> previous instructions (there's no cache), the order of the instructions
>> does not necessarily matter. Should this be the case I'll probably can
>> simply live with throwing random instructions at it.
> 
> What about other aspects of the processor?  Surely it has registers and 
> very likely the processor *does* have state, flags, status registers, 
> control registers, pipelining...

At higher level the 'state' of the processor is essentially the snapshot 
of all its internal registers at any given time, i.e. general purpose 
registers, memory and pipeline. AFAIK there's no instruction that is 
automatically performed by the processor on a given 'event' (like 
interrupt), so checking for stack/heap integrity is certainly not 
related to the processor itself but to the assembler correctness.

Pushing and popping PC to the stack is the only thing this processor 
does automatically AFAIK and context saving is up to the user. That 
would be fairly easy to verify since it suffice to check that returning 
from the ISR is at the right address.

For what concerns interrupt masking, that's another item, I'm not quite 
sure what is this processor doing with interrupts, whether they are 
latched or masked, but this is only my lack of knowledge and I surely 
need to know what is the processor *specified to do* and verify that it 
does it correctly.

I've read something about the Viper, as Hans suggested, and it looks to 
me that formal verification (from formal specification) is nice but not 
a silver bullet (see here: 
http://www.google.ch/url?sa=t&rct=j&q=avraproofpaper&source=web&cd=1&cad=rja&uact=8&ved=0CCIQFjAA&url=http%3A%2F%2Fwww.cl.cam.ac.uk%2F~mjcg%2Fpapers%2FAvraProofPaper.pdf&ei=3V3cVJOXJcrrUr2rgAg&usg=AFQjCNGkAs9TjCYZbWvN4ubT2Mna8ylflQ&bvm=bv.85761416,d.d24) 

OTOH it seems to me the Viper processor had advanced features that made 
it challenging to verify, like multiway branching, instruction and data 
caches and four pipelines in parallel (a nice beast!).

That being said, I certainly do not underestimate the effort required to 
validate a processor and that is also the reason for the thread. 
Awareness is among engineer's most valuable tools!

Al

[toc] | [prev] | [next] | [standalone]

#20019

On 08/02/2015 22:02, alb wrote:
> Hi everyone,

Hi Al,


> I was wondering if anyone can point me to some formal method to validate
> a soft processor core.
>
> We have the source code (vhdl) and a simulation environment to load
> programs and execute them, but I'm not sure in this case code coeverage
> will be sufficient. What about cases like interrupt handling?

I assume you know that Code Coverage has nothing to do with formal 
Verification and/or tells you if your processor is bug free, it just 
measure of the quality of your testbench.

If you want to formally test your processor then AFAIK your only option 
is to start writing lots of assertion and spend a years salary on a 
formal tool (solidify/Questa formal/etc). You can also run assertions in 
your simulator (like Modelsim DE/Riviera Pro) but this will not be 
exhaustive.

If your processor is small you might get away of writing top level 
assertions but most likely (due to the cone of logic) you will have to 
formally prove sub-blocks and use good old testvectors for the 
interconnects.

>
> I can run Dhrystone or CoreMark, but will it be sufficient?

What do you think ;-)

If you have a golden reference model then I would suggest a regression 
suite with lots of constrained random generated instructions, interrupt 
test programs, OS load, etc and comparing the output to your reference 
model.

I would also suggest you look up the (old) Viper processor which was a 
hot topic when I was working in the space industry.

Good luck,

Regards,
Hans.
www.ht-lab.com

>
> Any idea/pointer/comment is appreciated,
>
> Al
>

[toc] | [prev] | [next] | [standalone]

#20020

HT-Lab wrote:

> I would also suggest you look up the (old) Viper processor which was a
> hot topic when I was working in the space industry.
> 
> Good luck,

What happened to Viper? Haven't heard anything about it since the early 
90's.

-- 
********************************************************************
Paul E. Bennett IEng MIET.....<email://Paul_E.Bennett@topmail.co.uk>
Forth based HIDECS Consultancy.............<http://www.hidecs.co.uk>
Mob: +44 (0)7811-639972
Tel: +44 TBA (due to  re-location)
Going Forth Safely ..... EBA. www.electric-boat-association.org.uk..
********************************************************************

[toc] | [prev] | [next] | [standalone]

#20021

On 09/02/2015 09:41, Paul E Bennett wrote:
> HT-Lab wrote:
>
>> I would also suggest you look up the (old) Viper processor which was a
>> hot topic when I was working in the space industry.
>>
>> Good luck,
>
> What happened to Viper? Haven't heard anything about it since the early
> 90's.
>
Hi Paul,

I have no idea, from what I remember Marconi made an SOS rad-hardened 
version but I don't believe it ever went commercially,

Regards,
Hans.
www.ht-lab.com

[toc] | [prev] | [next] | [standalone]

#20022

On 09/02/15 09:41, Paul E Bennett wrote:
> HT-Lab wrote:
>
>> I would also suggest you look up the (old) Viper processor which was a
>> hot topic when I was working in the space industry.
>>
>> Good luck,
>
> What happened to Viper? Haven't heard anything about it since the early
> 90's.
>


IIRC there was a lawsuit. I don't know the real story, but I
remember hearing something to do with the chain of proof
not quite being complete from top to bottom.

I have no idea what happened to Viper's associated language,
NewSpeak (in which it was supposed to be impossible to express
an incorrect thought!).

[toc] | [prev] | [next] | [standalone]

#20025

Hi Hans,

HT-Lab <hans64@htminuslab.com> wrote:
[]
>> I was wondering if anyone can point me to some formal method to validate
>> a soft processor core.
>>
> I assume you know that Code Coverage has nothing to do with formal 
> Verification and/or tells you if your processor is bug free, it just 
> measure of the quality of your testbench.

sure, functional verification is certainly something different from code 
coverage.

> If you want to formally test your processor then AFAIK your only option 
> is to start writing lots of assertion and spend a years salary on a 
> formal tool (solidify/Questa formal/etc). You can also run assertions in 
> your simulator (like Modelsim DE/Riviera Pro) but this will not be 
> exhaustive.

That's an interesting tool, I didn't know about that. Surely it will 
speed up functional coverage since it analyses the reachable/unreachable 
states from a defined stimulus.

I believe though that is out of budget for the intended purpose.

> If your processor is small you might get away of writing top level 
> assertions but most likely (due to the cone of logic) you will have to 
> formally prove sub-blocks and use good old testvectors for the 
> interconnects.

It looks like ABV might be one path but it looks to me extremely 
tedious, especially if it needs to go at block level.

> 
>>
>> I can run Dhrystone or CoreMark, but will it be sufficient?
> 
> What do you think ;-)

Yeah, that was a silly question!

> 
> If you have a golden reference model then I would suggest a regression 
> suite with lots of constrained random generated instructions, interrupt 
> test programs, OS load, etc and comparing the output to your reference 
> model.

We should be able to set up the environment with one of the models 
provided by OVP, then throw a lot of transactions to both of them and 
see how they behave.

I suspect though that the model itself might be not so bug-free in the 
end. Still it would be a good starting point.

> I would also suggest you look up the (old) Viper processor which was a 
> hot topic when I was working in the space industry.

Didn't know about that. Thanks for the pointer.

Al

[toc] | [prev] | [standalone]

Back to top | Article view | comp.arch.embedded

csiph-web