使用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 ];           
}

????

審核編輯：湯梓紅

聲明：本文內容及配圖由入駐作者撰寫或者入駐合作網站授權轉載。文章觀點僅代表作者本人，不代表電子發燒友網立場。文章及其配圖僅供工程師學習之用，如有內容侵權或者其他違規問題，請聯系本站處理。舉報投訴