YosysHQ / sby

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
Other
389 stars 73 forks source link

Incorrect vector length seen in VCD #123

Closed Harshitha172000 closed 2 years ago

Harshitha172000 commented 3 years ago

I asserted some properties to check the following code.

for (i = 0; i < NUMWAYS; i = i + 1) begin         
       if (access[i]) begin         
           for (j = 0; j < NUMWAYS; j = j + 1) begin              
                 if (i != j) begin                  
                   expand[i][j] = 1'b0;              
                 end       
          end         
           for (j = 0; j < NUMWAYS; j = j + 1) begin          
                 if (i != j) begin                
                    expand[j][i] = 1'b1;               
                end           
         end        
 end      
end 

I ended up with the following error where the last row of the expand vector has only 3 bits instead of 4.

expand_error

Later, I asserted properties to check whether all vectors of the expand array are of the same length, then the test passed.

VCD showing up incorrect vector length for the above code snippet.

jix commented 2 years ago

I can't reproduce this nor see how this could happen with the current version of sby and yosys. There have been changes in the meantime, so it might have been fixed by one of those. If this issue still persists with a current sby and yosys version, please provide a complete runnable example, not just a snippet.