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


Groups > comp.arch.embedded > #20025

Re: processor core validation

From al.basili@gmail.com (alb)
Newsgroups comp.arch.embedded
Subject Re: processor core validation
Date 2015-02-09 17:16 +0000
Message-ID <cjs8b5FgeoqU1@mid.individual.net> (permalink)
References <cjq4nnFu1psU2@mid.individual.net> <BK_Bw.674540$CV7.600546@fx18.am4>

Show all headers | View raw


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

Back to comp.arch.embedded | Previous | Next — Previous 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