Boolector Verilog Verification System

[yoshihide sugiura]

Hi,

Boolector combined with Verilog environment has been build up in this
October that has mentioned about eight months ago.

Feature of this system is:
BTOR is used as interface format.
Verilog2001 is implemented as RTL language.
System Verilog Assertion(SVA) is implemented as assertion/root
description language.
Distributed parallel processing system is implemented as Boolector
running environment.

Operation procedure of this system is:
Set signal(s) sequence(s) in the meaning of interval temporal logic
through SVA to the given Verilog.
Run Boolector.
Make Verilog input vector top module that activate the signal sequence
true.

Example of Verilog to BTOR translation is:
1. Circuit A ... graphical application
Verilog source code size => 4k step with 'for loop'
BTOR size => 79k step, where
'and' => 26k step
'redor' => 23k step

2. Circuit B ... graphical application
Verilog source code size => 9.6k step without 'for loop'
BTOR size => 7.6k step, where
'and' => 2k step
'redor' => 1.6k step

A set of mask 'and' and reduction 'redor' operators is used for single
bit selection.
For bit range selection, on the other hand, a set of 'concat' and
'slice' operators is used.
Result of examples shows that bit selection operation occupies about
50% of BTOR steps.

The most impressive BTOR command for me was 'slice'.
After making a set of equations and solving it, it took a few weeks
for me, I could understand how 'slice' is useful and powerful for the
bit range specification.
A lot of thanks for your great job.

The system is under final debugging phase now, and the next step for
me is to make an unsat analyzer.
I would like to report again when progressed.

Thank you again.

Regards,
Sugiura

[Jinpeng Lv]

Great. I am also looking for such a tool.

Greatly appreciated.

Thanks
Jinpeng

On Fri, Jun 15, 2012 at 8:31 AM, <roberto.b...@gmail.com> wrote:
> Hello Sugiura,
>
> do you maybe have a verilog2btor translator available for sharing ?
>
> Thanks,
> Roberto

> --
> You received this message because you are subscribed to the Google Groups
> "Boolector" group.
> To view this discussion on the web visit
> https://groups.google.com/d/msg/boolector/-/3JHU1aPjwh8J.
>
> To post to this group, send email to bool...@googlegroups.com.
> To unsubscribe from this group, send email to
> boolector+...@googlegroups.com.
> For more options, visit this group at
> http://groups.google.com/group/boolector?hl=en.



--
Jinpeng Lv
Ph.D. Candidate
CAD Research Group
Department of Electrical&Computer Engineering
University of Utah

[Roberto Bruttomesso]

I was expecting something more "flexible"

Thanks anyway,
Roberto

On Mon, Jun 18, 2012 at 2:27 AM, <sugiura....@gmail.com> wrote:
> Hi,
>
> Let me explain the status of Verilog2BTOR translation.
>
> It becomes a commercial product in Japan from this summer with name of
> "AiPG".
> The meaning is "All cases verify on invariant Property Global."
> The details is listed in my linkedin.
> http://www.linkedin.com/pub/sugiura-yoshihide/43/8a3/4b
>
> I would like to ship it if you could accept following conditions:
> 1) Academic purpose.
> 2) AiPG is written with Ruby so that encoded (encrypted) source will be
> shipped.
>    Encoding itself is done by tool from rrubyencoder.com (Inovica, UK).
> 3) Locked with ip-address and with some time period.
> 4) 64bit Linux.
>
> First of all, I think English document is necessary.
> I will send it to here when it becomes available at first.
>
> Thank you for finding out my Verilog2BTOR translation capability.
> If you have any questions or comments, please send it to here or to my
> e-mail address,
> sugiura....@gmail.com
>
> Regards,
> Sugiura

> --
> You received this message because you are subscribed to the Google Groups
> "Boolector" group.
> To view this discussion on the web visit

> https://groups.google.com/d/msg/boolector/-/k41VoRmEBrsJ.

>
> To post to this group, send email to bool...@googlegroups.com.
> To unsubscribe from this group, send email to
> boolector+...@googlegroups.com.
> For more options, visit this group at
> http://groups.google.com/group/boolector?hl=en.



--

Roberto Bruttomesso, PhD - http://tinyurl.com/r0b3r70