Bug/error in synthesized file

[midoze...@gmail.com]

Hello everyone,

I am new to this tool and I am not sure if I am missing something but it seems that there is a bug in the tool. I have written the following C code and I used Panda to generate a vhdl file for it.

The C code is as following:

int mix (int x, int sel, int y, int z)  
{
int z10;
if (sel == 0)
{z10=x+y;}
else if (sel == 1)
{z10=x+y+x+z;}
else if (sel == 2)
{z10=x-y;}
else if (sel == 3)
{z10=x*z;}        // try else if
else if (sel == 4)
{z10=x+2*y;}
else if (sel == 5)
{z10=x;}

return z10;

}

The property for the vhdl file is as following:

property mix is
dependencies: no_reset;
for timepoints:
        t_end = t+0;



assume:                         
         at t: x = 10;
         at t: y = 2;
         at t: z = 9;

         at t: sel = 1;

prove:                                                                 



          at t_end:   return_port = x+y+x+z;


end property;

The problem is, whenever I write a property to verify the behavior of the generated vhdl file, I check the return port in the vhdl file. The return port always return the value of x*z which is the condition if sel == 3, even if I changed the value of sel in my property and I made it 0 or 1 for example, I should get either x+y or x+y+x+z in the return port. But this does not happen, I always get the value of x*z. On the other hand, whenever I change x*z to x+z in my C code, the whole program works completely fine, so it seems that the problem is in the multiplication operation. I would appreciate it if someone could give me some feedback regarding this.

[Fabrizio Ferrandi]

Hello,

I checked your code against my local version of bambu and I do not find any issue.

This is the command I used:

bambu ../module.c --generate-tb=x=10,y=2,z=9,sel=1 --simulate --simulator=XSIM -v4 -wH

I used XSIM from Xilinx since I need a simulator supporting mixed Verilog/VHDL simulation. MODELSIM should work as well.

Besides that, I notices that variable z10 is not initialized and in case the input sel is less than zero or greater than 5 the results is undefined.

Anyway, could you provide some further detail on which is the version you are using and which options you are passing to Bambu? In particular, I would like to understand which compiler, clang or gcc,  you are using.

Cheers,

Fabrizio

[Mohamed Basem]

Hello,

Thanks for your prompt reply. Maybe I have not clarified myself properly. So let me elaborate more. I am using Onespin software, I am using it to verify the VHDL file produced by Bambu PandA. So I am not using simulation in PandA to verify the behavior. Instead, due to my research experimentation, I take the generated VHDL file from Bambu and try to verify its behavior using properties that I write in Onespin [the property is written in the post I sent if you want to check it]. So I am facing this issue when I try to verify the behavior of the VHDL using the properties. 

Regarding the options I passed to bambu I simply ran the following command: "/opt/panda/bin/bambu --top-fname=loopy_n --writer H ../arithmetic.c"

Hope this clarified my question a bit more. So the main issue as I have stated before is that if I change the multiplication to addition or subtraction, all the cases work fine, but when I use multiplication, no matter which sel value I insert in my property, it always returns back the multiplication value.

Best Regards,

--
You received this message because you are subscribed to a topic in the Google Groups "PandA project discussions and questions" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/panda-project-discussions-questions/TXMiYnzLdI8/unsubscribe.
To unsubscribe from this group and all its topics, send an email to panda-project-discussio...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/panda-project-discussions-questions/8c870ec6-cfd2-45a1-97c5-9f7ff9d5ab0do%40googlegroups.com.

[Fabrizio Ferrandi]

Dear Mohamed,

I'm willing to help but I need some support from you. We do not have the Onespin software and so it is hard to understand what it is wrong with your experiment.

On my side, I need an input test vector showing the difference between the expected value and what the VHDL design produces. What Onesping say is for me useless without a counter example showing the unsatisfied property.

Moreover, to reproduce the error I need to know which bambu version you are using. Are you using the VM or are you using the bambu built from the github sources?

Another bit of information is related to the compiler you used. I saw that you used the default one, but the configure selects the default compiler among the ones available on your compilation environment. Redirecting the bambu log to a file and raising the verbosity with -v4 would help.

Finally, sharing the VHDL generated would help us in understanding the issue.

Kind regards,

Fabrizio

On Monday, July 27, 2020 at 1:28:16 PM UTC+2, Mohamed Basem wrote:

Hello,

Thanks for your prompt reply. Maybe I have not clarified myself properly. So let me elaborate more. I am using Onespin software, I am using it to verify the VHDL file produced by Bambu PandA. So I am not using simulation in PandA to verify the behavior. Instead, due to my research experimentation, I take the generated VHDL file from Bambu and try to verify its behavior using properties that I write in Onespin [the property is written in the post I sent if you want to check it]. So I am facing this issue when I try to verify the behavior of the VHDL using the properties. 

Regarding the options I passed to bambu I simply ran the following command: "/opt/panda/bin/bambu --top-fname=loopy_n --writer H ../arithmetic.c"

Hope this clarified my question a bit more. So the main issue as I have stated before is that if I change the multiplication to addition or subtraction, all the cases work fine, but when I use multiplication, no matter which sel value I insert in my property, it always returns back the multiplication value.

Best Regards,

To unsubscribe from this group and all its topics, send an email to panda-project-discussions-questions+unsubscribe@googlegroups.com.