Retrascope » Retrascope Test Suite

h1. Found Errors

Here the collection of public benchmarks (that are used in the project) and bug fixes are presented.

{{toc}}

h2. Texas97 benchmark

"Texas97 benchmark Web page":https://ptolemy.berkeley.edu/projects/embedded/research/vis/texas-97

The complete collection of our fixes is available in the "patch":https://forge.ispras.ru/attachments/5900/0001-test-apply-fixes-to-Texas97-modules.patch below.

1. 

src/main/verilog/texas97-benchmarks/Blackjack/dp.v: RDelaer1 -> RDealer1

src/main/verilog/texas97-benchmarks/Blackjack/dp.v: RDelaer2 -> RDealer2

2.

<pre><code class="diff">

--- a/src/main/verilog/texas97-benchmarks/DLX/PDLX/control.v

+++ b/src/main/verilog/texas97-benchmarks/DLX/PDLX/control.v

@@ -14,7 +14,7 @@ module Control(

         SESel,

         Reset,

-        Clk ,

+        Clk// ,

               );

    reg monitor_lw;

    reg monitor_j;

</code></pre>

h3. $ND macro

This macro implements a Non-Deterministic choice from the sequence of values. Since this macro is not a standard one, it should be substituted by the *$random* system calls.

In our version of Texas97 benchmark *$ND* calls are substituted by concatenation operations, like here:

<pre><code class="diff">

--- a/src/test/verilog/texas97-tests/Blackjack/dp.v

+++ b/src/test/verilog/texas97-tests/Blackjack/dp.v

@@ -93,24 +93,25 @@

                Deck[13] =0;

                Deck[14] =0;

                Deck[15] =0;

-               First6Card[0]=$ND(0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15);

-               First6Card[1]=$ND(0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15);

-               First6Card[2]=$ND(0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15);

-               First6Card[3]=$ND(0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15);

-               First6Card[4]=$ND(0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15);

-               First6Card[5]=$ND(0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15);

+               First6Card[0]={0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15};

+               First6Card[1]={0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15};

+               First6Card[2]={0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15};

+               First6Card[3]={0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15};

+               First6Card[4]={0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15};

</code></pre>

h3. Enums

There are no enums in Verilog 2005, so 'typedef enum {...}' constructions were substituted by defines:

<pre><code class="diff">

--- a/src/test/verilog/texas97-tests/PI_BUS/multi_master/bus.v

+++ b/src/test/verilog/texas97-tests/PI_BUS/multi_master/bus.v

@@ -1,6 +1,11 @@

-typedef enum{BUS_IDLE,BUS_REQ,BUS_ADDR,BUS_ADDRDATA,BUS_DATA} busst;

+//typedef enum{BUS_IDLE,BUS_REQ,BUS_ADDR,BUS_ADDRDATA,BUS_DATA} busst;

+`define BUS_IDLE 3'b000

+`define BUS_REQ 3'b001

+`define BUS_ADDR 3'b010

+`define BUS_ADDRDATA 3'b011

+`define BUS_DATA 3'b100

</code></pre>

h2. VCEGAR benchmark

"VCEGAR benchmark Web page":http://www.cprover.org/ebmc/

h3. Syntax errors

<pre><code class="diff">

--- a/src/test/verilog/vcegar-tests/small/seq/example.v

+++ b/src/test/verilog/vcegar-tests/small/seq/example.v

@@ -1,13 +1,13 @@

-always @ (posedge clock) begin

-       if (a<100) 

+always @ (posedge clk) begin

+       if (a<100)

           a<=b+a;

</code></pre>