制約付きランダム化 (Constraint Random Value Generation)
概要
SVで導入された制約付きのランダム化機能により、自動機能検証テストの生成をすることができるようになります。この手法により、従来のダイレクトテストベンチよりも効率的に、ハードウェアのコーナケースバグを検証することができます。
ランダム化の対象は、クラス上の変数になります。
-クラスにする意味がここにもあると思います。
この制約を記述するのはユーザの仕事で、その制約上でランダムを生成するのは、シミュレータの仕事です。シミュレータ内には、ユーザが与えた制約を満足する空間を探索するソルバを内包しています。 LRMは、ソルバの実装方法について規定していませんので、生成するランダム数の値や順序は、シミュレータの実装依存になります。
-制約付きランダム化ソルバは、制約論理プログラミングにおける充足問題の一形態と見ることもできます。（純粋な数学問題に帰着します。） しかしSVの場合、単に解の有無だけを求めるのではなく、解の重み分布も指定することができます。その場合の分布解は、制約問題をBDDに展開しBDD上で解くことになります。解としては、存在することは分かっても現実的な時間とメモリでは解けないこともあります。また、ランタイムでの計算が重い場合もあり、シミュレーションパフォーマンスのボトルネックになってしまう場合もあります。
ここでは、制約を書くことで、可能になること、また、制約を書く上での制約を例で見ていきたいと思います。
クラス内の変数宣言で、rand 属性をつけた変数がランダム化の対象になります。
program cr3;
class bus;
rand byte addr;
rand byte data;
constraint addr_max {
addr >100;
data==addr+1;
} //制約条件
endclass
bus c1;
initial begin
c1=new;
repeat(10) begin
c1.randomize();
$display("c1.addr=%d c1.data=%d" ,c1.addr,c1.data);
end
end
endprogram
***** Veritak SV32 Engine Version 449 Build Jun 26 2013***** c1.addr= 119 c1.data= 120 c1.addr= 118 c1.data= 119 c1.addr= 115 c1.data= 116 c1.addr= 114 c1.data= 115 c1.addr= 113 c1.data= 114 c1.addr= 118 c1.data= 119 c1.addr= 110 c1.data= 111 c1.addr= 102 c1.data= 103 c1.addr= 123 c1.data= 124 c1.addr= 101 c1.data= 102 ---------- シミュレーションを終了します。time=0ns
ランダマイズの制御
制約の書き方
複数の制約を書く場合の注意
次の例は、まずい書き方です。
program cr1;
class bus;
rand int addr;
constraint addr_max {
0 < addr < 100;//BAD (0< addr ) <100 になってしまう。
} //制約条件
endclass
bus c1;
initial begin
c1=new;
repeat(20) begin
c1.randomize();
$display("c1.addr=%d ,c1.addr);
end
end
endprogram
次のように意図したに動きません。
***** Veritak SV32 Engine Version 449 Build Jun 26 2013***** c1.addr= 1930320482 c1.addr= 1473764418 c1.addr= 1892017771 c1.addr= 851928013 c1.addr= -677990020 c1.addr= 1500733529 c1.addr= -861842297 c1.addr= 1134036892 c1.addr= -609173158 c1.addr= -550383961 c1.addr= -631432959 c1.addr= 1675406586 c1.addr= 587618114 c1.addr= -403223153 c1.addr= -378577201 c1.addr= 734465886 c1.addr= -541838364 c1.addr= 926132111 c1.addr= -246653150 c1.addr= -355976802 ---------- シミュレーションを終了します。time=0ns次のように分けて書きましょう。
program cr1b;
class bus;
rand int addr;
constraint addr_max {
0 <addr ;//分けて書く
addr < 100;
} //制約条件
endclass
bus c1;
initial begin
c1=new;
repeat(20) begin
c1.randomize();
$display("c1.addr=%d " ,c1.addr);
end
end
endprogram
一つの制約内で複数のステートメントを書くのは、ステートメント同士を論理積
&&で結ぶのと等値です。 上の例で、制約を
constraint addr_max {
0<addr && addr<100;
}
と書いても同じです。
***** Veritak SV32 Engine Version 449 Build Jun 26 2013***** c1.addr= 45 c1.addr= 53 c1.addr= 73 c1.addr= 46 c1.addr= 53 c1.addr= 52 c1.addr= 3 c1.addr= 42 c1.addr= 54 c1.addr= 93 c1.addr= 58 c1.addr= 59 c1.addr= 22 c1.addr= 28 c1.addr= 56 c1.addr= 34 c1.addr= 55 c1.addr= 27 c1.addr= 29 c1.addr= 43 ---------- シミュレーションを終了します。time=0ns
符号付の制約に注意
符号付の制約は、細心の注意が必要です。
class C;
rand byte x;
constraint C {
x<=100;
}
endclass
program pr2;
C obj;
int m[int];
initial
begin
obj=new();
repeat(10) begin
void'(obj.randomize());
$display("obj.a=%d ",obj.x);
end
$finish(2);
end
endprogram
マイナスの値も確かに制約を満足しますね。(byteは、符号付8ビットです。)
***** Veritak SV32 Engine Version 449 Build Jun 26 2013***** obj.a= 45 obj.a= -11 obj.a= -55 obj.a= -66 obj.a= 81 obj.a= -52 obj.a= 74 obj.a= -15 obj.a= -35 obj.a= -70 Info: $finishコマンドを実行します。time=0ns
マイナス値を意図していない場合は、次のように符号なしにすればOKです。
class C;
rand byte unsigned x;
constraint C {
x<=100;
}
endclass
***** Veritak SV32 Engine Version 449 Build Jun 26 2013***** obj.a= 45 obj.a= 53 obj.a= 73 obj.a= 46 obj.a= 53 obj.a= 56 obj.a= 3 obj.a= 42 obj.a= 54 obj.a= 93 Info: $finishコマンドを実行します。time=0ns
SystemVerilog制約ソルバで、連立方程式を解く(Solve simultaneous equations by systemverilog
constraint solver)
3元連立方程式を解きます。変数はx,y,zです。解は、整数であることが分かっているものとします。
（整数でないと解けません。SystemVerilogソルバーは、IntegralTypeのみ(real/shortreal/realtimeは、使えません。）
class C;
rand byte unsigned x,y,z;
constraint C {
2*x+y+z==6;
x+2*y-z==0;
x+y+2*z==4;
}
endclass
program pr2f;
C obj;
initial
begin
obj=new();
repeat(10) begin
void'(obj.randomize());
$display("obj.a=%d %d %d",obj.x,obj.y,obj.z);
end
$finish(2);
end
endprogram
しかし、コンパイル時にエラーがでてしまいます。
（VeritakSVでは、可能な制約については、コンパイル時に解きます。）
------------Starting Verilog Build Process...---------- Verilog プリプロセッサを起動中です。 C:\Users\tak.sugawara\Documents\Visual Studio 2012\Projects\veritak_sv52\test\sim_engine\std\std.sv(1):: Reading C:/Users/Public/sv_test/class_random/pr2f.sv(1):: Reading Verilog プリプロセッシングを終了します。 C:\Users\tak.sugawara\Documents\Visual Studio 2012\Projects\veritak_sv52\test\sim_engine\std\std.sv(5):: Info: 構文解析中です。 C:\Users\Public\sv_test\class_random\pr2f.sv(13):: Info: 構文解析中です。 構文解析が終了しました。 スコープを生成中です。Loading vpi.dll parameterを評価中です。 reg/wire..を評価中です。 moduleを評価中です。 Elaboration Phaseでエラーはありませんでした。コード生成中です... C:\Users\Public\sv_test\class_random\pr2f.sv(7)::Error: 制約を満たす解が見つかりませんでした。 コード生成でエラーが発生したためコンパイルできませんでした。
原因は、変数を"符号なし"にしたためです。符号付に変更します。
class C;
rand byte x,y,z;
今度は、見つかりました。
***** Veritak SV32 Engine Version 449 Build Jun 26 2013***** obj.a= 3 -1 1 obj.a= 3 -1 1 obj.a= 3 -1 1 obj.a= 3 -1 1 obj.a= 3 -1 1 obj.a= 3 -1 1 obj.a= 3 -1 1 obj.a= 3 -1 1 obj.a= 3 -1 1 obj.a= 3 -1 1 Info: $finishコマンドを実行します。time=0ns
SystemVerilog制約ソルバで、２次方程式を解く(Solve a quadratic equation by systemverilog constraint solver)
class C;
rand bit signed [3:0] x;
constraint C {
x *x +6*x +5 ==9'h0;
}
endclass
残念ながら、これも解がありません、と言ってきました。原因は、符号にあります。右辺の9'h0により”符号なし”になってす。VerilogHDLで符号付の評価が行われるのは、RHS/LHS共に符号付のときだけです。それ故に、LHSも符号なしで評価されてしまいます。その結果、解に負の値があるとき、解が見つからない、となってしまいます。
それでは次のソースではどうでしょうか？
class C;
rand int x;
constraint C {
x *x +6*x +5 ==0;
}
endclass
残念ながら、このコンパイルは、大変時間がかかってしまいます。BDD演算にとって、乗算（変数ｘ変数）は、大変にメモリを食います。ビット幅に対して指数関数的に内部のメモリを食います。それ故に乗算/割り算/MOD
演算は、使わないことをお勧めします。どうしても使う場合には、次のようにビット幅を数ビット程度(多くても8ビット程度）に抑えてください。なお、変数ｘ定数は、それほどセンシティブではありません。
class C;
rand byte x;
constraint C {
x *x +6*x +5 ==0;
}
endclass
program pr2hb;
C obj;
initial
begin
obj=new();
repeat(10) begin
void'(obj.randomize());
$display("obj.x=%d ",obj.x);
end
$finish(2);
end
endprogram
***** Veritak SV32 Engine Version 449 Build Jun 26 2013***** obj.x= -5 obj.x= -1 obj.x= -5 obj.x= -5 obj.x= -1 obj.x= -5 obj.x= -1 obj.x= -5 obj.x= -5 obj.x= -1 Info: $finishコマンドを実行します。time=0ns
SystemVerilog制約ソルバで、3次方程式を解く(Solve a cubic equation by systemverilog constraint solver)
rand byte x;
constraint C {
x*x *x +6*x*x +3*x-2 ==0;
}
***** Veritak SV32 Engine Version 449 Build Jun 28 2013***** obj.x= -1 obj.x= -1 obj.x= -1 obj.x= -1 obj.x= -1 obj.x= -1 obj.x= -1 obj.x= -1 obj.x= -1 obj.x= -1 Info: $finishコマンドを実行します。time=0ns
class C;
rand int x1,x2,x3;
rand int y1,y2,y3;
rand int z1,z2,z3;
rand int s;
function void check();
if (s !==x1+x2+x3) $display("Fail");
if (s !==y1+y2+y3) $display("Fail");
if (s !==z1+z2+z3) $display("Fail");
if (s !==x1+y1+z1) $display("Fail");
if (s !==x2+y2+z2) $display("Fail");
if (s !==x3+y3+z3) $display("Fail");
if (s !==x1+y2+z3) $display("Fail");
if (s !==x3+y2+z1) $display("Fail");
endfunction
constraint Equations {
x1+x2+x3==s;//縦横を足してある整数sになります。
y1+y2+y3==s;
z1+z2+z3==s;
x1+y1+z1==s;
x2+y2+z2==s;
x3+y3+z3==s;
x1+y2+z3==s;//対角線を足してある整数sになります。
x3+y2+z1==s;
x1 !=x2;//互いに異なる数です。
x1 !=x3;
x1 !=y1;
x1 !=y2;
x1 !=y3;
x1 !=z1;
x1 !=z2;
x1 !=z3;
x2 !=x3;
x2 !=y1;
x2 !=y2;
x2 !=y3;
x2 !=z1;
x2 !=z2;
x2 !=z3;
x3 !=y1;
x3 !=y2;
x3 !=y3;
x3 !=z1;
x3 !=z2;
x3 !=z3;
y1 !=y2;
y1 !=y3;
y1 !=z1;
y1 !=z2;
y1 !=z3;
y2 !=y3;
y2 !=z1;
y2 !=z2;
y2 !=z3;
y3 !=z1;
y3 !=z2;
y3 !=z3;
z1 !=z2;
z1 !=z3;
z2 !=z3;
x1 >=1;//1から9までの数です。
x1 <=9;
x2>=1;
x2<=9;
x3>=1;
x3<=9;
y1>=1;
y1<=9;
y2>=1;
y2<=9;
y3>=1;
y3<=9;
z1>=1;
z1<=9;
z2>=1;
z2<=9;
//z3>=1;
//z3<=9;
}
endclass
program pr2;
C obj;
initial
begin
obj=new();
repeat(10) begin
void'(obj.randomize());
$display("%d %d %d",obj.x1,obj.x2,obj.x3);
$display("%d %d %d",obj.y1,obj.y2,obj.y3);
$display("%d %d %d",obj.z1,obj.z2,obj.z3);
$display("");
obj.check();
end
$finish(2);
end
endprogram
制約をすこしづつ追加しながら、様子を見たのですが、中々解が収束する雰囲気がしませんでした。（３次の魔方陣は、一つしかありません。）
最終的に上のような記述になりました。一般に、SAT型のソルバの方が、高速に見つけることができます。（例えば、巡回セールスマンの問題では、ある条件の下に１０００都市程度を解くソルバが存在しますが、BDDでは、15都市程度が限界と言われています。）
BDD タイプのソルバの利点は、すべての解を列挙できる点です。（SVのrandomizeが全てを列挙するという意味ではなく、ソルバのアーキテクチャ的にという意味です。)これにより解の確率をフラットにできます。SAT型のソルバーは、一点を見つけるのは、速いのですが、解がそれで全部か？という答えは(一回では）得られません。
***** Veritak SV32 Engine Version 449 Build Jun 25 2013*****
6 7 2
1 5 9
8 3 4
6 7 2
1 5 9
8 3 4
2 9 4
7 5 3
6 1 8
6 7 2
1 5 9
8 3 4
8 3 4
1 5 9
6 7 2
4 3 8
9 5 1
2 7 6
4 3 8
9 5 1
2 7 6
6 7 2
1 5 9
8 3 4
6 7 2
1 5 9
8 3 4
2 7 6
9 5 1
4 3 8
Info: $finishコマンドを実行します。time=0ns
制約記述中のState Variableとは
制約の記述中、ランダム化の対象として指定されていない変数を言います。ランダム化対象ではないので、randomize コールで値が変わることはありません。しかし、制約は、実行中のStateVariableの値下での制約になることに注意します。
program cr1;
class bus;
randc bit[1:0] addr;
endclass
bus c1;
initial begin
c1=new;
repeat(25) begin
repeat(4) begin
c1.randomize();
$write("%x", c1.addr);
end
$display("");
end
end
endprogram
の場合は、{0,1,2,3}が取り得る値の全てです。この順列、次の24シーケンスを繰り返します。（出力の仕方は、実装依存です。）
***** Veritak SV32 Engine Version 449 Build Jun 22 2013***** 0123 0312 0321 0213 0231 2130 2103 2310 2301 2013 2031 1302 1320 1032 1023 1230 1203 3102 3120 3012 3021 3210 3201 0132 0123 ---------- シミュレーションを終了します。time=0ns
LRMは、シミュレータに8ビット以上の実装を要求しています。 ですから、8ビットより大きい値は、実装依存です。
意外に少ないと思われるかもしれませんが、制約がない場合、8ビットの場合の順列のパターンは、一体どれ位でしょうか？上の2ビットの場合は、4!=4*3*2*1=24通りでした。3ビットの場合で、8!=40320通りです。8ビットの場合は、256!=256*255*.....*1
となります。このパターン数は、宇宙全体の素粒子の数よりはるかに大きい数で、シミュレータが最後まで行き着くことはないでしょう。
SVのソルバ出力は、一様分布(uniform distribution)
SVソルバが解く確率分布は、一様（均一）になります。この性質は、勿論入力変数が均一に分布したときが前提です。簡単な例で見ていきましょう。
program cr13a;
class bus;
rand bit a;
rand bit b;
constraint C{ a| b ;}
endclass
bus c1;
int map [int];
initial begin
c1=new;
repeat(3000) begin
int i;
c1.randomize();
i={c1.a,c1.b};
map[i]+=1;
$display("c1.a=%b c1.b%b",c1.a,c1.b);
end
$display("map=%p",map);
end
endprogram
この制約前後での確率は、次のようになります。
| a | b | a|b | 制約前確率 | 制約後確率 |
| 0 | 0 | 0 | 1/4 | 0 |
| 0 | 1 | 1 | 1/4 | 1/3 |
| 1 | 0 | 1 | 1/4 | 1/3 |
| 1 | 1 | 1 | 1/4 | 1/3 |
制約後では、それぞれの出現確率は、均一であり1/3になる筈です。 本当にそうなるかシミュレーションしてみます。
***** Veritak SV32 Engine Version 449 Build Jun 28 2013*****
C:\Users\Public\sv_test\class_random\cr13a.sv(17)::Warning: 連想配列のインデックスが存在しません。default値を返します。
c1.a=1 c1.b1
c1.a=1 c1.b1
c1.a=1 c1.b0
c1.a=1 c1.b1
c1.a=1 c1.b0
c1.a=1 c1.b0
c1.a=1 c1.b1
c1.a=0 c1.b1
c1.a=1 c1.b0
....
c1.a=0 c1.b1
c1.a=1 c1.b0
c1.a=1 c1.b1
c1.a=1 c1.b1
c1.a=0 c1.b1
c1.a=1 c1.b0
c1.a=0 c1.b1
c1.a=1 c1.b0
c1.a=1 c1.b0
c1.a=1 c1.b1
c1.a=1 c1.b0
c1.a=1 c1.b0
map='{1:1009,2:1005,3:986}
---------- シミュレーションを終了します。time=0ns
確かに、解の出力は3パターンあり、各々ほぼ1/3の確率になっていることが確かめられました。この性質は、複雑な制約下にあっても同じです。
次の例では、a+b==99 の制約下で出力されるデータを統計処理して、グラフ化してみました。
program cr13;
class bus;
rand bit signed [7:0]a;
rand bit signed [7:0] b;
constraint C{
a+b==8'sd99 ;
a<=0;//a<=0 && a<=127に限定する
b<=0;//b<=0 && b<=127に限定する
}
endclass
bus c1;
int map [int][int];
int a,b;
int f1;
initial begin
c1=new;
repeat(1000000) begin//100万回試行して統計データを取得
c1.randomize();
map[c1.a][c1.b]+=1;
// $display("c1.a=%b c1.b%b",c1.a,c1.b);
end
//2元MAPをCSV形式で出力
f1=$fopen("data.csv","w");
if ( map.first( a ) )begin
do
begin
if (map[a].first(b)) begin
do
begin
$fdisplay(f1, " %d, %d ,%d",a,b,map[a][b] );
end
while (map[a].next(b));
end
end
while ( map.next(a ) );
$fclose(f1);
end
end
endprogram
Z軸が度数を現しています。確かに、一様分布で出力されています。
-SVソルバは、一様分布で出力するために、全部の解がいくつあるかを把握しています。また、内部で複雑な確率計算を行っています。
| 命題 P | 命題 Q | P ⇒ Q |
|---|---|---|
| 真 | 真 | 真 |
| 真 | 偽 | 偽 |
| 偽 | 真 | 真 |
| 偽 | 偽 | 真 |
次の記述で制約の前後で、a==0になる確率と、b==1になる確率がどのように変化するのか計算してみます。
論理包含演算子と制約の関係
1bitの例
次の例では、a==0なら、b==1を制約として附加するということを言っています。反対にa==0が成立しない、つまり a!=0なら、制約を附加しない、つまり自由にランダムに（しかし、等確率となるように）変化してよいという意味になります。
rand bit a, b;
constraint c { (a == 0) -> (b == 1); }
制約前
aとbは、互いに独立です。aは、a==0とa==1の二通りしか存在しないので、それぞれ確率は、1/2です。同様に、b==1と
b==0になる確率も1/2です。
制約（a==0 -> b==1)後
ブール代数的には、上の真理値表にあてはめると、結果が偽になる(候補から除外されるのは、)
a==0 && b !=1 です。制約前は、全ての組み合わせは、4通りのところ、この条件だけが、制約フィルタによって除去されて、出現するのは、3通りになります。
その場合、a==0になるのは、真真の一通りだけですので、確率は、1/3になります。b==1になるのは、真真、偽真の2通りで、確率は、2/3になります。
| a==0 -> b==1 | 制約前 | 制約後 |
| a==0になる確率 | 1/2 | 1/3 |
| b==1になる確率 | 1/2 | 2/3 |
| a | b | remarks |
| 0 | 1 | 制約 |
| 0 | 0 | 制約により禁止 |
| 1 | 0 | 制約されない(RANDOM) |
| 1 | 1 |
上の真理値表は、 a==0 をA, b==1をBとすると
下のように書き換えられます。
| A | B | remarks |
| 1 | 1 | 制約 |
| 1 | 0 | 制約により禁止 |
| 0 | 0 | 制約されない(RANDOM) |
| 0 | 1 |
つまり制約後の論理は、
AB+!A!B+!AB
= AB+ !A(!B+B)
=AB+!A
=AB+!A(1+B)
=AB+!AB+!A
=B(A+!A)+!A
=B+!A
となり、論理包含の定義と一致します。 A->B によって、Bのみならず、Aの確率も変化することに注意してください。
制約を課すことによって、a、b共 出現確率が変化することがわかります。独立していた変数が、制約を課すことで、独立ではなくなります。
制約を課すとは、言い方を変えるとありえないパターン、禁止パターンを定義することです。出現する空間を狭めることを意味します。結果として、相互に出現確率が変化することになります。
-ソルバは、最初に制約された出現空間を求めます。これは、制約後のあらゆるパターンを内包した集合です。
class impli;
rand bit a, b;
constraint c { (a == 0) -> (b == 1); }
endclass
program imp2;
impli obj;
int map[int unsigned] ;
initial
begin
obj=new();
for(int i=0; i< 100000; i++) begin
obj.randomize();
$display("%d",obj.a);
map[obj.a] +=1;
end
$display("%p",map);
$display(" count_0 = %0d count_1 = %0d; a==0となる確率%1.1f[パーセント] Expected:%1.1f[パーセント]",map[0] ,map[1],100.0* map[0]/(map[0]+map[1]),1.0/3*100);
end
endprogram
結果です。
....
1
1
1
0
1
'{0:33331,1:66669}
count_0 = 33331 count_1 = 66669; a==0となる確率33.3[パーセント] Expected:33.3[パーセント]
---------- シミュレーションを終了します。time=0ns
期待値=1/3 =>33.3%と一致しました。
2bitの例
class impli;
rand bit a;
rand bit [1:0] b;
constraint c { (a == 0) -> (b == 0); }
endclass
program impli_p3a;
impli obj;
int map[int unsigned] ;
parameter int NUM=10000;
initial
begin
obj=new();
for(int i=0; i< NUM; i++) begin
obj.randomize();
$display("%d",obj.a);
map[obj.a] +=1;
end
$display("%p",map);
$display(" count_0 = %0d ; %1.1f% Expected:%1.1f%",map[0] ,100.0* map[0]/NUM,1.0/5*100);
end
endprogram
'{0:1983,1:8017}
count_0 = 1983 ; 19.8Expected:20.0
---------- シミュレーションを終了します。time=0ns
| 解 | a | b | 確率 | |
| A | 0 | 0 | 1/5 | 制約 |
| B | 0 | 1 | 0 | 制約により禁止 |
| C | 0 | 2 | 0 | |
| D | 0 | 3 | 0 | |
| E | 1 | 0 | 1/5 | 制約がない（RANDOM) |
| F | 1 | 1 | 1/5 | |
| G | 1 | 2 | 1/5 | |
| H | 1 | 3 | 1/5 |
この例は、SystemVerilog for Verification Table 6.5 (3rd Edition) に同じですが、上が正しい結果になります。
rand [3:0]bit a, b;
constraint c { (a == 0) -> (b == 1); }
制約前
aとbは、互いに独立ですから、aは、4ビットで全部で2の4乗＝16個の組み合わせが存在します。このうちa==0になるのは、1個しかないので、1/16です。同様に、b==1となる確率は1/16です。
制約（a==0 -> b==1)後
ブール代数的には、上の真理値表にあてはめると、結果が偽になる(候補から除外されるのは、)
a==0 && b !=1 です。制約前は、全ての組み合わせは、2の8乗=256通りのところ、この条件だけが、制約フィルタによって除去されます。a==0になるのは、一個、b!=1
になるのは、15個ですから、1*15=15個が禁止パターンとして除外されます。出現空間としては、256-15=241通りです。
上の真理値表で、a==0になるのは、真真だけです。(真偽は、禁止パターンで除外済） つまり、a==0 &&
b==1だけですので、確率は、1/241になります。b==1になるのは、真真、偽真の2通りです。真真は、1通り、偽真は、a!=0
&& b==1となるのは、15通りですから、合計16通り
| a==0 | b==1 | P ⇒ Q |
|---|---|---|
| a==0 | b==1 | 1通り |
|
|
|
|
| !(a==0) | 15通り | |
| !(a==0) | !(b==1) | 15*15＝225通り |
結果、下表のよう意外な結果になります
| a==0 -> b==1 | 制約前 | 制約後 |
| a==0になる確率 | 1/16 | 1/241 |
| b==1になる確率 | 1/16 | 16/241 |
このように、論理包含演算(Implication)は、双方に影響を与えます。
class impli;
rand bit [3:0] a, b;
constraint c { (a == 0) -> (b == 1); }
endclass
program imp2a;
impli obj;
int map[int unsigned] ;
initial
begin
obj=new();
for(int i=0; i< 100000; i++) begin
obj.randomize();
$display("%d",obj.a);
map[obj.a] +=1;
end
$display("%p",map);
$display(" count_0 = %0d count_1 = %0d; a==0となる確率%1.1f[パーセント] Expected:%1.1f[パーセント]",map[0] ,map[1],100.0* map[0]/(100000),1.0/241.0*100);
end
endprogram
...
8
10
4
11
7
10
13
13
'{0:433,1:6581,2:6576,3:6638,4:6644,5:6727,6:6631,7:6621,8:6566,9:6753,10:6743,11:6735,12:6599,13:6442,14:6745,15:6566}
count_0 = 433 count_1 = 6581; a==0となる確率0.4[パーセント] Expected:0.4[パーセント]
---------- シミュレーションを終了します。time=0ns
このように、a==０の確率が随分小さくなってしまいました。
特定の変数を等確率で発生させるには
上で a==0 の確率は、1/241となり、大部分は、a==1(240/241)になってしまいます。全体の事象から見れば等確率で、公平なテストですが、a==0だけの確率に着目すると非効率なテストに見えます。
そこで、aの発生事象を等確率にしたいときは、次のように
solve a before b構文を使います。
rand bit [3:0]a,b;
constraint c {
(a == 0) -> (b ==1);
solve a before b;
}
solve before 構文の追加で解の空間は変りませんが、確率が変化します。aは、最初に a==0
からa==15までの任意の値がランダムに等確率で生成されます。次に、bの値が、制約に見合うように決定されます。
-この構文がない場合には、全体事象から見て、等確率となるように、a,bの値が決定されます。BDD上ではボトムアップ操作で確率が決定されます。一方、solve
a before b については、 BDD上のノードaをトップに置いて（少なくともaは、bよりも上に置いて）、トップダウン的に決定されます。
class impli;
rand bit [3:0]a,b;
constraint c {
(a == 0) -> (b ==1);
solve a before b;
}
endclass
program impli3e;
impli obj;
int map[int unsigned] ;
parameter int NUM=100000;
initial
begin
obj=new();
for(int i=0; i< NUM; i++) begin
obj.randomize();
map[obj.a] +=1;
end
$display("%p",map);
end
endprogram
***** Veritak SV32 Engine Version 449 Build Jul 14 2013*****
C:\Users\Public\sv_test\class_random\imp3e.sv(24)::Warning: 連想配列のインデックスが存在しません。default値を返します。
'{0:6236,1:6127,2:6201,3:6340,4:6346,5:6208,6:6228,7:6314,8:6229,9:6349,10:6137,11:6381,12:6338,13:6215,14:6191,15:6160}
---------- シミュレーションを終了します。time=0ns
| a==0 -> b==1 | 制約前 | 制約後 | 制約後(solve a before b;) |
| a==0になる確率 | 1/16 | 1/241 | 1/16 |
先ほどの2ビットの例でまとめると以下のようになります。
制約前
禁止パターンがなく、すべてのパターンが等確率になります。
| 解 | a | b | 確率 |
| A | 0 | 0 | 1/8 |
| B | 0 | 1 | 1/8 |
| C | 0 | 2 | 1/8 |
| D | 0 | 3 | 1/8 |
| E | 1 | 0 | 1/8 |
| F | 1 | 1 | 1/8 |
| G | 1 | 2 | 1/8 |
| H | 1 | 3 | 1/8 |
制約後 (a == 0) -> (b == 0);
禁止パターンの確率は0です。a==0となる確率は、1/5, a==1となる確率は、4/5です。
| 解 | a | b | 確率 |
| A | 0 | 0 | 1/5 |
| B | 0 | 1 | 0 |
| C | 0 | 2 | 0 |
| D | 0 | 3 | 0 |
| E | 1 | 0 | 1/5 |
| F | 1 | 1 | 1/5 |
| G | 1 | 2 | 1/5 |
| H | 1 | 3 | 1/5 |
制約後 (a == 0) -> (b == 0); solve a before b;
a==0 が1/2 a==1が1/2と 等確率になります。
| 解 | a | b | 確率 |
| A | 0 | 0 | 1/2 |
| B | 0 | 1 | 0 |
| C | 0 | 2 | 0 |
| D | 0 | 3 | 0 |
| E | 1 | 0 | 1/8 |
| F | 1 | 1 | 1/8 |
| G | 1 | 2 | 1/8 |
| H | 1 | 3 | 1/8 |
制約後 (a == 0) -> (b == 0); solve b before a;
b==0, b==1,b==2,b==3 が等確率で1/4になっています。
| 解 | a | b | 確率 |
| A | 0 | 0 | 1/8 |
| B | 0 | 1 | 0 |
| C | 0 | 2 | 0 |
| D | 0 | 3 | 0 |
| E | 1 | 0 | 1/8 |
| F | 1 | 1 | 1/4 |
| G | 1 | 2 | 1/4 |
| H | 1 | 3 | 1/4 |
上の結果は、下のベンチで確認しました。
class impli;
rand bit [1:0]b,c;
rand bit a;
constraint c {
(a == 0) -> (b ==0);
solve b before a;
}
endclass
program impli3c;
impli obj;
int map[int unsigned][int unsigned] ;
parameter int NUM=10000;
initial
begin
obj=new();
for(int i=0; i< NUM; i++) begin
obj.randomize();
$display("b=%d c=%d",obj.b,obj.c);
map[obj.a][obj.b] +=1;
end
$display("%p",map);
end
endprogram
結果です。
....
b=3 c=0
b=2 c=1
b=2 c=3
b=2 c=1
b=3 c=0
b=0 c=0
'{0:'{0:1195},1:'{0:1239,1:2517,2:2540,3:2509}}
---------- シミュレーションを終了します。time=0ns
solve beforeによる確率空間の変化
解全体集合としては、変化がありませんが、個々の確率が変化します。
class slove_before;
rand bit [2:0] x,y;
constraint C {
x < y;
//solve x before y;
}
endclass
program imp3g0;
slove_before obj ;
int map [int unsigned ];
parameter int NUM=100000;
initial
begin
obj = new();
repeat(NUM) begin
obj.randomize();
map[obj.x] +=1;
$display(" x : %d :: y :%d ",obj.x,obj.y);
end
$display("%p",map);
end
endprogram
この確率分布は、次のように求まります。
組み合わせの総数 Sumは、等差数列の和公式より、Sum=7(7+1)/2=28通りです。
| x | y | 確率 | |
| 6 | 7 | 1/28 | 3.6% |
| 5 | 6,7 | 2/28 | 7.1% |
| 4 | 5,6,7 | 3/28 | 10.7% |
| 3 | 4,5,6,7 | 4/28 | 14.2% |
| 2 | 3,4,5,6,7 | 5/28 | 17.8% |
| 1 | 2,3,4,5,6,7 | 6/28 | 21.4% |
| 0 | 1,2,3,4,5,6,7 | 7/28 | 25% |
この理論値に対して、
.....
x : 2 :: y :3
x : 0 :: y :1
x : 2 :: y :5
x : 0 :: y :2
x : 0 :: y :2
x : 2 :: y :5
x : 5 :: y :6
x : 0 :: y :4
x : 3 :: y :6
'{0:24992,1:21509,2:18026,3:14206,4:10527,5:7213,6:3527}
---------- シミュレーションを終了します。time=0ns
ソルバは、全体の解空間中の全ての解に対して、確率を均一に出力していることが分かります。
ｘについて、solve before を追加すると、
constraint C {
x < y;
solve x before y;
}
.....
x : 2 :: y :7
x : 1 :: y :3
x : 0 :: y :3
x : 2 :: y :3
x : 0 :: y :7
x : 4 :: y :7
x : 3 :: y :4
x : 6 :: y :7
'{0:14242,1:14312,2:14272,3:14219,4:14358,5:14370,6:14227}
解x=0-6が出力される事自体は変りありません。しかし、個々のｘについては、均一な確率となっています。
solve x beforeによって、まず、ｘの分布が均一になるようにｘの値が決定されます。次に残ったyが制約を満たすように選ばれます。
-BDDの実装アルゴリズムは、次の通りです。
1) ORDERに従いグラフ化（ループ検出->循環エラー）、BDDのINDEXを与える。(bit
Indexは、interleaved,のまま。 bit indexまでreorderingすると、BDDが爆発することがあるので不可)
2) BDDを構築する
3) Ordered Variableについて、単独のパス重みを求める。
4) Ordered Variableの値を求める。(BDD traverse)
5) Ordered VariableをStateVariableとして全体のパス重みを求める
6) 全ての変数の値を求める (BDD traverse)
このうち、RUNTIMEでは、３）−６）が必要になります。
solve before の制限事項
解の空間は変化しないので、基本的には、この構文の追加によって理屈的には、「解がありません。」と言ってくることはありません。
次の例のように、yについて、自明な解がある場合でも、その条件下での確率をフラットにします。（ユーザサイドで特に気をつける必要はありません。）
class slove_before;
rand int unsigned x,y;
constraint C {
x < y;
y==5;
solve x before y;
}
endclass
...
x : 2 :: y : 5
x : 1 :: y : 5
x : 2 :: y : 5
x : 4 :: y : 5
x : 4 :: y : 5
x : 3 :: y : 5
x : 4 :: y : 5
x : 3 :: y : 5
'{0:189,1:210,2:202,3:187,4:212}
一般的な注意事項として、
があります。
if else 制約
基本的に、->と同じ動きをします。(A/B..双方向に確率が変化することに注意してください。）
if (A) B; 制約は、 A->B に全く同じです。（同じ確率分布になります。）
constraint c {
if (a == 0) (b ==0);//a==0 -> b==0に同じ
}
if (A) B; else C制約は、
constraint c {
if (a == FINISHED) (b ==0);//a==FINISHED -> b==0;
else b>=2;//a!=FINISHED -> b>=2;
}
次の -> に等価です。（同じ確率分布になります。)
A->B;
!A-> C;
constraint c {
a==FINISHED -> b==0;
a!=FINISHED -> b>=2;
}
次のif (A) B; else if (C) D; else E;制約は、
constraint c {
if ( a==FINISHED ) b==0;
else if( a==RUNNING) b==1;
else b>=2;
}
次の->に等価です。
class impli;
rand bit [1:0]b,c;
rand enum bit [1:0] { FINISHED=0, RUNNING=1, WAITING=2, SUSPENDED=3 } a;
constraint c {
a==FINISHED -> b==0;
a==RUNNING -> b==1;
!(a==FINISHED || a==RUNNING) -> b>=2;
}
endclass
program impli3aif02;
impli obj;
int map[int unsigned][int unsigned] ;
parameter int NUM=1000;
initial
begin
obj=new();
for(int i=0; i< NUM; i++) begin
obj.randomize();
$display("b=%d c=%d",obj.b,obj.c);
map[obj.a][obj.b] +=1;
end
$display("%p",map);
end
endprogram
....
b=2 c=2
b=2 c=1
b=1 c=0
b=2 c=2
b=1 c=1
b=1 c=2
b=2 c=1
b=3 c=1
'{0:'{0:152},1:'{1:176},2:'{2:149,3:169},3:'{2:194,3:160}}
---------- シミュレーションを終了します。time=0ns
foreach イタレータ制約
配列に関してまとめて書きたいときに使います。魔法陣の例では、3x3行列を表現するのに、9つの変数を使いました。これを、3x3配列で表現すると、各要素は、foreachで宣言した変数を使って表現できます。そうすると、多くの制約式をまとめて書ける場合(下ソース12行目、20行目,28行目)があります。（下ソースでは、魔法陣のソースを配列を使って書き換えました。参考にしました。）
class C;
parameter int unsigned N = 3;
parameter int unsigned M = ((N*N*N)+N)/2;
rand bit [3:0] X[N][N];
constraint Equations {
// Row sums
foreach (X[i,]) {// 制約セットは、begin-endではなく { } で囲む
X[i][0]+X[i][1]+X[i][2]==M;
//X[0][0]+X[0][1]+X[0][2]==M;
//X[1][0]+X[1][1]+X[1][2]==M;
//X[2][0]+X[2][1]+X[2][2]==M;
//と等価
}
// Column sums
foreach (X[,j]) {
X[0][j] +X[1][j]+X[2][j]==M;
//X[0][0]+X[1][0]+X[2][0]==M;
//X[0][1]+X[1][1]+X[2][1]==M;
//X[0][2]+X[1][2]+X[2][2]==M;
//と等価
}
// All entries between 1 and 9
foreach (X[i,j]) X[i][j] inside { [1:N*N] };
// X[0][0] >=1 && X[0][0] <=N*N;
// X[0][1] >=1 && X[0][1] <=N*N;
// X[0][2] >=1 && X[0][2] <=N*N;
// X[1][0] ...
// X[2][2] >=1 && X[2][2] <=N*N;
//と等価
// Diagonal sums
X[0][0] + X[1][1] + X[2][2] == M;
X[0][2] + X[1][1] + X[2][0] == M;
// Unique entries
X[0][0] !=X[0][1];
X[0][0] !=X[0][2];
X[0][0] !=X[1][0];
X[0][0] !=X[1][1];
X[0][0] !=X[1][2];
X[0][0] !=X[2][0];
X[0][0] !=X[2][1];
X[0][0] !=X[2][2];
X[0][1] !=X[0][2];
X[0][1] !=X[1][0];
X[0][1] !=X[1][1];
X[0][1] !=X[1][2];
X[0][1] !=X[2][0];
X[0][1] !=X[2][1];
X[0][1] !=X[2][2];
X[0][2] !=X[1][0];
X[0][2] !=X[1][1];
X[0][2] !=X[1][2];
X[0][2] !=X[2][0];
X[0][2] !=X[2][1];
X[0][2] !=X[2][2];
X[1][0] !=X[1][1];
X[1][0] !=X[1][2];
X[1][0] !=X[2][0];
X[1][0] !=X[2][1];
X[1][0] !=X[2][2];
X[1][1] !=X[1][2];
X[1][1] !=X[2][0];
X[1][1] !=X[2][1];
X[1][1] !=X[2][2];
X[1][2] !=X[2][0];
X[1][2] !=X[2][1];
X[1][2] !=X[2][2];
X[2][0] !=X[2][1];
X[2][0] !=X[2][2];
X[2][1] !=X[2][2];
// foreach (X[x,y])
// foreach (X[i,j])
// if ((x < i) || (y < j))
// X[x][y] != X[i][j];
}
// Convert the solution to a string
function void to_string();
for (int i = 0; i < N; i++) begin
for (int j = 0; j < N; j++) $write("%1d ", X[i][j]);
$display("");
end
$display("");
endfunction : to_string
// Sanity Check
function void check();
foreach (X[i,]) begin
if (X[i][0]+X[i][1]+X[i][2]!=M) $display("Fail");
end
foreach (X[,j]) begin
if (X[0][j] +X[1][j]+X[2][j]!=M) $display("Fail");
end
foreach (X[i,j]) if (X[i][j] %lt;1 || X[j][j] >N*N) $display("Fail");
if(X[0][0] + X[1][1] + X[2][2] != M) $display("Fail");
if( X[0][2] + X[1][1] + X[2][0] != M) $display("Fail");
endfunction
endclass
program array2;
C obj;
initial
begin
obj=new();
repeat(5) begin
void'(obj.randomize());
obj.to_string();
// foreach (obj.X[i,j])
// $display("X[%1d][%1d]=%d",i,j,obj.X[i][j]);
obj.check();
end
$finish(2);
end
endprogram
***** Veritak SV32 Engine Version 449 Build Jul 30 2013***** 6 7 2 1 5 9 8 3 4 4 9 2 3 5 7 8 1 6 4 3 8 9 5 1 2 7 6 2 9 4 7 5 3 6 1 8 8 1 6 3 5 7 4 9 2 Info: $finishコマンドを実行します。time=0ns
foreachの変数は、制約上では、実行時定数であることに注意してください。制約式を見た目上まとめる効果しかありません。ソース的には一行でも、内部的には、多数の制約を課していることになるので、大量のメモリ食いまたは遅くなる可能性があります。
if は、論理包含(Implication)のif それとも ガードのif ?
制約中のif は、次の二つの意味があり別物です。
どちらも、if (A) B の形ですので、構文的には、判断できません。
| 意味 | 制約適用後 | A | |
| 論理包含 (Implication) | A->Bに等価 | ！A||B | Aは、rand/randc変数を含む項 |
| ガード項(Expression) | Aがtrueなら制約Bを適用。Aがfalseなら制約Bは、適用しない。 | B | Aは、rand/randc変数を含まない |
なので、Aの項のプロパティを見て、判断することが必要です。
上のソースで、
// Unique entries
X[0][0] !=X[0][1];
X[0][0] !=X[0][2];
X[0][0] !=X[1][0];
X[0][0] !=X[1][1];
X[0][0] !=X[1][2];
X[0][0] !=X[2][0];
X[0][0] !=X[2][1];
X[0][0] !=X[2][2];
X[0][1] !=X[0][2];
X[0][1] !=X[1][0];
X[0][1] !=X[1][1];
X[0][1] !=X[1][2];
X[0][1] !=X[2][0];
X[0][1] !=X[2][1];
X[0][1] !=X[2][2];
X[0][2] !=X[1][0];
X[0][2] !=X[1][1];
X[0][2] !=X[1][2];
X[0][2] !=X[2][0];
X[0][2] !=X[2][1];
X[0][2] !=X[2][2];
X[1][0] !=X[1][1];
X[1][0] !=X[1][2];
X[1][0] !=X[2][0];
X[1][0] !=X[2][1];
X[1][0] !=X[2][2];
X[1][1] !=X[1][2];
X[1][1] !=X[2][0];
X[1][1] !=X[2][1];
X[1][1] !=X[2][2];
X[1][2] !=X[2][0];
X[1][2] !=X[2][1];
X[1][2] !=X[2][2];
X[2][0] !=X[2][1];
X[2][0] !=X[2][2];
X[2][1] !=X[2][2];
は、「同じ数字が入らない」という制約を述べたものですが、foreach とガード項を使って、別表現として次のように短く表現できます。
foreach (X[x,y])
foreach (X[i,j])
if ((x < i) || (y < j))
X[x][y] != X[i][j];
ここで、x,y,i,jは、foreachのローカル変数ですが、制約評価時には、定数であることを思いだしてください。なので、if
(x<i || y< j ) の x<i の結果は、定数として判断出来、y< j の結果も定数として判断することが出来ます。結果として、implication
演算ではなく、ガード項になることが分かります。
SystemVerilog制約ソルバで、数独を解く(Solve sudoku by using systemverilog
constraint solver)
sudokuは、有名なパズルです。N=2については、BDDソルバで全解を求めることができます。
class Sudoku ;
parameter int N=2;
// The random Sudoku table
rand bit[3:0] X[N**2][N**2];
// Helper arrays
local bit[3:0] box[N-1];
function void to_string();
for (int i = 0; i < N**2; i++) begin
for (int j = 0; j < N**2; j++) $write("%1d ", X[i][j]);
$display("");
end
$display("");
endfunction : to_string
// Random table constraints
constraint con_rtab {
foreach (X[i,j]) {
foreach (X[k,]) // Unique colums
if (i < k) X[i][j] != X[k][j];
foreach (X[,m])// Unique rows
if (j<m) X[i][j] !=X[i][m];
X[i][j] inside {[1:N**2]};// All entries between 1 and N^2
foreach (box[x]) // Unique NxN
foreach (box[y])
X[i][j] != X[i-i%N+(i+x+1)%N][j-j%N+(j+y+1)%N];
}
}
endclass: Sudoku
program sudoku1;
Sudoku obj;
initial
begin
obj=new();
repeat(5) begin
void'(obj.randomize());
obj.to_string();
end
$finish(2);
end
endprogram
***** Veritak SV32 Engine Version 449 Build Aug 1 2013***** 3 1 2 4 4 2 1 3 1 4 3 2 2 3 4 1 4 3 2 1 1 2 3 4 3 1 4 2 2 4 1 3 2 4 1 3 1 3 4 2 3 1 2 4 4 2 3 1 3 2 1 4 1 4 2 3 2 3 4 1 4 1 3 2 2 3 1 4 1 4 2 3 4 1 3 2 3 2 4 1 Info: $finishコマンドを実行します。time=0ns
sudokuを制約プログラミングで解く例は、沢山(ruby, python,Haskell...)ありますが、上の制約記述は、そのような超高級言語に比しても短く書けています。（しかもNをパラメータにして。） SystemVerilogは、CMOSトランジスタやネットリストを扱う低級な言語である反面、このような高級な記述も出来ます。モンスターフランケンシュタインな言語であることに同意です。上のソースはこちらの改変です。
SAT型ソルバで、数独を解く
N=3
N=3については、BDDの爆発が生じ（Reasonableな時間とメモリの範囲内で）解くことはできませんでした。BDDで求められる範囲は、それほど広範囲ではなく、変数の個数は、数百程度とされています。BDDは、
といったランダムスティミュラス生成上の利点があるのですが、算術演算が苦手で、特に算術不等式では、10変数程度でも解空間を求めることができなくなります。
そういう訳で、シミュレータは、BDDソルバ以外に、SAT型のソルバも搭載しています。SAT型のソルバは、命題論理に対して、解がある場合には、一つの解を出力します。SAT型のソルバは、全解空間を一度に出力することはできませんが、変数の規模制限は、BDDに比べればずっと緩やかです。（近年、SAT手法は、急速に進歩しています。）
そこで、数独N=3については、SAT型ソルバで求めてみます。
***** Veritak SV32 Engine Version 449 Build Aug 7 2013***** 2 6 8 7 4 3 1 5 9 5 3 4 2 9 1 6 8 7 9 1 7 6 8 5 4 2 3 7 9 2 1 5 4 8 3 6 6 8 3 9 7 2 5 4 1 1 4 5 8 3 6 7 9 2 4 2 1 5 6 9 3 7 8 3 7 6 4 2 8 9 1 5 8 5 9 3 1 7 2 6 4 2 6 8 3 4 7 1 5 9 5 3 4 2 9 1 6 8 7 9 1 7 6 8 5 4 2 3 7 9 2 1 5 4 8 3 6 6 8 3 9 7 2 5 4 1 1 4 5 8 3 6 7 9 2 4 2 1 5 6 9 3 7 8 3 7 6 4 2 8 9 1 5 8 5 9 7 1 3 2 6 4 4 9 6 1 3 8 5 7 2 5 2 8 9 4 7 3 1 6 1 3 7 5 2 6 4 9 8 8 7 5 3 1 4 2 6 9 2 1 3 8 6 9 7 4 5 6 4 9 7 5 2 8 3 1 9 6 2 4 8 3 1 5 7 3 8 1 6 7 5 9 2 4 7 5 4 2 9 1 6 8 3 3 2 1 7 8 9 5 4 6 5 8 9 3 6 4 7 2 1 7 4 6 2 5 1 3 9 8 9 3 7 4 2 6 8 1 5 1 5 2 8 7 3 4 6 9 8 6 4 1 9 5 2 7 3 6 7 5 9 3 2 1 8 4 4 9 8 5 1 7 6 3 2 2 1 3 6 4 8 9 5 7 6 2 4 8 9 5 7 1 3 3 5 9 2 7 1 6 4 8 7 1 8 3 6 4 5 9 2 9 6 3 4 1 7 8 2 5 5 7 1 9 2 8 4 3 6 8 4 2 5 3 6 9 7 1 4 3 7 6 5 2 1 8 9 2 8 6 1 4 9 3 5 7 1 9 5 7 8 3 2 6 4 Info: $finishコマンドを実行します。time=0ns **** Test Done. Total 144.00[msec] ****
N=4
N=4では、かなり遅くなりました。SATソルバは、CNF形式で制約を与えますが、N=4では、約16万節(clause)になっていました。（ビットのEncodeを0-15とすれば、少し緩くなります。） 数独をSATソルバで解くには、CNFへのエンコードに工夫が要りますが、上のようなダイレクトな記述でもそこそこに解いてくれることがわかりました。
***** Veritak SV32 Engine Version 449 Build Aug 7 2013***** 6 5 12 3 9 10 7 16 14 11 1 2 8 15 4 13 11 8 2 14 15 13 3 5 12 16 7 4 9 1 6 10 7 16 9 15 11 4 2 1 6 10 13 8 12 5 3 14 13 10 4 1 12 8 6 14 15 9 3 5 7 11 2 16 15 13 10 9 16 12 14 6 1 3 5 11 4 7 8 2 12 6 3 2 8 1 4 10 9 14 16 7 15 13 11 5 4 7 1 16 5 11 15 9 8 6 2 13 10 3 14 12 8 14 5 11 2 3 13 7 4 15 12 10 16 6 9 1 14 2 11 6 3 16 10 4 7 5 15 12 13 8 1 9 9 4 13 8 1 15 5 12 10 2 6 3 11 14 16 7 3 1 16 12 7 6 8 13 11 4 9 14 5 2 10 15 5 15 7 10 14 2 9 11 16 13 8 1 6 4 12 3 10 9 8 7 4 5 16 3 2 1 11 15 14 12 13 6 1 12 14 5 6 7 11 2 13 8 10 9 3 16 15 4 2 11 6 13 10 14 12 15 3 7 4 16 1 9 5 8 16 3 15 4 13 9 1 8 5 12 14 6 2 10 7 11 10 14 16 1 15 3 12 2 7 9 6 5 8 4 11 13 7 8 5 4 1 10 9 6 11 12 13 3 15 2 14 16 15 2 13 3 14 11 5 7 16 8 10 4 12 6 1 9 6 11 12 9 13 16 8 4 1 14 15 2 3 10 7 5 8 13 6 11 7 9 4 16 5 3 1 15 2 12 10 14 14 9 2 7 10 6 1 5 12 16 4 13 11 3 15 8 5 10 1 15 2 12 3 11 14 6 8 9 4 16 13 7 3 12 4 16 8 13 15 14 10 2 7 11 5 1 9 6 16 6 14 2 5 8 11 15 13 10 12 1 7 9 4 3 1 3 9 13 12 4 6 10 8 7 2 14 16 15 5 11 4 15 10 8 16 2 7 3 9 5 11 6 13 14 12 1 11 5 7 12 9 14 13 1 15 4 3 16 6 8 2 10 13 7 3 5 6 1 14 12 2 15 16 10 9 11 8 4 12 16 15 6 11 5 10 13 4 1 9 8 14 7 3 2 9 4 11 10 3 15 2 8 6 13 14 7 1 5 16 12 2 1 8 14 4 7 16 9 3 11 5 12 10 13 6 15 15 8 14 12 16 1 13 10 9 6 2 7 5 4 11 3 7 3 9 16 2 11 14 12 5 15 10 4 6 13 1 8 10 2 11 4 3 15 6 5 14 1 13 8 7 16 12 9 13 5 6 1 7 4 9 8 11 16 12 3 14 15 10 2 6 7 3 5 11 9 10 1 15 2 8 13 12 14 4 16 12 11 13 15 14 2 5 16 10 4 6 9 8 7 3 1 16 1 10 2 4 7 8 15 12 5 3 14 9 11 13 6 4 9 8 14 6 12 3 13 1 7 11 16 10 2 5 15 9 13 12 10 1 6 4 14 16 11 7 15 3 8 2 5 14 15 5 3 9 8 2 7 13 10 1 12 4 6 16 11 1 4 2 7 10 16 12 11 8 3 5 6 13 9 15 14 11 6 16 8 5 13 15 3 4 14 9 2 1 10 7 12 2 16 4 6 12 5 7 9 3 13 14 11 15 1 8 10 5 14 7 13 8 10 16 2 6 12 15 1 11 3 9 4 3 12 1 9 15 14 11 4 7 8 16 10 2 5 6 13 8 10 15 11 13 3 1 6 2 9 4 5 16 12 14 7 14 1 10 3 4 15 2 11 5 12 13 8 7 16 9 6 11 9 6 5 8 3 12 7 15 14 16 10 2 13 4 1 4 7 8 15 6 14 13 16 3 9 1 2 11 12 5 10 16 12 2 13 10 5 1 9 7 4 11 6 8 14 3 15 8 14 9 16 15 13 7 5 1 3 6 4 10 11 12 2 2 11 4 12 3 9 16 14 13 10 15 5 6 1 8 7 5 3 13 6 2 1 4 10 11 7 8 12 9 15 16 14 15 10 7 1 11 12 8 6 2 16 14 9 3 5 13 4 12 15 11 2 5 4 6 1 16 8 10 3 13 7 14 9 9 13 5 14 16 11 10 3 4 6 2 7 1 8 15 12 1 4 3 10 13 7 9 8 14 11 12 15 5 2 6 16 7 6 16 8 12 2 14 15 9 13 5 1 4 10 11 3 13 5 15 9 7 10 11 4 12 1 3 16 14 6 2 8 6 2 12 4 9 8 5 13 10 15 7 14 16 3 1 11 3 16 14 7 1 6 15 2 8 5 4 11 12 9 10 13 10 8 1 11 14 16 3 12 6 2 9 13 15 4 7 5 8 14 6 10 3 15 12 7 2 11 16 4 5 13 1 9 12 15 11 9 4 1 5 2 7 13 6 8 14 3 10 16 16 1 2 13 11 8 9 6 14 10 5 3 4 15 7 12 7 5 4 3 14 10 16 13 12 15 1 9 2 8 6 11 9 12 7 4 15 16 3 14 5 8 11 1 13 10 2 6 3 2 15 6 8 11 13 1 16 14 7 10 12 9 4 5 14 13 10 8 5 7 6 9 4 3 2 12 15 11 16 1 1 11 16 5 2 4 10 12 9 6 15 13 8 14 3 7 2 16 3 14 10 9 8 15 6 1 4 7 11 5 12 13 10 4 5 12 7 14 11 3 13 16 9 15 1 6 8 2 15 6 1 7 13 5 2 16 8 12 14 11 3 4 9 10 13 9 8 11 12 6 1 4 3 5 10 2 7 16 15 14 4 7 12 1 6 13 15 10 11 9 8 14 16 2 5 3 11 3 14 15 16 2 7 5 10 4 12 6 9 1 13 8 5 10 9 2 1 3 14 8 15 7 13 16 6 12 11 4 6 8 13 16 9 12 4 11 1 2 3 5 10 7 14 15 Info: $finishコマンドを実行します。time=0ns **** Test Done. Total 1015924.00[msec] ****
class Sudoku ;
parameter int N=4;
// The random Sudoku table
rand bit[4:0] X[N**2][N**2];
// Helper arrays
local bit[4:0] box[N-1];
function void to_string();
for (int i = 0; i < N**2; i++) begin
for (int j = 0; j < N**2; j++) $write("%2d ", X[i][j]);
$display("");
end
$display("");
endfunction : to_string
// Random table constraints
constraint con_rtab {
foreach (X[i,j]) {
foreach (X[k,]) // Unique colums
if (i < k) X[i][j] != X[k][j];
foreach (X[,m])// Unique rows
if (j<m) X[i][j] !=X[i][m];
X[i][j] inside {[1:N**2]};// All entries between 1 and N^2
foreach (box[x]) // Unique NxN
foreach (box[y])
X[i][j] != X[i-i%N+(i+x+1)%N][j-j%N+(j+y+1)%N];
}
}
endclass: Sudoku
program sudoku1;
Sudoku obj;
initial
begin
obj=new();
repeat(5) begin
void'(obj.randomize());
obj.to_string();
end
$finish(2);
end
endprogram
SystemVerilog制約ソルバで、N-クイーンを解く(Solve N-ｑueens by using systemverilog
constraint solver)
program N_queens;
parameter SIZE_LOG2 = 3;
parameter SIZE = 1 << SIZE_LOG2;
`define ABS_DIFF(a,b) (a>b?a-b:b-a)
class board; rand bit [SIZE_LOG2-1:0] row[SIZE];
constraint equations {
foreach (row[i])
foreach (row[j])
if (i < j)
row[i] != row[j];
foreach (row[i])
foreach (row[j])
if (i < j)
`ABS_DIFF(row[i], row[j]) != `ABS_DIFF(i,j);
}
function void to_string();
foreach (row[i])
begin
automatic bit [SIZE-1:0] x = 1 << row[i];
$display( " %b", x );
end
$display("--");
endfunction
endclass
board b = new;
initial
repeat(5) begin
b.randomize();
b.to_string();
end
endprogram
***** Veritak SV32 Engine Version 449 Build Aug 1 2013***** 00001000 00100000 10000000 00000100 00000001 01000000 00010000 00000010 -- 00001000 00000010 10000000 00010000 01000000 00000001 00000100 00100000 -- 00001000 01000000 00010000 00000100 00000001 00100000 10000000 00000010 -- 00000100 01000000 00000010 10000000 00100000 00001000 00000001 00010000 -- 00001000 00000010 01000000 00010000 00000001 10000000 00100000 00000100 -- ---------- シミュレーションを終了します。time=0ns
こちらも8x8までならBDDソルバで解けるのですが、それより大きいと解けませんでした。元のソースは、こちらです。
そこで、こちらもSATソルバで解いてみました。256x256までは、解けています。そのときのCNFは、476万節でした。こちらも専用ソルバに比較すれば見劣りする結果ではあります。確かに、最高難度の問題を解こうとすれば、専用ソルバには及びません。が、制約プログラミングの要は、簡易な記述にあります。その道の専門家でないと、最適な問題解法のアルゴリズム開発は難しいでしょう。制約プログラミングを用いれば、解法のアルゴリズム開発は必要ありません。必要なものは、制約を宣言の形で記述するだけでよいのです。多くの場合、最高難度の問題を最高速度で解く専用ソルバは必要なく、簡易な制約プログラミングで済むでしょう。
シミュレータの実装
SVのrandomize()は、SystemCと比べても格段に高機能です。より高い機能を使うとより速度が落ちてしまう傾向にあります。特に小規模なシミュレーションの場合、相対的に影響が顕著になります。シミュレータの実装は、ブラックボックスですが、使われているアルゴリズムを理解することで、遅い理由が想像できるのではないかと思います。
ランダム生成のアルゴリズム評価
シミュレータの実装依存になります。こちらの評価を参考にして選定しました。よい乱数、悪い乱数も参考にしました。シミュレータの場合、多数のランダム状態を維持しなければならない関係で、品質が良いメルセンヌツイスタの実装は、見送りました。
Uniform Distributionのアルゴリズム
一般に、BDD上で、入力を均一にランダム化しても、出力空間上では、均一分布にはなりません。また、BDD上のオーダも出現に影響するので、各BDDノード上で、Then/Else
に対する遷移確率を補正してやる必要があります。
randcの実装
制約のある場合：
コンパイル時に、制約のBDD表現を求めます。BDD空間にあるものが、制約を満たす全ての解の集合です。つまり、制約を満たす解は、知ろうと思えば全てこの時に分かります。ただし、一つ一つの解は、randomize()コール時に得ます。randomize()コールの度、生成した値（ランダムに選んだBDDノードs)を除去し、次回に出現しないようにします。（重複の除去） この作業は、一回り（すべての候補が出尽すまで）するまで行われます。つまり一回りするまで、BDD演算が入ることになります。BDD演算は、基本的にビット単位ですので、重いのです。（遅いです） 一回りした後は、制約のない場合と同じです。
制約のない場合：
生成した全ての値を覚えておいて、その全ての順列を求めます。std::next_permutation()をそのまま使っています。
実装の参考にした文献リスト
LRM2012
システムLSI設計自動化技術の基礎
CUDD: CU Decision Diagram Package
Constraint-Based Verification
http://www-alg.ist.hokudai.ac.jp/~minato/alg2006/alg2006-4.pdf
http://www-alg.ist.hokudai.ac.jp/~minato/alg2006/alg2006-5.pdf
http://www-alg.ist.hokudai.ac.jp/~minato/alg2006/alg2006-6.pdf
http://www-alg.ist.hokudai.ac.jp/~minato/alg2006/alg2006-7.pdf
http://www.nurse-scheduling-software.com/index.html
