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

Groups > comp.arch.embedded > #20066

Re: processor core validation

Show all headers | View raw

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

Back to comp.arch.embedded | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

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

csiph-web