使用SystemVerilog解决数组问题

数独是一种非常流行的游戏，数独本质上也是一个约束问题，所以我们可以让SystemVerilog的约束求解器来帮助我们解决。 约束求解器的精妙之处就是，我们只描述约束限制，繁重的数值生成工作由工具来帮我们完成。 你只需“既要...又要...”，其他的让下人干吧～

我们将数独网格表示为9x9整数数组，在名为sudoku_solver_base的类中定义所有属性字段和约束。

class sudoku_solver_base;          
  rand int grid[9][9];          
            
  // ...          
endclass

我们的第一个约束是数组中的所有元素都必须是 1 到 9 之间的数字，这很容易：

constraint all_elements_1_to_9_c {          
  foreach (grid[i, j])          
    grid[i][j] inside { [1:9] };          
}

每行中的元素必须是唯一的，可以使用SystemVerilog中的unique语法结构来描述：

constraint unique_on_row_c {          
  foreach (grid[i])          
    unique { grid[i] };          
}

另外，每列上的所有元素也必须是唯一的。此时我们就需要构建一个辅助数组，将网格转置。

local rand int grid_transposed[9][9];                  
constraint create_transposed_c {          
  foreach (grid[i, j])          
    grid_transposed[i][j] == grid[j][i];          
}

然后再加上类似的unique约束：

constraint unique_on_column_c {          
  foreach (grid_transposed[i])          
    unique { grid_transposed[i] };          
}

要解决一个数独问题，仅有这3个约束远远是不够的，因为还需要9 个子网格（3x3）都满足相同的约束。 我们将9x9网格保存在四维数组中：

local  rand  int  sub_grids [ 3 ][ 3 ][ 3 ][ 3 ];
constraint  create_sub_grids_c  {           
  foreach  ( sub_grids [ i ,  j ,  k ,  l ])           
    sub_grids [ i ][ j ][ k ][ l ]  ==  grid [ i * 3  +  k ][ j * 3  +  l ];           
}

在我们已经拿到所有对应的3x3网格后，我们类似地可以使用unique语法结构进行约束。 注意，这里需要将3x3的网格转换成一个一维数组再约束。

local  rand  int  sub_grids_lin [ 3 ][ 3 ][ 9 ];                    
constraint  create_sub_grids_lin_c  {           
  foreach  ( sub_grids_lin [ i ,  j ,  k ])           
    sub_grids_lin [ i ][ j ][ k ]  ==  sub_grids [ i ][ j ][ k / 3 ][ k % 3 ];           
}

‍‍‍‍

审核编辑：汤梓红