diff options
Diffstat (limited to 'tests')
66 files changed, 2399 insertions, 99 deletions
diff --git a/tests/arch/fabulous/.gitignore b/tests/arch/fabulous/.gitignore new file mode 100644 index 000000000..9a71dca69 --- /dev/null +++ b/tests/arch/fabulous/.gitignore @@ -0,0 +1,4 @@ +*.log +/run-test.mk ++*_synth.v ++*_testbench diff --git a/tests/arch/fabulous/complexflop.ys b/tests/arch/fabulous/complexflop.ys new file mode 100644 index 000000000..13f4522b9 --- /dev/null +++ b/tests/arch/fabulous/complexflop.ys @@ -0,0 +1,37 @@ +read_verilog <<EOT +module top ( input d0, d1, d2, d3, ce, sr, clk, output reg q0, q1, q2, q3 ); + always @(posedge clk) + begin + if (sr) begin + q0 <= 1'b0; + q1 <= 1'b1; + end else begin + q0 <= d0; + q1 <= d1; + end + if (ce) begin + if (sr) begin + q2 <= 1'b0; + q3 <= 1'b1; + end else begin + q2 <= d2; + q3 <= d3; + end + end + end +endmodule +EOT + +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/fabulous/prims.v synth_fabulous -complex-dff # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 1 t:LUTFF_SR +select -assert-count 1 t:LUTFF_SS +select -assert-count 1 t:LUTFF_ESR +select -assert-count 1 t:LUTFF_ESS + +select -assert-none t:LUTFF_SR t:LUTFF_SS t:LUTFF_ESR t:LUTFF_ESS %% t:* %D diff --git a/tests/arch/fabulous/counter.ys b/tests/arch/fabulous/counter.ys new file mode 100644 index 000000000..d79b378a6 --- /dev/null +++ b/tests/arch/fabulous/counter.ys @@ -0,0 +1,26 @@ +read_verilog <<EOT +module top ( out, clk, reset ); + output [7:0] out; + input clk, reset; + reg [7:0] out; + + always @(posedge clk) + if (reset) + out <= 8'b0; + else + out <= out + 1; +endmodule +EOT + +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/fabulous/prims.v synth_fabulous # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 1 t:LUT2 +select -assert-count 7 t:LUT3 +select -assert-count 4 t:LUT4 +select -assert-count 8 t:LUTFF +select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUTFF %% t:* %D diff --git a/tests/arch/fabulous/custom_map.v b/tests/arch/fabulous/custom_map.v new file mode 100644 index 000000000..1538e837b --- /dev/null +++ b/tests/arch/fabulous/custom_map.v @@ -0,0 +1,3 @@ +module AND(input [7:0] A, B, output [7:0] Y); + ALU #(.MODE("AND")) _TECHMAP_REPLACE_ (.A(A), .B(B), .Y(Y)); +endmodule diff --git a/tests/arch/fabulous/custom_prims.v b/tests/arch/fabulous/custom_prims.v new file mode 100644 index 000000000..4989188e2 --- /dev/null +++ b/tests/arch/fabulous/custom_prims.v @@ -0,0 +1,8 @@ +(* blackbox *) +module AND(input [7:0] A, B, output [7:0] Y); +endmodule + +(* blackbox *) +module ALU(input [7:0] A, B, output [7:0] Y); +parameter MODE = ""; +endmodule diff --git a/tests/arch/fabulous/customisation.ys b/tests/arch/fabulous/customisation.ys new file mode 100644 index 000000000..0e78d2e56 --- /dev/null +++ b/tests/arch/fabulous/customisation.ys @@ -0,0 +1,10 @@ +read_verilog <<EOT +module prim_test(input [7:0] a, b, output [7:0] q); + AND and_i (.A(a), .B(b), .Y(q)); +endmodule +EOT + +# Test adding custom primitives and techmap rules +synth_fabulous -top prim_test -extra-plib custom_prims.v -extra-map custom_map.v +cd prim_test +select -assert-count 1 t:ALU diff --git a/tests/arch/fabulous/fsm.ys b/tests/arch/fabulous/fsm.ys new file mode 100644 index 000000000..9c3831682 --- /dev/null +++ b/tests/arch/fabulous/fsm.ys @@ -0,0 +1,19 @@ +read_verilog ../common/fsm.v +hierarchy -top fsm +proc +flatten + +equiv_opt -run :prove -map +/fabulous/prims.v synth_fabulous +async2sync +miter -equiv -make_assert -flatten gold gate miter +stat +sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter + +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd fsm # Constrain all select calls below inside the top module + +select -assert-count 6 t:LUTFF +select -assert-max 4 t:LUT2 +select -assert-max 2 t:LUT3 +select -assert-max 9 t:LUT4 +select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUTFF %% t:* %D diff --git a/tests/arch/fabulous/logic.ys b/tests/arch/fabulous/logic.ys new file mode 100644 index 000000000..730d9ab54 --- /dev/null +++ b/tests/arch/fabulous/logic.ys @@ -0,0 +1,10 @@ +read_verilog ../common/logic.v +hierarchy -top top +proc +equiv_opt -assert -map +/fabulous/prims.v synth_fabulous # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-max 1 t:LUT1 +select -assert-max 6 t:LUT2 +select -assert-max 2 t:LUT4 +select -assert-none t:LUT1 t:LUT2 t:LUT4 %% t:* %D diff --git a/tests/arch/fabulous/regfile.ys b/tests/arch/fabulous/regfile.ys new file mode 100644 index 000000000..8d1eedef0 --- /dev/null +++ b/tests/arch/fabulous/regfile.ys @@ -0,0 +1,33 @@ +read_verilog <<EOT +module sync_sync(input clk, we, input [4:0] aw, aa, ab, input [3:0] wd, output reg [3:0] ra, rb); + reg [3:0] mem[0:31]; + always @(posedge clk) + if (we) mem[aw] <= wd; + always @(posedge clk) + ra <= mem[aa]; + always @(posedge clk) + rb <= mem[ab]; +endmodule +EOT + +synth_fabulous -top sync_sync +cd sync_sync +select -assert-count 1 t:RegFile_32x4 + +design -reset + +read_verilog <<EOT +module async_sync(input clk, we, input [4:0] aw, aa, ab, input [3:0] wd, output reg [3:0] ra, rb); + reg [3:0] mem[0:31]; + always @(posedge clk) + if (we) mem[aw] <= wd; + always @(posedge clk) + ra <= mem[aa]; + always @(*) + rb <= mem[ab]; +endmodule +EOT + +synth_fabulous -top async_sync +cd async_sync +select -assert-count 1 t:RegFile_32x4 diff --git a/tests/arch/fabulous/tribuf.ys b/tests/arch/fabulous/tribuf.ys new file mode 100644 index 000000000..0dcf1cbab --- /dev/null +++ b/tests/arch/fabulous/tribuf.ys @@ -0,0 +1,12 @@ +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +tribuf +flatten +synth +equiv_opt -assert -map +/fabulous/prims.v -map +/simcells.v synth_fabulous -iopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd tristate # Constrain all select calls below inside the top module +select -assert-count 3 t:IO_1_bidirectional_frame_config_pass +select -assert-max 1 t:LUT1 +select -assert-none t:IO_1_bidirectional_frame_config_pass t:LUT1 %% t:* %D diff --git a/tests/arch/gatemate/gen_luttrees.py b/tests/arch/gatemate/gen_luttrees.py new file mode 100644 index 000000000..27d2225a2 --- /dev/null +++ b/tests/arch/gatemate/gen_luttrees.py @@ -0,0 +1,48 @@ +from random import Random + +def main(): + r = Random(1) + + N = 750 + with open("tests/arch/gatemate/luttrees.v", "w") as v: + print(f"module luttrees(input [{N-1}:0] a, b, c, d, e, output [{N-1}:0] q);", file=v) + for i in range(N): + def f(): + return r.choice(["&", "|", "^"]) + + def a(x): + return f"({r.choice(['', '!'])}{x}[{i}])" + + # Bias towards testing bigger functions + k = r.choice([2, 3, 4, 4, 4, 5, 5, 5]) + if k == 2: + expr = f"{a('a')}{f()}{a('b')}" + elif k == 3: + expr = f"({a('a')}{f()}{a('b')}){f()}{a('c')}" + elif k == 4: + # Two types of 4-input function + if r.choice([False, True]): + expr = f"(({a('a')}{f()}{a('b')}){f()}{a('c')}){f()}{a('d')}" + else: + expr = f"({a('a')}{f()}{a('b')}){f()}({a('c')}{f()}{a('d')})" + elif k == 5: + expr = f"(({a('a')}{f()}{a('b')}){f()}({a('c')}{f()}{a('d')})){f()}{a('e')}" + print(f" assign q[{i}] = {expr};", file=v) + print("endmodule", file=v) + with open("tests/arch/gatemate/luttrees.ys", "w") as s: + print(f""" +read_verilog luttrees.v +design -save read + +hierarchy -top luttrees +proc +equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -nomx4 -nomx8 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd luttrees # Constrain all select calls below inside the top module + +select -assert-count {N} t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %% +select -assert-none t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %% t:* %D +""", file=s) + +if __name__ == '__main__': + main() diff --git a/tests/arch/gatemate/luttrees.v b/tests/arch/gatemate/luttrees.v new file mode 100644 index 000000000..7fc02916d --- /dev/null +++ b/tests/arch/gatemate/luttrees.v @@ -0,0 +1,752 @@ +module luttrees(input [749:0] a, b, c, d, e, output [749:0] q); + assign q[0] = ((!a[0])&(!b[0]))|((!c[0])^(!d[0])); + assign q[1] = ((!a[1])&(!b[1]))|((c[1])^(!d[1])); + assign q[2] = ((a[2])|(b[2]))&((c[2])^(d[2])); + assign q[3] = (((a[3])|(b[3]))^((c[3])|(!d[3])))^(e[3]); + assign q[4] = (((a[4])^(b[4]))|((!c[4])&(!d[4])))^(e[4]); + assign q[5] = (((a[5])^(!b[5]))^(!c[5]))^(d[5]); + assign q[6] = (((!a[6])^(!b[6]))^(c[6]))|(d[6]); + assign q[7] = (((!a[7])^(b[7]))|((!c[7])&(!d[7])))^(e[7]); + assign q[8] = (((!a[8])|(b[8]))|(c[8]))|(!d[8]); + assign q[9] = ((a[9])&(b[9]))^((c[9])|(!d[9])); + assign q[10] = (((!a[10])|(b[10]))|((c[10])^(d[10])))|(e[10]); + assign q[11] = (((!a[11])^(b[11]))^((!c[11])|(!d[11])))|(!e[11]); + assign q[12] = (!a[12])|(b[12]); + assign q[13] = ((a[13])&(!b[13]))&((c[13])&(d[13])); + assign q[14] = (((a[14])|(b[14]))|((c[14])^(d[14])))|(!e[14]); + assign q[15] = ((a[15])&(!b[15]))^(c[15]); + assign q[16] = (((!a[16])^(!b[16]))|(!c[16]))&(d[16]); + assign q[17] = (((!a[17])|(b[17]))|(c[17]))|(d[17]); + assign q[18] = (((a[18])&(b[18]))|((c[18])&(d[18])))|(!e[18]); + assign q[19] = (((a[19])^(b[19]))|(!c[19]))^(!d[19]); + assign q[20] = (!a[20])&(b[20]); + assign q[21] = (!a[21])&(b[21]); + assign q[22] = (((a[22])|(!b[22]))&(c[22]))^(d[22]); + assign q[23] = (((a[23])^(b[23]))|(c[23]))|(d[23]); + assign q[24] = (((a[24])|(b[24]))^(!c[24]))|(!d[24]); + assign q[25] = (!a[25])^(!b[25]); + assign q[26] = ((a[26])&(!b[26]))^((c[26])|(!d[26])); + assign q[27] = (((a[27])|(!b[27]))^(!c[27]))^(d[27]); + assign q[28] = ((a[28])&(b[28]))&(c[28]); + assign q[29] = (((!a[29])^(!b[29]))|(!c[29]))|(d[29]); + assign q[30] = ((!a[30])&(b[30]))|((c[30])|(d[30])); + assign q[31] = (((a[31])&(!b[31]))&((!c[31])&(d[31])))^(e[31]); + assign q[32] = (((!a[32])^(b[32]))|(!c[32]))&(d[32]); + assign q[33] = ((a[33])&(!b[33]))&((c[33])&(d[33])); + assign q[34] = (((a[34])&(!b[34]))&((c[34])&(d[34])))|(!e[34]); + assign q[35] = (((!a[35])|(b[35]))&(!c[35]))&(d[35]); + assign q[36] = (!a[36])^(!b[36]); + assign q[37] = (((!a[37])|(!b[37]))&((c[37])|(!d[37])))&(!e[37]); + assign q[38] = (((!a[38])|(b[38]))^(c[38]))|(d[38]); + assign q[39] = (((a[39])|(b[39]))|(c[39]))^(!d[39]); + assign q[40] = (((!a[40])&(!b[40]))&(!c[40]))^(!d[40]); + assign q[41] = (((a[41])^(b[41]))&(c[41]))&(d[41]); + assign q[42] = (((a[42])|(b[42]))^((c[42])&(d[42])))|(!e[42]); + assign q[43] = (((!a[43])&(b[43]))^((!c[43])&(d[43])))&(e[43]); + assign q[44] = (((!a[44])&(!b[44]))&(c[44]))&(d[44]); + assign q[45] = (((a[45])&(!b[45]))|((c[45])&(d[45])))|(e[45]); + assign q[46] = (((!a[46])^(!b[46]))^((!c[46])^(!d[46])))&(!e[46]); + assign q[47] = (((a[47])|(!b[47]))&((!c[47])^(d[47])))&(!e[47]); + assign q[48] = ((a[48])|(!b[48]))|((!c[48])&(d[48])); + assign q[49] = (((a[49])&(!b[49]))^(!c[49]))^(d[49]); + assign q[50] = (((!a[50])^(!b[50]))&(!c[50]))|(!d[50]); + assign q[51] = ((a[51])^(!b[51]))&((c[51])|(!d[51])); + assign q[52] = (((a[52])^(!b[52]))^(c[52]))&(!d[52]); + assign q[53] = ((!a[53])|(b[53]))^((c[53])|(!d[53])); + assign q[54] = (((!a[54])^(b[54]))^((c[54])^(d[54])))|(e[54]); + assign q[55] = ((a[55])^(b[55]))|((c[55])|(!d[55])); + assign q[56] = (((a[56])|(!b[56]))&((!c[56])&(d[56])))|(!e[56]); + assign q[57] = ((!a[57])|(b[57]))|(c[57]); + assign q[58] = (((a[58])&(b[58]))|(c[58]))&(!d[58]); + assign q[59] = ((!a[59])|(!b[59]))^((!c[59])&(!d[59])); + assign q[60] = (((!a[60])&(b[60]))^((!c[60])&(!d[60])))&(e[60]); + assign q[61] = ((a[61])^(!b[61]))^(c[61]); + assign q[62] = ((!a[62])^(!b[62]))|(!c[62]); + assign q[63] = (((a[63])&(!b[63]))^((!c[63])|(!d[63])))^(!e[63]); + assign q[64] = (((!a[64])&(!b[64]))|((c[64])^(d[64])))|(e[64]); + assign q[65] = (((!a[65])^(!b[65]))^((c[65])|(d[65])))|(e[65]); + assign q[66] = (((!a[66])|(!b[66]))^((c[66])|(d[66])))^(!e[66]); + assign q[67] = (!a[67])^(b[67]); + assign q[68] = (((!a[68])&(b[68]))^((c[68])|(!d[68])))^(!e[68]); + assign q[69] = ((!a[69])|(!b[69]))&((!c[69])^(d[69])); + assign q[70] = ((!a[70])&(!b[70]))&((!c[70])&(d[70])); + assign q[71] = ((!a[71])^(!b[71]))^((!c[71])&(d[71])); + assign q[72] = (((!a[72])&(b[72]))^(!c[72]))|(d[72]); + assign q[73] = (((!a[73])|(b[73]))|(!c[73]))&(!d[73]); + assign q[74] = (((a[74])|(b[74]))^(c[74]))^(!d[74]); + assign q[75] = (((!a[75])&(!b[75]))&((c[75])^(d[75])))^(!e[75]); + assign q[76] = (((!a[76])^(b[76]))&(c[76]))^(!d[76]); + assign q[77] = (((!a[77])|(b[77]))&((c[77])^(!d[77])))&(e[77]); + assign q[78] = (((!a[78])|(b[78]))&(c[78]))&(d[78]); + assign q[79] = ((!a[79])^(!b[79]))|((!c[79])&(d[79])); + assign q[80] = ((a[80])|(b[80]))|(!c[80]); + assign q[81] = (((a[81])&(b[81]))|((!c[81])^(!d[81])))&(!e[81]); + assign q[82] = (((!a[82])^(b[82]))&(c[82]))&(d[82]); + assign q[83] = (!a[83])|(!b[83]); + assign q[84] = ((!a[84])&(b[84]))&((c[84])|(d[84])); + assign q[85] = (!a[85])|(b[85]); + assign q[86] = ((!a[86])^(!b[86]))&(c[86]); + assign q[87] = (a[87])&(!b[87]); + assign q[88] = ((!a[88])&(b[88]))&(!c[88]); + assign q[89] = (((a[89])^(!b[89]))|(!c[89]))^(!d[89]); + assign q[90] = ((a[90])&(b[90]))|((!c[90])^(d[90])); + assign q[91] = (((!a[91])^(b[91]))^((!c[91])^(d[91])))^(!e[91]); + assign q[92] = ((!a[92])&(b[92]))&(c[92]); + assign q[93] = (((a[93])&(b[93]))^(!c[93]))^(!d[93]); + assign q[94] = ((!a[94])&(b[94]))^(c[94]); + assign q[95] = (((a[95])|(!b[95]))&((!c[95])&(!d[95])))|(e[95]); + assign q[96] = ((!a[96])&(!b[96]))|((c[96])|(!d[96])); + assign q[97] = ((!a[97])&(!b[97]))&(c[97]); + assign q[98] = (((!a[98])^(!b[98]))^((!c[98])&(d[98])))^(!e[98]); + assign q[99] = (!a[99])^(b[99]); + assign q[100] = (((!a[100])^(!b[100]))&(!c[100]))|(d[100]); + assign q[101] = ((a[101])|(!b[101]))|(!c[101]); + assign q[102] = (((!a[102])|(!b[102]))^((c[102])^(d[102])))&(!e[102]); + assign q[103] = (((!a[103])^(b[103]))|((!c[103])|(!d[103])))|(!e[103]); + assign q[104] = ((a[104])&(b[104]))^(!c[104]); + assign q[105] = ((!a[105])|(!b[105]))|((!c[105])|(!d[105])); + assign q[106] = ((a[106])|(b[106]))^((c[106])&(d[106])); + assign q[107] = (((a[107])&(!b[107]))^((c[107])&(!d[107])))&(e[107]); + assign q[108] = ((a[108])^(b[108]))^(!c[108]); + assign q[109] = (!a[109])|(!b[109]); + assign q[110] = ((!a[110])&(!b[110]))|((!c[110])^(d[110])); + assign q[111] = (((a[111])|(!b[111]))&((c[111])^(!d[111])))^(!e[111]); + assign q[112] = ((!a[112])^(!b[112]))&(!c[112]); + assign q[113] = (((a[113])&(!b[113]))^((c[113])^(d[113])))|(!e[113]); + assign q[114] = (((!a[114])^(!b[114]))|(!c[114]))&(!d[114]); + assign q[115] = ((!a[115])^(b[115]))|((c[115])|(!d[115])); + assign q[116] = (((!a[116])^(b[116]))&((c[116])&(!d[116])))|(!e[116]); + assign q[117] = (((!a[117])|(!b[117]))|(c[117]))|(!d[117]); + assign q[118] = (((a[118])&(b[118]))|(!c[118]))&(!d[118]); + assign q[119] = (((!a[119])^(!b[119]))^((!c[119])^(!d[119])))|(!e[119]); + assign q[120] = (((a[120])^(!b[120]))|((!c[120])&(d[120])))&(e[120]); + assign q[121] = ((a[121])&(!b[121]))&((!c[121])&(!d[121])); + assign q[122] = ((a[122])|(b[122]))^((c[122])^(!d[122])); + assign q[123] = (((a[123])^(b[123]))^((!c[123])^(d[123])))|(!e[123]); + assign q[124] = (((a[124])&(b[124]))|(c[124]))^(!d[124]); + assign q[125] = (((!a[125])&(!b[125]))&(c[125]))|(d[125]); + assign q[126] = (((!a[126])^(!b[126]))|(c[126]))^(!d[126]); + assign q[127] = (((a[127])&(!b[127]))^((!c[127])&(!d[127])))|(e[127]); + assign q[128] = (((!a[128])^(b[128]))|(c[128]))&(!d[128]); + assign q[129] = (((a[129])^(b[129]))|(!c[129]))|(!d[129]); + assign q[130] = (((!a[130])&(!b[130]))|(!c[130]))&(!d[130]); + assign q[131] = ((!a[131])^(b[131]))&((!c[131])^(d[131])); + assign q[132] = (((!a[132])|(!b[132]))&(c[132]))&(!d[132]); + assign q[133] = ((a[133])^(b[133]))^((c[133])&(d[133])); + assign q[134] = (((!a[134])&(b[134]))|(c[134]))&(d[134]); + assign q[135] = (((!a[135])^(!b[135]))&(c[135]))|(!d[135]); + assign q[136] = ((!a[136])&(b[136]))|((c[136])&(d[136])); + assign q[137] = (((a[137])|(b[137]))|(c[137]))&(d[137]); + assign q[138] = (((!a[138])^(b[138]))&((!c[138])|(d[138])))^(!e[138]); + assign q[139] = ((!a[139])^(b[139]))^(!c[139]); + assign q[140] = (((a[140])^(!b[140]))^((!c[140])^(!d[140])))|(e[140]); + assign q[141] = ((a[141])^(b[141]))&((c[141])&(!d[141])); + assign q[142] = ((!a[142])^(!b[142]))^((!c[142])|(d[142])); + assign q[143] = (((a[143])^(!b[143]))&((!c[143])^(d[143])))^(!e[143]); + assign q[144] = (((a[144])&(b[144]))^((c[144])^(d[144])))|(!e[144]); + assign q[145] = (((!a[145])&(b[145]))|((!c[145])|(d[145])))^(e[145]); + assign q[146] = (((a[146])^(b[146]))^(c[146]))|(d[146]); + assign q[147] = (((a[147])|(!b[147]))|((!c[147])|(!d[147])))^(!e[147]); + assign q[148] = (a[148])|(b[148]); + assign q[149] = (a[149])&(b[149]); + assign q[150] = (((!a[150])^(!b[150]))|((c[150])^(d[150])))&(!e[150]); + assign q[151] = ((a[151])^(!b[151]))|((!c[151])|(d[151])); + assign q[152] = (((!a[152])|(!b[152]))|((!c[152])|(d[152])))^(e[152]); + assign q[153] = (!a[153])^(b[153]); + assign q[154] = (((!a[154])^(b[154]))^(c[154]))|(d[154]); + assign q[155] = (((a[155])|(b[155]))&((c[155])|(!d[155])))^(e[155]); + assign q[156] = (((!a[156])|(!b[156]))^((c[156])|(!d[156])))|(e[156]); + assign q[157] = (((!a[157])&(b[157]))&((!c[157])|(d[157])))&(e[157]); + assign q[158] = (((!a[158])^(!b[158]))&(c[158]))^(d[158]); + assign q[159] = ((!a[159])|(b[159]))^((!c[159])&(d[159])); + assign q[160] = (((a[160])^(b[160]))|((c[160])&(d[160])))&(!e[160]); + assign q[161] = (a[161])|(b[161]); + assign q[162] = (a[162])^(b[162]); + assign q[163] = (((!a[163])&(b[163]))|(c[163]))^(d[163]); + assign q[164] = (((a[164])^(b[164]))&((c[164])|(!d[164])))|(!e[164]); + assign q[165] = ((!a[165])^(!b[165]))^((!c[165])^(d[165])); + assign q[166] = (((!a[166])&(!b[166]))|((!c[166])&(!d[166])))^(!e[166]); + assign q[167] = ((!a[167])|(b[167]))|((!c[167])|(!d[167])); + assign q[168] = (((!a[168])^(!b[168]))&((c[168])&(!d[168])))&(e[168]); + assign q[169] = ((a[169])^(!b[169]))^(c[169]); + assign q[170] = (((!a[170])^(b[170]))&(c[170]))&(d[170]); + assign q[171] = (!a[171])|(!b[171]); + assign q[172] = ((a[172])&(!b[172]))&((!c[172])&(!d[172])); + assign q[173] = (((a[173])&(!b[173]))^((c[173])|(!d[173])))^(!e[173]); + assign q[174] = ((!a[174])&(!b[174]))&(!c[174]); + assign q[175] = ((!a[175])|(!b[175]))^(c[175]); + assign q[176] = (!a[176])&(b[176]); + assign q[177] = ((a[177])|(b[177]))^(c[177]); + assign q[178] = (((a[178])^(b[178]))|((c[178])^(!d[178])))^(e[178]); + assign q[179] = ((a[179])^(!b[179]))^(!c[179]); + assign q[180] = (((a[180])^(b[180]))^(c[180]))|(!d[180]); + assign q[181] = (((!a[181])|(!b[181]))&((c[181])&(d[181])))|(e[181]); + assign q[182] = (((a[182])|(!b[182]))&((c[182])&(d[182])))|(!e[182]); + assign q[183] = ((a[183])^(!b[183]))^((!c[183])&(d[183])); + assign q[184] = (((a[184])|(b[184]))|((c[184])^(d[184])))&(!e[184]); + assign q[185] = (((a[185])^(b[185]))^((!c[185])&(!d[185])))^(!e[185]); + assign q[186] = (((!a[186])|(!b[186]))&((!c[186])&(!d[186])))|(!e[186]); + assign q[187] = (((a[187])^(!b[187]))|(!c[187]))^(d[187]); + assign q[188] = ((a[188])^(b[188]))&(!c[188]); + assign q[189] = (((!a[189])^(b[189]))^((!c[189])^(d[189])))|(e[189]); + assign q[190] = (((!a[190])^(b[190]))&((!c[190])|(d[190])))&(e[190]); + assign q[191] = ((!a[191])|(!b[191]))|(!c[191]); + assign q[192] = (((a[192])^(b[192]))^(c[192]))|(!d[192]); + assign q[193] = ((a[193])^(b[193]))|((!c[193])&(d[193])); + assign q[194] = (((a[194])&(b[194]))|(!c[194]))&(!d[194]); + assign q[195] = ((!a[195])|(!b[195]))^((c[195])&(!d[195])); + assign q[196] = (((a[196])&(!b[196]))|((c[196])^(d[196])))^(!e[196]); + assign q[197] = ((a[197])&(b[197]))^((c[197])^(!d[197])); + assign q[198] = (((a[198])&(!b[198]))|((!c[198])^(!d[198])))&(e[198]); + assign q[199] = (!a[199])&(b[199]); + assign q[200] = ((a[200])&(b[200]))^((c[200])&(d[200])); + assign q[201] = (((!a[201])&(!b[201]))^(!c[201]))|(!d[201]); + assign q[202] = ((a[202])^(b[202]))&(!c[202]); + assign q[203] = (((!a[203])|(b[203]))|((c[203])&(!d[203])))^(!e[203]); + assign q[204] = (((a[204])^(!b[204]))&((!c[204])^(!d[204])))^(!e[204]); + assign q[205] = (((a[205])|(!b[205]))^((!c[205])^(!d[205])))|(!e[205]); + assign q[206] = (a[206])|(!b[206]); + assign q[207] = (((a[207])^(!b[207]))&((!c[207])|(d[207])))|(!e[207]); + assign q[208] = (a[208])|(b[208]); + assign q[209] = ((!a[209])|(b[209]))|((!c[209])|(d[209])); + assign q[210] = ((!a[210])&(b[210]))&((!c[210])|(!d[210])); + assign q[211] = ((a[211])^(!b[211]))|((!c[211])|(!d[211])); + assign q[212] = (((a[212])&(!b[212]))&((c[212])^(d[212])))^(e[212]); + assign q[213] = (((!a[213])&(b[213]))^(!c[213]))^(!d[213]); + assign q[214] = (!a[214])|(!b[214]); + assign q[215] = ((a[215])|(!b[215]))^((!c[215])^(!d[215])); + assign q[216] = (((a[216])^(!b[216]))^((!c[216])|(d[216])))|(e[216]); + assign q[217] = (((a[217])^(b[217]))^((!c[217])|(!d[217])))&(e[217]); + assign q[218] = ((a[218])&(!b[218]))&(c[218]); + assign q[219] = ((a[219])|(b[219]))&((c[219])&(d[219])); + assign q[220] = (((!a[220])&(b[220]))^((c[220])|(d[220])))|(!e[220]); + assign q[221] = ((a[221])&(!b[221]))&((c[221])^(!d[221])); + assign q[222] = (!a[222])|(!b[222]); + assign q[223] = ((a[223])^(b[223]))^(c[223]); + assign q[224] = ((a[224])&(!b[224]))&((c[224])|(d[224])); + assign q[225] = ((!a[225])&(b[225]))&(!c[225]); + assign q[226] = (((a[226])^(b[226]))|((c[226])&(d[226])))&(e[226]); + assign q[227] = ((a[227])&(b[227]))|((!c[227])^(!d[227])); + assign q[228] = ((!a[228])&(!b[228]))|((!c[228])|(!d[228])); + assign q[229] = (((a[229])|(b[229]))|((!c[229])&(d[229])))&(e[229]); + assign q[230] = (((!a[230])^(!b[230]))|((!c[230])|(!d[230])))|(!e[230]); + assign q[231] = (((!a[231])|(b[231]))|((c[231])|(d[231])))|(e[231]); + assign q[232] = ((!a[232])^(b[232]))&((c[232])&(!d[232])); + assign q[233] = (((!a[233])&(!b[233]))|(!c[233]))&(!d[233]); + assign q[234] = (((!a[234])&(b[234]))^(!c[234]))&(d[234]); + assign q[235] = (((a[235])&(b[235]))^((!c[235])^(!d[235])))^(!e[235]); + assign q[236] = (((!a[236])^(b[236]))&((!c[236])&(!d[236])))^(e[236]); + assign q[237] = (a[237])|(!b[237]); + assign q[238] = (((a[238])|(b[238]))&((!c[238])^(d[238])))&(e[238]); + assign q[239] = ((!a[239])^(!b[239]))&((c[239])&(d[239])); + assign q[240] = (((!a[240])^(!b[240]))&(!c[240]))&(!d[240]); + assign q[241] = ((!a[241])&(b[241]))&(c[241]); + assign q[242] = ((a[242])|(!b[242]))&((c[242])|(d[242])); + assign q[243] = ((a[243])|(b[243]))^((!c[243])&(d[243])); + assign q[244] = (((!a[244])^(b[244]))&(!c[244]))|(!d[244]); + assign q[245] = (((a[245])^(!b[245]))^(!c[245]))^(!d[245]); + assign q[246] = ((!a[246])|(!b[246]))&(!c[246]); + assign q[247] = ((!a[247])&(b[247]))|(c[247]); + assign q[248] = (((!a[248])|(!b[248]))|((!c[248])&(!d[248])))&(!e[248]); + assign q[249] = (a[249])|(!b[249]); + assign q[250] = (((!a[250])^(!b[250]))^(!c[250]))^(!d[250]); + assign q[251] = (((a[251])|(b[251]))|(!c[251]))^(d[251]); + assign q[252] = (((!a[252])&(!b[252]))^((c[252])&(d[252])))&(e[252]); + assign q[253] = (!a[253])^(!b[253]); + assign q[254] = (((a[254])^(!b[254]))|((c[254])|(!d[254])))&(!e[254]); + assign q[255] = (!a[255])|(!b[255]); + assign q[256] = (((a[256])|(!b[256]))&(c[256]))&(!d[256]); + assign q[257] = (!a[257])^(!b[257]); + assign q[258] = (((!a[258])&(b[258]))^(c[258]))|(d[258]); + assign q[259] = (((!a[259])&(!b[259]))|(c[259]))&(!d[259]); + assign q[260] = ((!a[260])&(!b[260]))|((!c[260])^(!d[260])); + assign q[261] = (((a[261])|(b[261]))^(c[261]))|(d[261]); + assign q[262] = (((!a[262])^(b[262]))^((!c[262])|(!d[262])))|(e[262]); + assign q[263] = (a[263])^(b[263]); + assign q[264] = ((!a[264])&(!b[264]))|(c[264]); + assign q[265] = (((!a[265])^(b[265]))^((c[265])^(!d[265])))|(!e[265]); + assign q[266] = (((a[266])^(!b[266]))&(c[266]))^(d[266]); + assign q[267] = ((a[267])|(!b[267]))|(!c[267]); + assign q[268] = ((!a[268])&(!b[268]))|(!c[268]); + assign q[269] = (((!a[269])^(b[269]))&((!c[269])^(!d[269])))^(!e[269]); + assign q[270] = (((a[270])|(b[270]))^(c[270]))&(d[270]); + assign q[271] = (((a[271])&(b[271]))|((c[271])|(d[271])))|(!e[271]); + assign q[272] = (((a[272])|(!b[272]))^(!c[272]))|(!d[272]); + assign q[273] = (((!a[273])|(b[273]))&((!c[273])&(!d[273])))&(!e[273]); + assign q[274] = ((a[274])^(!b[274]))|(!c[274]); + assign q[275] = (((!a[275])^(!b[275]))|((!c[275])^(!d[275])))^(e[275]); + assign q[276] = ((a[276])^(b[276]))&((!c[276])^(d[276])); + assign q[277] = (((!a[277])&(!b[277]))|((!c[277])^(!d[277])))&(!e[277]); + assign q[278] = (((!a[278])^(!b[278]))^(c[278]))&(!d[278]); + assign q[279] = (((a[279])&(b[279]))^((!c[279])|(d[279])))^(!e[279]); + assign q[280] = ((!a[280])&(!b[280]))&(!c[280]); + assign q[281] = ((a[281])|(b[281]))|((!c[281])|(!d[281])); + assign q[282] = ((a[282])&(b[282]))&((c[282])|(d[282])); + assign q[283] = (((a[283])|(!b[283]))^((c[283])&(!d[283])))&(e[283]); + assign q[284] = (((!a[284])&(b[284]))&(!c[284]))^(d[284]); + assign q[285] = (((a[285])|(!b[285]))&(!c[285]))|(d[285]); + assign q[286] = (((a[286])^(b[286]))&((c[286])^(!d[286])))&(!e[286]); + assign q[287] = ((a[287])&(!b[287]))|((c[287])|(!d[287])); + assign q[288] = ((!a[288])|(!b[288]))|((!c[288])|(!d[288])); + assign q[289] = ((a[289])&(b[289]))&((c[289])&(!d[289])); + assign q[290] = (((!a[290])^(b[290]))&((c[290])^(d[290])))&(!e[290]); + assign q[291] = (((a[291])&(!b[291]))|(!c[291]))^(d[291]); + assign q[292] = (((a[292])^(!b[292]))^((c[292])|(d[292])))&(e[292]); + assign q[293] = (((a[293])&(!b[293]))&((c[293])|(d[293])))|(e[293]); + assign q[294] = (((a[294])^(!b[294]))&((!c[294])^(d[294])))&(!e[294]); + assign q[295] = (((a[295])^(!b[295]))|((!c[295])|(d[295])))&(e[295]); + assign q[296] = (((a[296])&(!b[296]))&((c[296])&(d[296])))&(!e[296]); + assign q[297] = ((!a[297])|(b[297]))^((!c[297])^(!d[297])); + assign q[298] = (((a[298])^(b[298]))|((!c[298])|(d[298])))|(!e[298]); + assign q[299] = (((!a[299])^(b[299]))|((c[299])^(!d[299])))|(!e[299]); + assign q[300] = (((!a[300])^(!b[300]))^(!c[300]))|(d[300]); + assign q[301] = ((a[301])&(!b[301]))&((!c[301])|(!d[301])); + assign q[302] = ((a[302])^(b[302]))|((c[302])|(!d[302])); + assign q[303] = (((!a[303])&(b[303]))^((c[303])|(d[303])))|(!e[303]); + assign q[304] = (!a[304])^(b[304]); + assign q[305] = (((a[305])&(!b[305]))^((!c[305])&(!d[305])))^(!e[305]); + assign q[306] = (a[306])&(b[306]); + assign q[307] = ((a[307])&(!b[307]))&(c[307]); + assign q[308] = ((a[308])&(!b[308]))^((!c[308])|(d[308])); + assign q[309] = ((a[309])^(!b[309]))&((c[309])|(!d[309])); + assign q[310] = (((!a[310])|(b[310]))&((c[310])^(d[310])))^(!e[310]); + assign q[311] = (((!a[311])|(b[311]))&((c[311])&(d[311])))|(e[311]); + assign q[312] = (((!a[312])&(b[312]))|((c[312])^(!d[312])))&(!e[312]); + assign q[313] = (!a[313])|(!b[313]); + assign q[314] = ((a[314])^(!b[314]))^((c[314])|(!d[314])); + assign q[315] = (a[315])&(!b[315]); + assign q[316] = ((!a[316])^(!b[316]))&(!c[316]); + assign q[317] = ((a[317])&(!b[317]))^(c[317]); + assign q[318] = (((!a[318])^(!b[318]))|(!c[318]))&(!d[318]); + assign q[319] = (((a[319])&(!b[319]))|(!c[319]))^(d[319]); + assign q[320] = (((!a[320])^(!b[320]))|(c[320]))|(d[320]); + assign q[321] = ((a[321])|(!b[321]))|((c[321])|(d[321])); + assign q[322] = ((!a[322])^(!b[322]))&(!c[322]); + assign q[323] = (((!a[323])&(b[323]))|(c[323]))|(d[323]); + assign q[324] = ((!a[324])&(!b[324]))^((c[324])|(d[324])); + assign q[325] = ((a[325])&(!b[325]))|(!c[325]); + assign q[326] = ((!a[326])^(!b[326]))|(c[326]); + assign q[327] = (((a[327])|(b[327]))&((c[327])|(!d[327])))^(!e[327]); + assign q[328] = ((!a[328])|(b[328]))&((c[328])&(d[328])); + assign q[329] = (((a[329])&(b[329]))^(c[329]))|(!d[329]); + assign q[330] = ((a[330])|(b[330]))|((c[330])^(!d[330])); + assign q[331] = (((!a[331])|(b[331]))&(c[331]))&(d[331]); + assign q[332] = (((!a[332])&(b[332]))|((!c[332])^(d[332])))&(e[332]); + assign q[333] = (((a[333])^(!b[333]))|(!c[333]))|(!d[333]); + assign q[334] = ((a[334])&(!b[334]))&((c[334])&(!d[334])); + assign q[335] = (((!a[335])&(b[335]))^((c[335])&(d[335])))&(e[335]); + assign q[336] = (!a[336])^(b[336]); + assign q[337] = (((a[337])^(b[337]))&(c[337]))&(d[337]); + assign q[338] = (((a[338])^(!b[338]))&(!c[338]))&(!d[338]); + assign q[339] = (((!a[339])^(!b[339]))|((!c[339])|(d[339])))&(!e[339]); + assign q[340] = (((a[340])^(b[340]))^((c[340])^(d[340])))|(e[340]); + assign q[341] = (((!a[341])&(!b[341]))^(!c[341]))^(d[341]); + assign q[342] = (a[342])^(!b[342]); + assign q[343] = (((!a[343])^(b[343]))&((c[343])|(!d[343])))|(e[343]); + assign q[344] = ((a[344])&(b[344]))&((!c[344])&(d[344])); + assign q[345] = (((!a[345])&(b[345]))&((c[345])^(!d[345])))|(e[345]); + assign q[346] = (((a[346])^(!b[346]))&(c[346]))&(!d[346]); + assign q[347] = (((!a[347])^(!b[347]))|((c[347])|(!d[347])))|(!e[347]); + assign q[348] = (((a[348])|(b[348]))&((!c[348])&(d[348])))|(!e[348]); + assign q[349] = (!a[349])&(b[349]); + assign q[350] = (((!a[350])^(b[350]))|((c[350])|(!d[350])))&(e[350]); + assign q[351] = (((!a[351])^(!b[351]))^((c[351])|(!d[351])))&(!e[351]); + assign q[352] = ((!a[352])|(b[352]))^(c[352]); + assign q[353] = (((a[353])&(!b[353]))^((c[353])&(!d[353])))|(!e[353]); + assign q[354] = (((!a[354])^(b[354]))^((!c[354])^(d[354])))^(e[354]); + assign q[355] = (a[355])|(b[355]); + assign q[356] = (((a[356])^(!b[356]))^(!c[356]))&(!d[356]); + assign q[357] = (((a[357])&(!b[357]))^((c[357])&(!d[357])))^(e[357]); + assign q[358] = (((a[358])&(b[358]))&((!c[358])&(d[358])))|(e[358]); + assign q[359] = (((a[359])&(!b[359]))&((!c[359])^(!d[359])))&(e[359]); + assign q[360] = (((!a[360])|(!b[360]))|((!c[360])|(d[360])))&(!e[360]); + assign q[361] = (((a[361])|(b[361]))^((c[361])|(!d[361])))^(!e[361]); + assign q[362] = (((!a[362])|(!b[362]))|(c[362]))|(d[362]); + assign q[363] = ((a[363])|(!b[363]))&((!c[363])^(!d[363])); + assign q[364] = (((a[364])&(!b[364]))&((c[364])&(d[364])))|(e[364]); + assign q[365] = ((a[365])|(!b[365]))&((c[365])|(d[365])); + assign q[366] = (((a[366])|(!b[366]))&((!c[366])|(!d[366])))^(!e[366]); + assign q[367] = ((a[367])^(!b[367]))^((!c[367])|(!d[367])); + assign q[368] = (((!a[368])&(b[368]))&((!c[368])|(!d[368])))&(!e[368]); + assign q[369] = ((a[369])^(b[369]))|((c[369])|(d[369])); + assign q[370] = (((a[370])^(b[370]))^(!c[370]))|(!d[370]); + assign q[371] = (((a[371])^(b[371]))&((!c[371])&(d[371])))&(!e[371]); + assign q[372] = (((!a[372])|(!b[372]))|((!c[372])&(d[372])))&(!e[372]); + assign q[373] = ((a[373])&(b[373]))&((!c[373])&(!d[373])); + assign q[374] = (((!a[374])^(!b[374]))^((!c[374])&(!d[374])))|(e[374]); + assign q[375] = ((!a[375])&(b[375]))^(!c[375]); + assign q[376] = (!a[376])|(b[376]); + assign q[377] = (((!a[377])^(b[377]))^((!c[377])^(!d[377])))^(e[377]); + assign q[378] = (((a[378])|(!b[378]))^((c[378])^(d[378])))&(!e[378]); + assign q[379] = (((a[379])|(b[379]))&((!c[379])^(!d[379])))^(e[379]); + assign q[380] = (((!a[380])^(!b[380]))^((c[380])|(!d[380])))&(!e[380]); + assign q[381] = (((!a[381])^(b[381]))^(c[381]))^(!d[381]); + assign q[382] = (((!a[382])^(b[382]))^(!c[382]))&(!d[382]); + assign q[383] = (((!a[383])&(!b[383]))&((c[383])^(d[383])))|(e[383]); + assign q[384] = (((a[384])&(b[384]))&((c[384])&(d[384])))^(e[384]); + assign q[385] = ((a[385])|(!b[385]))&(!c[385]); + assign q[386] = ((a[386])|(b[386]))&(!c[386]); + assign q[387] = (((!a[387])^(b[387]))|(c[387]))^(d[387]); + assign q[388] = (!a[388])&(!b[388]); + assign q[389] = ((a[389])^(b[389]))^(!c[389]); + assign q[390] = (((!a[390])|(b[390]))^(c[390]))|(d[390]); + assign q[391] = (!a[391])^(!b[391]); + assign q[392] = ((!a[392])^(b[392]))|(c[392]); + assign q[393] = (((!a[393])&(!b[393]))^((c[393])^(d[393])))^(e[393]); + assign q[394] = (((!a[394])^(b[394]))|(!c[394]))|(!d[394]); + assign q[395] = ((!a[395])&(!b[395]))^(!c[395]); + assign q[396] = ((a[396])^(b[396]))|((!c[396])|(d[396])); + assign q[397] = (((a[397])|(!b[397]))&((!c[397])&(d[397])))&(!e[397]); + assign q[398] = (((a[398])&(!b[398]))^((c[398])&(d[398])))|(!e[398]); + assign q[399] = (((!a[399])^(!b[399]))^((c[399])&(d[399])))|(!e[399]); + assign q[400] = (!a[400])&(b[400]); + assign q[401] = (((a[401])&(!b[401]))^(!c[401]))^(!d[401]); + assign q[402] = ((a[402])|(!b[402]))^((!c[402])^(!d[402])); + assign q[403] = (((!a[403])|(!b[403]))|((c[403])|(d[403])))^(!e[403]); + assign q[404] = (((!a[404])^(b[404]))&((c[404])&(d[404])))^(!e[404]); + assign q[405] = (((!a[405])^(b[405]))&(!c[405]))&(d[405]); + assign q[406] = (((!a[406])|(b[406]))|((c[406])^(!d[406])))&(!e[406]); + assign q[407] = (!a[407])|(b[407]); + assign q[408] = (((!a[408])&(!b[408]))|(!c[408]))&(!d[408]); + assign q[409] = (!a[409])^(!b[409]); + assign q[410] = (((!a[410])|(b[410]))|((!c[410])|(d[410])))|(!e[410]); + assign q[411] = (((!a[411])^(b[411]))|((c[411])&(d[411])))|(e[411]); + assign q[412] = ((!a[412])&(!b[412]))&((c[412])|(d[412])); + assign q[413] = (((!a[413])^(b[413]))^((c[413])&(!d[413])))&(!e[413]); + assign q[414] = (a[414])^(!b[414]); + assign q[415] = (((!a[415])^(b[415]))&(c[415]))|(!d[415]); + assign q[416] = ((!a[416])|(!b[416]))&(c[416]); + assign q[417] = (((!a[417])^(!b[417]))^((c[417])^(d[417])))|(!e[417]); + assign q[418] = ((!a[418])&(!b[418]))^((!c[418])&(!d[418])); + assign q[419] = (!a[419])&(!b[419]); + assign q[420] = ((a[420])^(!b[420]))|(!c[420]); + assign q[421] = ((!a[421])&(!b[421]))&((!c[421])^(d[421])); + assign q[422] = ((!a[422])^(b[422]))^((!c[422])&(!d[422])); + assign q[423] = (((a[423])|(b[423]))^((c[423])&(d[423])))^(!e[423]); + assign q[424] = (a[424])|(b[424]); + assign q[425] = (!a[425])^(b[425]); + assign q[426] = (!a[426])^(!b[426]); + assign q[427] = ((a[427])&(!b[427]))^((!c[427])^(!d[427])); + assign q[428] = (((!a[428])&(!b[428]))^(!c[428]))^(d[428]); + assign q[429] = (((!a[429])^(b[429]))&(c[429]))&(d[429]); + assign q[430] = ((!a[430])&(b[430]))^((c[430])^(d[430])); + assign q[431] = (((!a[431])|(b[431]))^((!c[431])|(d[431])))&(e[431]); + assign q[432] = (((!a[432])|(!b[432]))|((!c[432])^(d[432])))|(!e[432]); + assign q[433] = (((a[433])^(!b[433]))&(!c[433]))&(d[433]); + assign q[434] = ((!a[434])&(!b[434]))|((c[434])|(!d[434])); + assign q[435] = (!a[435])|(!b[435]); + assign q[436] = (((!a[436])^(!b[436]))&((!c[436])|(!d[436])))&(e[436]); + assign q[437] = (((!a[437])^(!b[437]))^(!c[437]))&(!d[437]); + assign q[438] = (!a[438])^(b[438]); + assign q[439] = ((a[439])^(!b[439]))|(c[439]); + assign q[440] = ((a[440])^(!b[440]))|((!c[440])&(!d[440])); + assign q[441] = (((a[441])&(b[441]))^((c[441])&(d[441])))|(e[441]); + assign q[442] = (!a[442])|(b[442]); + assign q[443] = (!a[443])^(b[443]); + assign q[444] = ((a[444])^(!b[444]))|((c[444])&(d[444])); + assign q[445] = (((a[445])|(!b[445]))&(c[445]))|(d[445]); + assign q[446] = ((a[446])&(b[446]))^((c[446])^(!d[446])); + assign q[447] = ((!a[447])&(!b[447]))^(!c[447]); + assign q[448] = (((!a[448])^(b[448]))&(c[448]))|(!d[448]); + assign q[449] = (((a[449])|(!b[449]))|((c[449])&(d[449])))|(!e[449]); + assign q[450] = (((!a[450])|(b[450]))|(c[450]))^(!d[450]); + assign q[451] = ((a[451])^(b[451]))|((c[451])^(d[451])); + assign q[452] = (((a[452])^(!b[452]))|(c[452]))|(d[452]); + assign q[453] = (!a[453])^(!b[453]); + assign q[454] = (((a[454])|(!b[454]))|(c[454]))^(d[454]); + assign q[455] = ((!a[455])&(b[455]))^((!c[455])|(!d[455])); + assign q[456] = (((a[456])^(!b[456]))|((c[456])^(d[456])))^(e[456]); + assign q[457] = (((a[457])&(!b[457]))^(c[457]))|(d[457]); + assign q[458] = (((!a[458])^(b[458]))^(c[458]))&(!d[458]); + assign q[459] = (((!a[459])&(b[459]))^((!c[459])&(!d[459])))&(e[459]); + assign q[460] = ((!a[460])^(!b[460]))|((c[460])&(!d[460])); + assign q[461] = ((a[461])&(!b[461]))&(c[461]); + assign q[462] = (((a[462])|(b[462]))^((c[462])^(d[462])))|(!e[462]); + assign q[463] = (((a[463])|(!b[463]))&((!c[463])|(d[463])))|(e[463]); + assign q[464] = (((!a[464])^(b[464]))&((!c[464])|(!d[464])))^(e[464]); + assign q[465] = ((!a[465])|(b[465]))&((c[465])&(d[465])); + assign q[466] = (((!a[466])^(b[466]))|((!c[466])&(d[466])))&(e[466]); + assign q[467] = (((!a[467])|(!b[467]))&((!c[467])&(!d[467])))^(!e[467]); + assign q[468] = ((!a[468])^(!b[468]))&((c[468])&(!d[468])); + assign q[469] = (((a[469])^(b[469]))^(c[469]))&(!d[469]); + assign q[470] = (((a[470])&(b[470]))^(c[470]))&(d[470]); + assign q[471] = (((!a[471])&(b[471]))^(c[471]))&(!d[471]); + assign q[472] = (((!a[472])|(b[472]))|((!c[472])|(!d[472])))|(!e[472]); + assign q[473] = (((a[473])|(b[473]))|((c[473])^(d[473])))|(e[473]); + assign q[474] = (a[474])^(!b[474]); + assign q[475] = (a[475])&(!b[475]); + assign q[476] = (((a[476])^(!b[476]))&((c[476])&(d[476])))|(!e[476]); + assign q[477] = ((a[477])^(b[477]))&(!c[477]); + assign q[478] = (((a[478])|(!b[478]))&((c[478])^(d[478])))|(e[478]); + assign q[479] = (((a[479])|(!b[479]))&((c[479])&(!d[479])))|(!e[479]); + assign q[480] = (((!a[480])|(b[480]))&((!c[480])|(!d[480])))|(e[480]); + assign q[481] = (((!a[481])&(b[481]))|((!c[481])^(d[481])))&(!e[481]); + assign q[482] = (a[482])^(!b[482]); + assign q[483] = (a[483])|(b[483]); + assign q[484] = (((a[484])|(!b[484]))&(c[484]))|(!d[484]); + assign q[485] = (((a[485])^(!b[485]))&(c[485]))|(!d[485]); + assign q[486] = ((!a[486])^(b[486]))&(c[486]); + assign q[487] = ((!a[487])&(b[487]))^((!c[487])^(!d[487])); + assign q[488] = ((a[488])&(b[488]))^((c[488])^(d[488])); + assign q[489] = (a[489])^(!b[489]); + assign q[490] = (((!a[490])^(b[490]))&(!c[490]))|(!d[490]); + assign q[491] = (a[491])^(!b[491]); + assign q[492] = (!a[492])|(!b[492]); + assign q[493] = (((!a[493])|(!b[493]))|((c[493])^(d[493])))^(e[493]); + assign q[494] = (((a[494])&(b[494]))^((c[494])&(!d[494])))&(e[494]); + assign q[495] = (((a[495])|(!b[495]))|((!c[495])^(d[495])))^(!e[495]); + assign q[496] = (((a[496])^(b[496]))&((!c[496])^(!d[496])))&(!e[496]); + assign q[497] = (((a[497])^(!b[497]))|((!c[497])&(d[497])))|(e[497]); + assign q[498] = (((!a[498])|(!b[498]))&(c[498]))&(!d[498]); + assign q[499] = (((a[499])|(b[499]))^((c[499])^(!d[499])))|(!e[499]); + assign q[500] = ((a[500])&(b[500]))^((!c[500])^(!d[500])); + assign q[501] = (((a[501])&(!b[501]))|(!c[501]))|(!d[501]); + assign q[502] = (((a[502])^(!b[502]))^(!c[502]))|(!d[502]); + assign q[503] = (((!a[503])&(b[503]))|(!c[503]))^(!d[503]); + assign q[504] = (((a[504])&(b[504]))|(c[504]))|(d[504]); + assign q[505] = (((!a[505])&(b[505]))&((c[505])&(!d[505])))^(!e[505]); + assign q[506] = (((!a[506])|(b[506]))|(c[506]))&(!d[506]); + assign q[507] = (((!a[507])^(b[507]))^(c[507]))&(d[507]); + assign q[508] = (((!a[508])&(b[508]))|((!c[508])|(d[508])))|(!e[508]); + assign q[509] = (!a[509])|(b[509]); + assign q[510] = (((a[510])|(!b[510]))^(c[510]))^(d[510]); + assign q[511] = ((!a[511])|(!b[511]))|((c[511])|(d[511])); + assign q[512] = ((a[512])|(!b[512]))&((!c[512])&(d[512])); + assign q[513] = (!a[513])&(!b[513]); + assign q[514] = (((a[514])|(!b[514]))^(!c[514]))&(d[514]); + assign q[515] = (((!a[515])|(!b[515]))^(c[515]))|(!d[515]); + assign q[516] = ((a[516])|(b[516]))|((c[516])&(!d[516])); + assign q[517] = (((a[517])^(!b[517]))^((c[517])&(!d[517])))&(e[517]); + assign q[518] = (((a[518])&(!b[518]))^((c[518])|(!d[518])))^(!e[518]); + assign q[519] = (((!a[519])^(!b[519]))&((c[519])&(d[519])))|(e[519]); + assign q[520] = ((a[520])^(b[520]))|((c[520])&(!d[520])); + assign q[521] = (((!a[521])^(!b[521]))^((!c[521])|(!d[521])))|(e[521]); + assign q[522] = (((a[522])|(b[522]))|(c[522]))&(!d[522]); + assign q[523] = (((a[523])|(b[523]))^((c[523])|(!d[523])))|(e[523]); + assign q[524] = ((!a[524])^(b[524]))&(c[524]); + assign q[525] = (a[525])&(b[525]); + assign q[526] = ((a[526])|(!b[526]))^((!c[526])^(!d[526])); + assign q[527] = ((!a[527])&(!b[527]))&((!c[527])|(!d[527])); + assign q[528] = ((a[528])^(b[528]))&(!c[528]); + assign q[529] = ((a[529])^(b[529]))|((c[529])|(!d[529])); + assign q[530] = ((!a[530])&(b[530]))|((c[530])&(!d[530])); + assign q[531] = (a[531])|(b[531]); + assign q[532] = (((!a[532])|(b[532]))&(c[532]))|(d[532]); + assign q[533] = ((a[533])&(!b[533]))&((c[533])&(!d[533])); + assign q[534] = (((a[534])&(!b[534]))&(!c[534]))|(d[534]); + assign q[535] = ((!a[535])^(b[535]))|((c[535])&(!d[535])); + assign q[536] = (((a[536])&(!b[536]))|((c[536])|(!d[536])))|(!e[536]); + assign q[537] = ((!a[537])^(b[537]))^((c[537])&(!d[537])); + assign q[538] = (((!a[538])&(b[538]))&(c[538]))|(d[538]); + assign q[539] = (a[539])|(!b[539]); + assign q[540] = (((!a[540])|(!b[540]))^((!c[540])|(d[540])))&(!e[540]); + assign q[541] = ((!a[541])&(!b[541]))&((c[541])^(d[541])); + assign q[542] = (((a[542])|(!b[542]))^(!c[542]))&(d[542]); + assign q[543] = (((!a[543])&(b[543]))&(!c[543]))^(d[543]); + assign q[544] = (((!a[544])|(b[544]))&((!c[544])&(d[544])))&(e[544]); + assign q[545] = (((a[545])^(!b[545]))|(!c[545]))&(d[545]); + assign q[546] = (((!a[546])|(!b[546]))^((!c[546])|(d[546])))&(!e[546]); + assign q[547] = (((a[547])^(!b[547]))|(c[547]))|(!d[547]); + assign q[548] = (((!a[548])^(b[548]))&((c[548])|(!d[548])))&(!e[548]); + assign q[549] = ((a[549])|(!b[549]))^((!c[549])^(d[549])); + assign q[550] = ((!a[550])&(!b[550]))^(c[550]); + assign q[551] = (((!a[551])&(b[551]))|((c[551])&(!d[551])))&(!e[551]); + assign q[552] = (((a[552])|(b[552]))^((!c[552])|(!d[552])))&(!e[552]); + assign q[553] = (((a[553])|(b[553]))|((!c[553])|(d[553])))&(e[553]); + assign q[554] = (((a[554])&(!b[554]))^(!c[554]))^(d[554]); + assign q[555] = ((!a[555])^(b[555]))|(!c[555]); + assign q[556] = (((!a[556])^(!b[556]))^(!c[556]))|(d[556]); + assign q[557] = ((a[557])&(!b[557]))|((c[557])&(d[557])); + assign q[558] = (((a[558])&(!b[558]))^((!c[558])^(!d[558])))^(!e[558]); + assign q[559] = (((!a[559])|(!b[559]))|((!c[559])|(!d[559])))^(!e[559]); + assign q[560] = ((!a[560])|(!b[560]))|((!c[560])^(d[560])); + assign q[561] = (((!a[561])|(b[561]))|(c[561]))^(!d[561]); + assign q[562] = ((!a[562])&(!b[562]))&((!c[562])^(!d[562])); + assign q[563] = (((a[563])^(b[563]))^(!c[563]))|(d[563]); + assign q[564] = (((!a[564])|(b[564]))|(!c[564]))|(d[564]); + assign q[565] = (((a[565])&(!b[565]))&((c[565])|(d[565])))|(!e[565]); + assign q[566] = (((a[566])&(b[566]))^(!c[566]))|(!d[566]); + assign q[567] = (((!a[567])&(!b[567]))&((c[567])&(!d[567])))|(!e[567]); + assign q[568] = (((!a[568])|(!b[568]))|(!c[568]))&(!d[568]); + assign q[569] = (!a[569])&(b[569]); + assign q[570] = ((!a[570])|(b[570]))|((!c[570])|(!d[570])); + assign q[571] = (((a[571])|(b[571]))&((!c[571])|(!d[571])))&(!e[571]); + assign q[572] = ((!a[572])&(b[572]))|((c[572])|(!d[572])); + assign q[573] = ((a[573])^(!b[573]))|((!c[573])|(!d[573])); + assign q[574] = (((!a[574])|(b[574]))&((!c[574])&(!d[574])))&(!e[574]); + assign q[575] = (((!a[575])&(b[575]))&((!c[575])|(!d[575])))|(!e[575]); + assign q[576] = (((a[576])|(!b[576]))^((c[576])^(d[576])))|(e[576]); + assign q[577] = (((a[577])|(b[577]))&(c[577]))^(d[577]); + assign q[578] = ((a[578])^(!b[578]))&(!c[578]); + assign q[579] = (((!a[579])&(!b[579]))^((!c[579])|(!d[579])))|(!e[579]); + assign q[580] = (((!a[580])|(b[580]))|(!c[580]))^(d[580]); + assign q[581] = ((a[581])&(b[581]))&((!c[581])|(d[581])); + assign q[582] = (((!a[582])^(b[582]))|(!c[582]))&(!d[582]); + assign q[583] = (a[583])&(b[583]); + assign q[584] = (((!a[584])|(b[584]))|((c[584])^(d[584])))^(e[584]); + assign q[585] = ((a[585])&(b[585]))|((!c[585])|(!d[585])); + assign q[586] = (((a[586])|(b[586]))^((!c[586])|(d[586])))^(!e[586]); + assign q[587] = ((a[587])|(!b[587]))&(!c[587]); + assign q[588] = (((!a[588])&(b[588]))^((!c[588])|(!d[588])))|(!e[588]); + assign q[589] = (((!a[589])|(b[589]))&((!c[589])|(d[589])))&(e[589]); + assign q[590] = (((a[590])^(b[590]))^((!c[590])&(d[590])))&(!e[590]); + assign q[591] = ((a[591])^(!b[591]))|(!c[591]); + assign q[592] = ((a[592])|(!b[592]))^((!c[592])^(!d[592])); + assign q[593] = ((!a[593])|(b[593]))&((c[593])&(!d[593])); + assign q[594] = ((!a[594])&(!b[594]))^(!c[594]); + assign q[595] = (((!a[595])^(b[595]))|(!c[595]))&(d[595]); + assign q[596] = (((a[596])|(!b[596]))&(!c[596]))|(!d[596]); + assign q[597] = (a[597])&(!b[597]); + assign q[598] = ((a[598])^(b[598]))|((!c[598])&(d[598])); + assign q[599] = ((a[599])&(b[599]))&(!c[599]); + assign q[600] = ((!a[600])|(b[600]))|((!c[600])^(!d[600])); + assign q[601] = ((a[601])&(!b[601]))|((c[601])^(!d[601])); + assign q[602] = ((!a[602])&(!b[602]))^(!c[602]); + assign q[603] = ((a[603])&(!b[603]))^((c[603])&(!d[603])); + assign q[604] = ((a[604])&(!b[604]))&((c[604])^(!d[604])); + assign q[605] = (((!a[605])|(b[605]))&((c[605])|(d[605])))|(e[605]); + assign q[606] = (((a[606])|(!b[606]))|((!c[606])^(d[606])))&(e[606]); + assign q[607] = ((a[607])&(!b[607]))^(!c[607]); + assign q[608] = ((a[608])^(!b[608]))&(!c[608]); + assign q[609] = ((a[609])^(!b[609]))&((!c[609])&(d[609])); + assign q[610] = ((!a[610])&(!b[610]))&(c[610]); + assign q[611] = (((!a[611])|(b[611]))&(!c[611]))|(!d[611]); + assign q[612] = (((a[612])^(!b[612]))&((!c[612])|(d[612])))^(e[612]); + assign q[613] = (((!a[613])|(b[613]))^((c[613])&(!d[613])))|(!e[613]); + assign q[614] = (a[614])^(!b[614]); + assign q[615] = (((!a[615])^(b[615]))|(!c[615]))^(d[615]); + assign q[616] = ((!a[616])&(!b[616]))|((c[616])&(!d[616])); + assign q[617] = (((a[617])^(b[617]))|(c[617]))|(d[617]); + assign q[618] = (((!a[618])^(!b[618]))^((c[618])^(d[618])))^(e[618]); + assign q[619] = (((!a[619])|(!b[619]))|(c[619]))^(!d[619]); + assign q[620] = (!a[620])^(!b[620]); + assign q[621] = ((!a[621])&(!b[621]))&((!c[621])|(d[621])); + assign q[622] = (((a[622])^(b[622]))&((!c[622])|(!d[622])))|(!e[622]); + assign q[623] = (((a[623])&(!b[623]))^(c[623]))&(d[623]); + assign q[624] = (((a[624])&(b[624]))|(c[624]))^(!d[624]); + assign q[625] = (((!a[625])^(!b[625]))&((!c[625])|(d[625])))&(!e[625]); + assign q[626] = (((!a[626])&(!b[626]))^(!c[626]))|(!d[626]); + assign q[627] = ((!a[627])|(b[627]))|(c[627]); + assign q[628] = (((!a[628])&(!b[628]))^((!c[628])|(!d[628])))^(e[628]); + assign q[629] = ((a[629])&(!b[629]))|((c[629])^(d[629])); + assign q[630] = (((!a[630])|(b[630]))^((c[630])|(!d[630])))|(!e[630]); + assign q[631] = (((!a[631])&(b[631]))&(!c[631]))^(!d[631]); + assign q[632] = (((a[632])&(!b[632]))&(!c[632]))|(!d[632]); + assign q[633] = (((a[633])|(b[633]))^(c[633]))|(d[633]); + assign q[634] = (((a[634])&(b[634]))|((c[634])|(d[634])))&(e[634]); + assign q[635] = (((a[635])&(!b[635]))&((c[635])&(!d[635])))&(!e[635]); + assign q[636] = (((!a[636])|(b[636]))^((!c[636])^(d[636])))^(e[636]); + assign q[637] = (((a[637])&(b[637]))&((!c[637])&(d[637])))|(!e[637]); + assign q[638] = ((!a[638])|(!b[638]))&(!c[638]); + assign q[639] = (((a[639])|(!b[639]))&((c[639])|(d[639])))^(!e[639]); + assign q[640] = (!a[640])&(b[640]); + assign q[641] = ((!a[641])^(!b[641]))^((!c[641])^(d[641])); + assign q[642] = (((!a[642])^(!b[642]))&(c[642]))&(!d[642]); + assign q[643] = (!a[643])^(!b[643]); + assign q[644] = ((!a[644])|(!b[644]))|((!c[644])^(!d[644])); + assign q[645] = (((a[645])&(b[645]))^((c[645])&(!d[645])))|(e[645]); + assign q[646] = ((a[646])&(!b[646]))&(c[646]); + assign q[647] = ((a[647])&(!b[647]))^((!c[647])^(!d[647])); + assign q[648] = (((!a[648])|(b[648]))&((!c[648])&(d[648])))|(e[648]); + assign q[649] = ((!a[649])|(b[649]))|((c[649])&(!d[649])); + assign q[650] = (((!a[650])&(b[650]))^(c[650]))^(d[650]); + assign q[651] = ((a[651])|(b[651]))^(!c[651]); + assign q[652] = (((a[652])^(b[652]))&((c[652])|(d[652])))|(e[652]); + assign q[653] = (((!a[653])|(b[653]))^(c[653]))^(d[653]); + assign q[654] = (((a[654])^(!b[654]))^(!c[654]))^(d[654]); + assign q[655] = (((!a[655])|(b[655]))|((!c[655])&(d[655])))&(e[655]); + assign q[656] = (((a[656])^(b[656]))|((!c[656])^(!d[656])))^(!e[656]); + assign q[657] = ((a[657])&(!b[657]))&(c[657]); + assign q[658] = (((!a[658])|(b[658]))|((!c[658])^(!d[658])))|(e[658]); + assign q[659] = (((a[659])&(b[659]))&((c[659])|(!d[659])))^(e[659]); + assign q[660] = (((!a[660])&(!b[660]))|((!c[660])|(!d[660])))&(e[660]); + assign q[661] = ((a[661])&(!b[661]))^((!c[661])^(!d[661])); + assign q[662] = (((!a[662])|(!b[662]))|((c[662])|(!d[662])))^(!e[662]); + assign q[663] = (a[663])^(b[663]); + assign q[664] = ((!a[664])&(!b[664]))|((!c[664])&(!d[664])); + assign q[665] = (((a[665])|(b[665]))&((!c[665])&(!d[665])))^(e[665]); + assign q[666] = (((a[666])&(b[666]))|((c[666])|(d[666])))|(!e[666]); + assign q[667] = ((a[667])&(!b[667]))&(!c[667]); + assign q[668] = (((!a[668])&(b[668]))^(c[668]))|(d[668]); + assign q[669] = (((!a[669])^(b[669]))^((!c[669])^(!d[669])))&(e[669]); + assign q[670] = ((!a[670])|(b[670]))&((c[670])|(!d[670])); + assign q[671] = (((a[671])&(!b[671]))^(c[671]))^(!d[671]); + assign q[672] = (((a[672])^(b[672]))^((c[672])&(!d[672])))|(!e[672]); + assign q[673] = (((a[673])^(!b[673]))&((c[673])|(d[673])))|(!e[673]); + assign q[674] = ((!a[674])|(!b[674]))|((!c[674])^(d[674])); + assign q[675] = ((!a[675])^(b[675]))&((!c[675])|(!d[675])); + assign q[676] = (((!a[676])&(!b[676]))^((!c[676])&(d[676])))|(!e[676]); + assign q[677] = (((!a[677])&(!b[677]))^(c[677]))&(!d[677]); + assign q[678] = (((!a[678])|(!b[678]))&((c[678])^(!d[678])))&(e[678]); + assign q[679] = (!a[679])|(b[679]); + assign q[680] = (a[680])&(!b[680]); + assign q[681] = (((!a[681])|(b[681]))|((c[681])&(d[681])))|(!e[681]); + assign q[682] = ((a[682])&(!b[682]))^((!c[682])|(!d[682])); + assign q[683] = ((!a[683])&(!b[683]))|((!c[683])^(!d[683])); + assign q[684] = (!a[684])&(!b[684]); + assign q[685] = (((a[685])&(!b[685]))|((c[685])&(!d[685])))|(!e[685]); + assign q[686] = (a[686])^(!b[686]); + assign q[687] = (((!a[687])|(b[687]))&((!c[687])|(d[687])))^(e[687]); + assign q[688] = (((a[688])^(!b[688]))^((!c[688])&(!d[688])))&(!e[688]); + assign q[689] = (((!a[689])^(b[689]))^(c[689]))&(!d[689]); + assign q[690] = ((a[690])^(!b[690]))|((!c[690])|(!d[690])); + assign q[691] = (((!a[691])^(b[691]))&((!c[691])&(!d[691])))^(!e[691]); + assign q[692] = ((a[692])^(!b[692]))|((c[692])|(!d[692])); + assign q[693] = (((a[693])&(b[693]))&((!c[693])|(d[693])))^(e[693]); + assign q[694] = ((!a[694])^(!b[694]))^((c[694])^(!d[694])); + assign q[695] = ((a[695])&(b[695]))&((!c[695])|(!d[695])); + assign q[696] = ((a[696])|(b[696]))&((c[696])|(d[696])); + assign q[697] = (((!a[697])^(b[697]))|((c[697])^(!d[697])))|(e[697]); + assign q[698] = (((a[698])|(b[698]))|((!c[698])&(!d[698])))^(!e[698]); + assign q[699] = (((!a[699])|(!b[699]))&(c[699]))|(!d[699]); + assign q[700] = ((!a[700])&(b[700]))|((!c[700])|(d[700])); + assign q[701] = (((!a[701])|(b[701]))|((c[701])^(d[701])))&(e[701]); + assign q[702] = (((!a[702])&(b[702]))&(c[702]))&(!d[702]); + assign q[703] = ((!a[703])&(!b[703]))|((c[703])|(d[703])); + assign q[704] = (((a[704])^(b[704]))^((c[704])&(d[704])))|(!e[704]); + assign q[705] = ((a[705])^(!b[705]))^((!c[705])^(!d[705])); + assign q[706] = (((!a[706])^(b[706]))^((!c[706])&(!d[706])))&(e[706]); + assign q[707] = ((a[707])&(!b[707]))|((c[707])^(d[707])); + assign q[708] = (((a[708])^(b[708]))|(!c[708]))|(d[708]); + assign q[709] = (((!a[709])&(b[709]))^((!c[709])&(!d[709])))&(!e[709]); + assign q[710] = ((!a[710])^(!b[710]))^(c[710]); + assign q[711] = (!a[711])&(b[711]); + assign q[712] = ((a[712])^(b[712]))&((c[712])^(!d[712])); + assign q[713] = (((a[713])^(b[713]))|((!c[713])^(d[713])))|(!e[713]); + assign q[714] = (((a[714])|(b[714]))&((c[714])^(d[714])))^(!e[714]); + assign q[715] = ((a[715])|(b[715]))|((!c[715])^(d[715])); + assign q[716] = (((a[716])|(b[716]))^(c[716]))^(!d[716]); + assign q[717] = (((!a[717])|(!b[717]))^((!c[717])^(!d[717])))^(e[717]); + assign q[718] = (((a[718])^(!b[718]))&(!c[718]))^(d[718]); + assign q[719] = (((!a[719])^(!b[719]))&((!c[719])|(d[719])))&(!e[719]); + assign q[720] = ((!a[720])^(b[720]))|(c[720]); + assign q[721] = ((!a[721])&(!b[721]))|((c[721])&(d[721])); + assign q[722] = (((!a[722])|(!b[722]))&((!c[722])&(!d[722])))&(!e[722]); + assign q[723] = ((a[723])|(b[723]))&((c[723])|(d[723])); + assign q[724] = (((!a[724])|(b[724]))^((c[724])^(!d[724])))^(e[724]); + assign q[725] = (((!a[725])^(!b[725]))|(!c[725]))&(!d[725]); + assign q[726] = ((a[726])^(!b[726]))^(c[726]); + assign q[727] = ((!a[727])&(!b[727]))^(c[727]); + assign q[728] = ((!a[728])^(!b[728]))^(c[728]); + assign q[729] = ((!a[729])&(b[729]))&(!c[729]); + assign q[730] = (((a[730])|(!b[730]))&(!c[730]))&(!d[730]); + assign q[731] = ((!a[731])|(!b[731]))^(c[731]); + assign q[732] = ((!a[732])&(!b[732]))|(c[732]); + assign q[733] = ((!a[733])&(!b[733]))^(!c[733]); + assign q[734] = (((a[734])|(b[734]))|((!c[734])^(!d[734])))|(!e[734]); + assign q[735] = (a[735])^(b[735]); + assign q[736] = ((!a[736])|(b[736]))&(!c[736]); + assign q[737] = (((!a[737])|(b[737]))|(c[737]))&(!d[737]); + assign q[738] = (((a[738])^(b[738]))^((c[738])^(!d[738])))|(e[738]); + assign q[739] = (!a[739])^(b[739]); + assign q[740] = (((a[740])|(b[740]))^((!c[740])^(!d[740])))&(!e[740]); + assign q[741] = ((!a[741])&(b[741]))^((!c[741])^(!d[741])); + assign q[742] = (((a[742])|(b[742]))|(c[742]))|(d[742]); + assign q[743] = (((a[743])&(b[743]))&((c[743])&(d[743])))|(!e[743]); + assign q[744] = (((!a[744])&(!b[744]))^((!c[744])&(d[744])))^(e[744]); + assign q[745] = (((!a[745])&(b[745]))^((!c[745])|(!d[745])))^(e[745]); + assign q[746] = (((a[746])&(b[746]))^(!c[746]))&(!d[746]); + assign q[747] = (((!a[747])^(b[747]))^((!c[747])^(d[747])))|(e[747]); + assign q[748] = (((a[748])^(b[748]))|((c[748])^(d[748])))&(!e[748]); + assign q[749] = (((a[749])^(b[749]))|((c[749])|(!d[749])))|(e[749]); +endmodule diff --git a/tests/arch/gatemate/luttrees.ys b/tests/arch/gatemate/luttrees.ys new file mode 100644 index 000000000..545643226 --- /dev/null +++ b/tests/arch/gatemate/luttrees.ys @@ -0,0 +1,13 @@ + +read_verilog luttrees.v +design -save read + +hierarchy -top luttrees +proc +equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad -luttree -nomx4 -nomx8 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd luttrees # Constrain all select calls below inside the top module + +select -assert-count 750 t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %% +select -assert-none t:CC_LUT2 t:CC_L2T4 t:CC_L2T5 %% t:* %D + diff --git a/tests/arch/ice40/.gitignore b/tests/arch/ice40/.gitignore index 9a71dca69..54f908bdb 100644 --- a/tests/arch/ice40/.gitignore +++ b/tests/arch/ice40/.gitignore @@ -1,4 +1,5 @@ *.log +*.json /run-test.mk +*_synth.v +*_testbench diff --git a/tests/arch/ice40/bug1597.ys b/tests/arch/ice40/bug1597.ys index b7983cfa4..c1509cabc 100644 --- a/tests/arch/ice40/bug1597.ys +++ b/tests/arch/ice40/bug1597.ys @@ -3,7 +3,7 @@ module top ( input CLK, PIN_1, PIN_2, PIN_3, PIN_4, PIN_5, PIN_6, PIN_7, PIN_8, PIN_9, PIN_10, PIN_11, PIN_12, PIN_13, PIN_25, output USBPU, PIN_14, PIN_15, PIN_16, PIN_17, PIN_18, - PIN_19, PIN_20, PIN_21, PIN_22, PIN_23, PIN_24, + PIN_19, ); assign USBPU = 0; @@ -67,6 +67,7 @@ module SSCounter6o (input wire rst, clk, adv, jmp, input wire [5:0] in, output w SB_LUT4 #(.LUT_INIT(16'h8BB8)) l5 (lo[5], in[5], jmp, out[5], co[4]); endmodule EOT +read_verilog -lib +/ice40/cells_sim.v hierarchy -top top flatten -equiv_opt -multiclock -map +/ice40/cells_sim.v synth_ice40 +equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 diff --git a/tests/arch/ice40/ice40_opt.ys b/tests/arch/ice40/ice40_opt.ys index 71b68431e..e779ab207 100644 --- a/tests/arch/ice40/ice40_opt.ys +++ b/tests/arch/ice40/ice40_opt.ys @@ -21,6 +21,7 @@ module top(input CI, I0, output [1:0] CO, output O); endmodule EOT +read_verilog -icells -lib +/ice40/abc9_model.v +/ice40/cells_sim.v equiv_opt -assert -map +/ice40/abc9_model.v -map +/ice40/cells_sim.v ice40_opt design -load postopt select -assert-count 1 t:* diff --git a/tests/arch/intel_alm/counter.ys b/tests/arch/intel_alm/counter.ys index 56c9cabb3..0a5b9356a 100644 --- a/tests/arch/intel_alm/counter.ys +++ b/tests/arch/intel_alm/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # equivalency check +equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd top # Constrain all select calls below inside the top module @@ -17,7 +17,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check +equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd top # Constrain all select calls below inside the top module diff --git a/tests/arch/xilinx/abc9_dff.ys b/tests/arch/xilinx/abc9_dff.ys index 0ba3901f7..79e5a322c 100644 --- a/tests/arch/xilinx/abc9_dff.ys +++ b/tests/arch/xilinx/abc9_dff.ys @@ -12,6 +12,7 @@ FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[6])); FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[7])); endmodule EOT +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 6 t:FD* @@ -31,6 +32,7 @@ FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6])); FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7])); endmodule EOT +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 4 t:FD* @@ -54,6 +56,7 @@ logger -expect warning "Whitebox '\$paramod\\FDRE\\INIT=.*1' with \(\* abc9_flop logger -expect warning "Whitebox '\$paramod\\FDRE_1\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 logger -expect warning "Whitebox 'FDSE' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 logger -expect warning "Whitebox '\$paramod\\FDSE_1\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 8 t:FD* @@ -75,6 +78,7 @@ always @(posedge clk or posedge pre) endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 1 t:FDCE @@ -94,6 +98,7 @@ assign q = ~r; endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 1 t:FDRE %co w:r %i @@ -111,6 +116,7 @@ assign q2 = r; endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 1 t:FDRE %co %a w:r %i @@ -128,6 +134,7 @@ assign o = r1 | r2; endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf diff --git a/tests/arch/xilinx/opt_lut_ins.ys b/tests/arch/xilinx/opt_lut_ins.ys index a01d02179..2328919a3 100644 --- a/tests/arch/xilinx/opt_lut_ins.ys +++ b/tests/arch/xilinx/opt_lut_ins.ys @@ -18,6 +18,7 @@ end EOF +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -map +/xilinx/cells_sim.v opt_lut_ins -tech xilinx design -load postopt diff --git a/tests/arch/xilinx/xilinx_dffopt.ys b/tests/arch/xilinx/xilinx_dffopt.ys index c09699411..9f0b27ced 100644 --- a/tests/arch/xilinx/xilinx_dffopt.ys +++ b/tests/arch/xilinx/xilinx_dffopt.ys @@ -5,7 +5,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -52,7 +52,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -100,7 +100,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -137,7 +137,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -183,7 +183,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -232,7 +232,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; diff --git a/tests/blif/bug3374.ys b/tests/blif/bug3374.ys new file mode 100644 index 000000000..792d4de20 --- /dev/null +++ b/tests/blif/bug3374.ys @@ -0,0 +1,4 @@ +logger -expect error "Syntax error in line 1!" 1 +read_blif <<EOF +.model +EOF diff --git a/tests/blif/bug3385.ys b/tests/blif/bug3385.ys new file mode 100644 index 000000000..e1e45983d --- /dev/null +++ b/tests/blif/bug3385.ys @@ -0,0 +1,9 @@ +logger -expect error "Syntax error in line 4: names' input plane must have fewer than 13 signals." 1 +read_blif <<EOF +.model test +.inputs w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 w16 w17 w18 w19 w20 w21 w22 w23 w24 w25 w26 w27 w28 w29 w30 +.outputs out +.names w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 w16 w17 w18 w19 w20 w21 w22 w23 w24 w25 w26 w27 w28 w29 w30 out +1101010001100110010001100111001 0 +.end +EOF diff --git a/tests/gen-tests-makefile.sh b/tests/gen-tests-makefile.sh index ab8fb7013..cde9ab1b9 100755 --- a/tests/gen-tests-makefile.sh +++ b/tests/gen-tests-makefile.sh @@ -17,7 +17,7 @@ generate_target() { generate_ys_test() { ys_file=$1 yosys_args=${2:-} - generate_target "$ys_file" "$YOSYS_BASEDIR/yosys -ql ${ys_file%.*}.log $yosys_args $ys_file" + generate_target "$ys_file" "\"$YOSYS_BASEDIR/yosys\" -ql ${ys_file%.*}.log $yosys_args $ys_file" } # $ generate_bash_test bash_file diff --git a/tests/opt/opt_dff_en.ys b/tests/opt/opt_dff_en.ys index 06ee6c63d..9538afcc2 100644 --- a/tests/opt/opt_dff_en.ys +++ b/tests/opt/opt_dff_en.ys @@ -6,7 +6,7 @@ module top(...); input CLK; input [1:0] D; -output [15:0] Q; +output [11:0] Q; input SRST; input ARST; input [1:0] CLR; diff --git a/tests/opt/opt_dff_mux.ys b/tests/opt/opt_dff_mux.ys index ed01bed59..f21f9e9b8 100644 --- a/tests/opt/opt_dff_mux.ys +++ b/tests/opt/opt_dff_mux.ys @@ -7,7 +7,7 @@ module top(...); input CLK; input NE, NS; input EN; -output [23:0] Q; +output [17:0] Q; input [23:0] D; input SRST; input ARST; diff --git a/tests/opt/opt_dff_qd.ys b/tests/opt/opt_dff_qd.ys index afc96c42f..7b0b4c224 100644 --- a/tests/opt/opt_dff_qd.ys +++ b/tests/opt/opt_dff_qd.ys @@ -7,7 +7,7 @@ module top(...); input CLK; input EN; (* init = 24'h555555 *) -output [23:0] Q; +output [19:0] Q; input SRST; input ARST; input [1:0] CLR; diff --git a/tests/opt/opt_dff_sr.ys b/tests/opt/opt_dff_sr.ys index 0961cb11e..1d3fd300e 100644 --- a/tests/opt/opt_dff_sr.ys +++ b/tests/opt/opt_dff_sr.ys @@ -22,10 +22,9 @@ EOT design -save orig -# Equivalence check will fail for unmapped adlatch and dlatchsr due to negative hold hack. -#equiv_opt -undef -assert -multiclock opt_dff -#design -load postopt -opt_dff +equiv_opt -undef -assert -multiclock opt_dff +design -load postopt + select -assert-count 1 t:$dffsr select -assert-count 1 t:$dffsr r:WIDTH=2 %i select -assert-count 1 t:$dffsre @@ -36,9 +35,9 @@ select -assert-none t:$sr design -load orig -#equiv_opt -undef -assert -multiclock opt_dff -keepdc -#design -load postopt -opt_dff -keepdc +equiv_opt -undef -assert -multiclock opt_dff -keepdc +design -load postopt + select -assert-count 1 t:$dffsr select -assert-count 1 t:$dffsr r:WIDTH=4 %i select -assert-count 1 t:$dffsre @@ -51,9 +50,9 @@ select -assert-count 1 t:$sr r:WIDTH=4 %i design -load orig simplemap -#equiv_opt -undef -assert -multiclock opt_dff -#design -load postopt -opt_dff +equiv_opt -undef -assert -multiclock opt_dff +design -load postopt + select -assert-count 1 t:$_DFF_PP0_ select -assert-count 1 t:$_DFF_PP1_ select -assert-count 1 t:$_DFFE_PN0P_ @@ -65,9 +64,9 @@ select -assert-none t:$_DFF_PP0_ t:$_DFF_PP1_ t:$_DFFE_PN0P_ t:$_DFFE_PN1P_ t:$_ design -load orig simplemap -#equiv_opt -undef -assert -multiclock opt_dff -keepdc -#design -load postopt -opt_dff -keepdc +equiv_opt -undef -assert -multiclock opt_dff -keepdc +design -load postopt + select -assert-count 1 t:$_DFF_PP0_ select -assert-count 1 t:$_DFF_PP1_ select -assert-count 2 t:$_DFFSR_PPP_ diff --git a/tests/opt/opt_expr_xnor.ys b/tests/opt/opt_expr_xnor.ys index f8ef0d352..225df7076 100644 --- a/tests/opt/opt_expr_xnor.ys +++ b/tests/opt/opt_expr_xnor.ys @@ -32,7 +32,7 @@ select -assert-count 1 c:* cd fine_keepdc simplemap opt_expr -keepdc -select -assert-count 1 t:$_XOR_ +select -assert-count 1 t:$_XNOR_ cd miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3 diff --git a/tests/opt/opt_expr_xor.ys b/tests/opt/opt_expr_xor.ys index a879f3ec9..9edec35d6 100644 --- a/tests/opt/opt_expr_xor.ys +++ b/tests/opt/opt_expr_xor.ys @@ -10,7 +10,7 @@ design -save read select -assert-count 2 t:$xor select -assert-count 2 t:$xnor -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt select -assert-none t:$xor select -assert-none t:$xnor @@ -19,12 +19,11 @@ select -assert-count 2 t:$not design -load read simplemap -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt select -assert-none t:$_XOR_ -select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_ -select -assert-count 3 t:$_NOT_ - +select -assert-none t:$_XNOR_ +select -assert-count 2 t:$_NOT_ design -reset read_verilog -icells <<EOT @@ -34,9 +33,9 @@ $_XNOR_ u1(.A(1'b1), .B(a), .Y(y[1])); endmodule EOT select -assert-count 2 t:$_XNOR_ -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt -select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_ +select -assert-none t:$_XNOR_ select -assert-count 1 t:$_NOT_ @@ -49,7 +48,7 @@ assign y = a~^1'b0; assign z = a~^1'b1; endmodule EOT -equiv_opt opt_expr +equiv_opt -assert opt_expr # Single-bit $xor diff --git a/tests/sim/run-test.sh b/tests/sim/run-test.sh index d34d1f3c9..a5120e77e 100755 --- a/tests/sim/run-test.sh +++ b/tests/sim/run-test.sh @@ -3,7 +3,7 @@ set -eu source ../gen-tests-makefile.sh echo "Generate FST for sim models" find tb/* -name tb*.v | while read name; do - test_name=$(basename -s .v $name) + test_name=$(basename $name .v) echo "Test $test_name" verilog_name=${test_name:3}.v iverilog -o tb/$test_name.out $name $verilog_name diff --git a/tests/simple/memory.v b/tests/simple/memory.v index f38bdafd3..b478d9409 100644 --- a/tests/simple/memory.v +++ b/tests/simple/memory.v @@ -137,8 +137,13 @@ endmodule // ---------------------------------------------------------- -module memtest06_sync(input clk, input rst, input [2:0] idx, input [7:0] din, output [7:0] dout); +module memtest06_sync(clk, rst, idx, din, dout); + input clk; + input rst; (* gentb_constant=0 *) wire rst; + input [2:0] idx; + input [7:0] din; + output [7:0] dout; reg [7:0] test [0:7]; integer i; always @(posedge clk) begin @@ -156,8 +161,13 @@ module memtest06_sync(input clk, input rst, input [2:0] idx, input [7:0] din, ou assign dout = test[idx]; endmodule -module memtest06_async(input clk, input rst, input [2:0] idx, input [7:0] din, output [7:0] dout); +module memtest06_async(clk, rst, idx, din, dout); + input clk; + input rst; (* gentb_constant=0 *) wire rst; + input [2:0] idx; + input [7:0] din; + output [7:0] dout; reg [7:0] test [0:7]; integer i; always @(posedge clk or posedge rst) begin diff --git a/tests/simple/module_scope_func.v b/tests/simple/module_scope_func.v new file mode 100644 index 000000000..928078da4 --- /dev/null +++ b/tests/simple/module_scope_func.v @@ -0,0 +1,45 @@ +// Some strict implementatins either forbid hierarchical identifiers within +// constant expressions, or forbid declaring functions in generate blocks, or +// both. Yosys and Iverilog are not strict in either of these ways. +module module_scope_func_top( + input wire inp, + output wire [31:0] out1, out2, out4, out5, out7, out8, + output reg [31:0] out3, out6, out9 +); + function automatic integer incr; + input integer value; + incr = value + 1; + endfunction + task send; + output integer out; + out = 55; + endtask + + assign out1 = module_scope_func_top.incr(inp); + localparam C = module_scope_func_top.incr(10); + assign out2 = C; + initial module_scope_func_top.send(out3); + + if (1) begin : blk + // shadows module_scope_func_top.incr + function automatic integer incr; + input integer value; + incr = value * 2; + endfunction + // shadows module_scope_func_top.send + task send; + output integer out; + out = 66; + endtask + + assign out4 = module_scope_func_top.incr(inp); + localparam D = module_scope_func_top.incr(20); + assign out5 = D; + initial module_scope_func_top.send(out6); + + assign out7 = incr(inp); + localparam E = incr(30); + assign out8 = E; + initial send(out9); + end +endmodule diff --git a/tests/svinterfaces/resolve_types.sv b/tests/svinterfaces/resolve_types.sv new file mode 100644 index 000000000..3c6644e33 --- /dev/null +++ b/tests/svinterfaces/resolve_types.sv @@ -0,0 +1,24 @@ +// This test checks that types, including package types, are resolved from within an interface. + +typedef logic [7:0] x_t; + +package pkg; + typedef logic [7:0] y_t; +endpackage + +interface iface; + x_t x; + pkg::y_t y; +endinterface + +module dut (input logic [7:0] x, output logic [7:0] y); + iface intf(); + assign intf.x = x; + assign y = intf.y; + + ondemand u(.intf); +endmodule + +module ref (input logic [7:0] x, output logic [7:0] y); + assign y = ~x; +endmodule diff --git a/tests/svinterfaces/resolve_types.ys b/tests/svinterfaces/resolve_types.ys new file mode 100644 index 000000000..a25791f37 --- /dev/null +++ b/tests/svinterfaces/resolve_types.ys @@ -0,0 +1,6 @@ +read_verilog -sv resolve_types.sv +hierarchy -libdir . -check +flatten +equiv_make ref dut equiv +equiv_simple +equiv_status -assert diff --git a/tests/svinterfaces/run-test.sh b/tests/svinterfaces/run-test.sh index 9ef53926c..afa222766 100755 --- a/tests/svinterfaces/run-test.sh +++ b/tests/svinterfaces/run-test.sh @@ -4,3 +4,4 @@ ./runone.sh svinterface_at_top ./run_simple.sh load_and_derive +./run_simple.sh resolve_types diff --git a/tests/svtypes/struct_array.sv b/tests/svtypes/struct_array.sv index 873f7befd..739f202ab 100644 --- a/tests/svtypes/struct_array.sv +++ b/tests/svtypes/struct_array.sv @@ -39,4 +39,195 @@ module top; always_comb assert(s2==80'hFC00_4200_0012_3400_FFFC); + // Same as s2, but with little endian addressing + struct packed { + bit [0:7] [7:0] a; // 8 element packed array of bytes + bit [0:15] b; // filler for non-zero offset + } s3; + + initial begin + s3 = '0; + + s3.a[5:6] = 16'h1234; + s3.a[2] = 8'h42; + + s3.a[0] = '1; + s3.a[0][1:0] = '0; + + s3.b = '1; + s3.b[14:15] = '0; + end + + always_comb assert(s3==80'hFC00_4200_0012_3400_FFFC); + + // Same as s3, but with little endian bit addressing + struct packed { + bit [0:7] [0:7] a; // 8 element packed array of bytes + bit [0:15] b; // filler for non-zero offset + } s3_b; + + initial begin + s3_b = '0; + + s3_b.a[5:6] = 16'h1234; + s3_b.a[2] = 8'h42; + + s3_b.a[0] = '1; + s3_b.a[0][6:7] = '0; + + s3_b.b = '1; + s3_b.b[14:15] = '0; + end + + always_comb assert(s3_b==80'hFC00_4200_0012_3400_FFFC); + + struct packed { + bit [0:7] [0:1] [0:3] a; + bit [0:15] b; // filler for non-zero offset + } s3_lll; + + initial begin + s3_lll = '0; + + s3_lll.a[5:6] = 16'h1234; + s3_lll.a[2] = 8'h42; + + s3_lll.a[0] = '1; + s3_lll.a[0][1][2:3] = '0; + + s3_lll.b = '1; + s3_lll.b[14:15] = '0; + end + + always_comb assert(s3_lll==80'hFC00_4200_0012_3400_FFFC); + + struct packed { + bit [0:7] [1:0] [0:3] a; + bit [0:15] b; // filler for non-zero offset + } s3_lbl; + + initial begin + s3_lbl = '0; + + s3_lbl.a[5:6] = 16'h1234; + s3_lbl.a[2] = 8'h42; + + s3_lbl.a[0] = '1; + s3_lbl.a[0][0][2:3] = '0; + + s3_lbl.b = '1; + s3_lbl.b[14:15] = '0; + end + + always_comb assert(s3_lbl==80'hFC00_4200_0012_3400_FFFC); + + struct packed { + bit [0:7] [0:1] [3:0] a; + bit [0:15] b; // filler for non-zero offset + } s3_llb; + + initial begin + s3_llb = '0; + + s3_llb.a[5:6] = 16'h1234; + s3_llb.a[2] = 8'h42; + + s3_llb.a[0] = '1; + s3_llb.a[0][1][1:0] = '0; + + s3_llb.b = '1; + s3_llb.b[14:15] = '0; + end + + always_comb assert(s3_llb==80'hFC00_4200_0012_3400_FFFC); + +`ifndef VERIFIC + // Note that the tests below for unpacked arrays in structs rely on the + // fact that they are actually packed in Yosys. + + // Same as s2, but using unpacked array syntax + struct packed { + bit [7:0] a [7:0]; // 8 element unpacked array of bytes + bit [15:0] b; // filler for non-zero offset + } s4; + + initial begin + s4 = '0; + + s4.a[2:1] = 16'h1234; + s4.a[5] = 8'h42; + + s4.a[7] = '1; + s4.a[7][1:0] = '0; + + s4.b = '1; + s4.b[1:0] = '0; + end + + always_comb assert(s4==80'hFC00_4200_0012_3400_FFFC); + + // Same as s3, but using unpacked array syntax + struct packed { + bit [7:0] a [0:7]; // 8 element unpacked array of bytes + bit [0:15] b; // filler for non-zero offset + } s5; + + initial begin + s5 = '0; + + s5.a[5:6] = 16'h1234; + s5.a[2] = 8'h42; + + s5.a[0] = '1; + s5.a[0][1:0] = '0; + + s5.b = '1; + s5.b[14:15] = '0; + end + + always_comb assert(s5==80'hFC00_4200_0012_3400_FFFC); + + // Same as s5, but with little endian bit addressing + struct packed { + bit [0:7] a [0:7]; // 8 element unpacked array of bytes + bit [0:15] b; // filler for non-zero offset + } s5_b; + + initial begin + s5_b = '0; + + s5_b.a[5:6] = 16'h1234; + s5_b.a[2] = 8'h42; + + s5_b.a[0] = '1; + s5_b.a[0][6:7] = '0; + + s5_b.b = '1; + s5_b.b[14:15] = '0; + end + + always_comb assert(s5_b==80'hFC00_4200_0012_3400_FFFC); + + // Same as s5, but using C-type unpacked array syntax + struct packed { + bit [7:0] a [8]; // 8 element unpacked array of bytes + bit [0:15] b; // filler for non-zero offset + } s6; + + initial begin + s6 = '0; + + s6.a[5:6] = 16'h1234; + s6.a[2] = 8'h42; + + s6.a[0] = '1; + s6.a[0][1:0] = '0; + + s6.b = '1; + s6.b[14:15] = '0; + end + + always_comb assert(s6==80'hFC00_4200_0012_3400_FFFC); +`endif + endmodule diff --git a/tests/svtypes/typedef_struct.sv b/tests/svtypes/typedef_struct.sv index 7ae007952..8df8e32b0 100644 --- a/tests/svtypes/typedef_struct.sv +++ b/tests/svtypes/typedef_struct.sv @@ -16,6 +16,7 @@ module top; bit a; logic[7:0] b; t_t t; + p::p_t ps; } s_t; s_t s; @@ -29,6 +30,7 @@ module top; assign s1 = s; assign ps.a = 8'hAA; assign ps.b = 8'h55; + assign s.ps = ps; always_comb begin assert(s.a == 1'b1); @@ -37,6 +39,8 @@ module top; assert(s1.t == 8'h55); assert(ps.a == 8'hAA); assert(ps.b == 8'h55); + assert(s.ps.a == 8'hAA); + assert(s.ps.b == 8'h55); end endmodule diff --git a/tests/svtypes/union_simple.sv b/tests/svtypes/union_simple.sv index 12e4b376f..a55df4d0a 100644 --- a/tests/svtypes/union_simple.sv +++ b/tests/svtypes/union_simple.sv @@ -48,14 +48,30 @@ module top; U_t u; } instruction_t; + typedef struct packed { + instruction_t ir; + logic [3:0] state; + } s_t; + instruction_t ir1; + s_t s1; + assign ir1 = 32'h0AA01EB7; // lui t4,0xAA01 + assign s1.ir = ir1; + assign s1.state = '1; + always_comb begin assert(ir1.u.opcode == 'h37); assert(ir1.r.opcode == 'h37); assert(ir1.u.rd == 'd29); assert(ir1.r.rd == 'd29); assert(ir1.u.imm == 'hAA01); + assert(s1.ir.u.opcode == 'h37); + assert(s1.ir.r.opcode == 'h37); + assert(s1.ir.u.rd == 'd29); + assert(s1.ir.r.rd == 'd29); + assert(s1.ir.u.imm == 'hAA01); + assert(s1.state == 4'b1111); end union packed { diff --git a/tests/techmap/adff2dff.ys b/tests/techmap/adff2dff.ys index 53f7d2f08..6d03d1963 100644 --- a/tests/techmap/adff2dff.ys +++ b/tests/techmap/adff2dff.ys @@ -16,4 +16,4 @@ EOT proc -equiv_opt -async2sync techmap -map +/adff2dff.v +#equiv_opt -assert -async2sync techmap -map +/adff2dff.v diff --git a/tests/techmap/bmuxmap_pmux.ys b/tests/techmap/bmuxmap_pmux.ys new file mode 100644 index 000000000..c75d981e7 --- /dev/null +++ b/tests/techmap/bmuxmap_pmux.ys @@ -0,0 +1,45 @@ +read_ilang << EOT + +module \top + wire width 4 input 0 \S + wire width 5 output 1 \Y + + cell $bmux $0 + parameter \WIDTH 5 + parameter \S_WIDTH 4 + connect \A 80'10110100011101110001110010001110101010111000110011111111111110100000110100111000 + connect \S \S + connect \Y \Y + end +end + +EOT + +hierarchy -auto-top +equiv_opt -assert bmuxmap -pmux + +### +design -reset + +read_ilang << EOT + +module \top + wire width 10 input 0 \A + wire input 1 \S + wire width 5 output 2 \Y + + cell $bmux $0 + parameter \WIDTH 5 + parameter \S_WIDTH 1 + connect \A \A + connect \S \S + connect \Y \Y + end +end + +EOT + +hierarchy -auto-top +equiv_opt -assert bmuxmap -pmux + + diff --git a/tests/techmap/dff2ff.ys b/tests/techmap/dff2ff.ys index 5adf14b07..6e7e6082b 100644 --- a/tests/techmap/dff2ff.ys +++ b/tests/techmap/dff2ff.ys @@ -13,4 +13,4 @@ EOT proc -equiv_opt techmap -map +/dff2ff.v +equiv_opt -assert techmap -map +/dff2ff.v diff --git a/tests/techmap/dfflegalize_adlatch.ys b/tests/techmap/dfflegalize_adlatch.ys index b242cc809..559363301 100644 --- a/tests/techmap/dfflegalize_adlatch.ys +++ b/tests/techmap/dfflegalize_adlatch.ys @@ -12,7 +12,7 @@ $_DLATCH_PN1_ ff1 (.E(E), .R(R), .D(D), .Q(Q[1])); $_DLATCH_NP1_ ff2 (.E(E), .R(R), .D(D), .Q(Q[2])); endmodule -module top(input C, E, R, D, output [13:0] Q); +module top(input C, E, R, D, output [5:0] Q); adlatch0 adlatch0_(.E(E), .R(R), .D(D), .Q(Q[2:0])); adlatch1 adlatch1_(.E(E), .R(R), .D(D), .Q(Q[5:3])); endmodule diff --git a/tests/techmap/dfflegalize_adlatch_init.ys b/tests/techmap/dfflegalize_adlatch_init.ys index a55082d1d..8e371c528 100644 --- a/tests/techmap/dfflegalize_adlatch_init.ys +++ b/tests/techmap/dfflegalize_adlatch_init.ys @@ -12,7 +12,7 @@ $_DLATCH_PN1_ ff1 (.E(E), .R(R), .D(D), .Q(Q[1])); $_DLATCH_NP1_ ff2 (.E(E), .R(R), .D(D), .Q(Q[2])); endmodule -module top(input C, E, R, D, output [13:0] Q); +module top(input C, E, R, D, output [5:0] Q); adlatch0 adlatch0_(.E(E), .R(R), .D(D), .Q(Q[2:0])); adlatch1 adlatch1_(.E(E), .R(R), .D(D), .Q(Q[5:3])); endmodule diff --git a/tests/techmap/dfflegalize_aldff.ys b/tests/techmap/dfflegalize_aldff.ys index 1ee9e3af6..5be3e9742 100644 --- a/tests/techmap/dfflegalize_aldff.ys +++ b/tests/techmap/dfflegalize_aldff.ys @@ -24,8 +24,8 @@ design -save orig flatten equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ x equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ x -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ x -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ x +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ x +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ x # Convert everything to ALDFFs. diff --git a/tests/techmap/dfflegalize_aldff_init.ys b/tests/techmap/dfflegalize_aldff_init.ys index f4db8dd32..ffa7cbf16 100644 --- a/tests/techmap/dfflegalize_aldff_init.ys +++ b/tests/techmap/dfflegalize_aldff_init.ys @@ -26,10 +26,10 @@ equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 # Convert everything to ALDFFs. diff --git a/tests/techmap/dfflegalize_dffsr_init.ys b/tests/techmap/dfflegalize_dffsr_init.ys index ce5a32f76..b6160bb87 100644 --- a/tests/techmap/dfflegalize_dffsr_init.ys +++ b/tests/techmap/dfflegalize_dffsr_init.ys @@ -41,18 +41,18 @@ EOT design -save orig flatten -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 # Convert everything to ADFFs. diff --git a/tests/techmap/dfflegalize_dlatchsr_init.ys b/tests/techmap/dfflegalize_dlatchsr_init.ys index b38a9eb3b..da4ca164e 100644 --- a/tests/techmap/dfflegalize_dlatchsr_init.ys +++ b/tests/techmap/dfflegalize_dlatchsr_init.ys @@ -14,7 +14,7 @@ $_DLATCHSR_PNP_ ff2 (.E(E), .R(R), .S(S), .D(D), .Q(Q[2])); $_DLATCHSR_NPP_ ff3 (.E(E), .R(R), .S(S), .D(D), .Q(Q[3])); endmodule -module top(input C, E, R, S, D, output [17:0] Q); +module top(input C, E, R, S, D, output [7:0] Q); dlatchsr0 dlatchsr0_(.E(E), .R(R), .S(S), .D(D), .Q(Q[3:0])); dlatchsr1 dlatchsr1_(.E(E), .R(R), .S(S), .D(D), .Q(Q[7:4])); endmodule @@ -23,12 +23,12 @@ EOT design -save orig flatten -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 # Convert everything to ADLATCHs. diff --git a/tests/techmap/dfflegalize_sr_init.ys b/tests/techmap/dfflegalize_sr_init.ys index 9d724de29..7cb1c629d 100644 --- a/tests/techmap/dfflegalize_sr_init.ys +++ b/tests/techmap/dfflegalize_sr_init.ys @@ -21,18 +21,18 @@ EOT design -save orig flatten -#equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 # Convert everything to SRs. diff --git a/tests/techmap/dfflibmap.ys b/tests/techmap/dfflibmap.ys index 04477eb14..b0a7d6b7e 100644 --- a/tests/techmap/dfflibmap.ys +++ b/tests/techmap/dfflibmap.ys @@ -17,9 +17,11 @@ EOT simplemap design -save orig +read_liberty -lib dfflibmap.lib + +equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib +equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib -#equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib -#equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib dfflibmap -prepare -liberty dfflibmap.lib equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dfflibmap.lib diff --git a/tests/techmap/dffunmap.ys b/tests/techmap/dffunmap.ys index b813078ee..247699f80 100644 --- a/tests/techmap/dffunmap.ys +++ b/tests/techmap/dffunmap.ys @@ -4,7 +4,7 @@ module top(...); input C, R, E, S; input [1:0] D; -output [20:0] Q; +output [17:0] Q; $dff #(.CLK_POLARITY(1'b0), .WIDTH(2)) ff0 (.CLK(C), .D(D), .Q(Q[1:0])); $dffe #(.CLK_POLARITY(1'b0), .EN_POLARITY(1'b0), .WIDTH(2)) ff1 (.CLK(C), .EN(E), .D(D), .Q(Q[3:2])); diff --git a/tests/techmap/pmux2mux.ys b/tests/techmap/pmux2mux.ys index 1714a6b87..1e08485ef 100644 --- a/tests/techmap/pmux2mux.ys +++ b/tests/techmap/pmux2mux.ys @@ -12,4 +12,4 @@ output [3:0] O; endmodule EOT -equiv_opt techmap -map +/pmux2mux.v +equiv_opt -assert techmap -map +/pmux2mux.v diff --git a/tests/techmap/shiftx2mux.ys b/tests/techmap/shiftx2mux.ys index f749e79b2..680681297 100644 --- a/tests/techmap/shiftx2mux.ys +++ b/tests/techmap/shiftx2mux.ys @@ -106,4 +106,4 @@ endmodule EOT opt wreduce -equiv_opt techmap +equiv_opt -assert techmap diff --git a/tests/techmap/zinit.ys b/tests/techmap/zinit.ys index bc07f40e6..562db0776 100644 --- a/tests/techmap/zinit.ys +++ b/tests/techmap/zinit.ys @@ -13,6 +13,8 @@ $_DFF_PN1_ dff5 (.C(C), .D(D[0]), .R(R), .Q(Q[5])); $_DFF_PP0_ dff6 (.C(C), .D(D[0]), .R(R), .Q(Q[6])); $_DFF_PP1_ dff7 (.C(C), .D(D[0]), .R(R), .Q(Q[7])); +assign Q[8] = 0; + $adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) dff8 (.CLK(C), .ARST(R), .D(D), .Q(Q[10:9])); $adff #(.WIDTH(2), .CLK_POLARITY(0), .ARST_POLARITY(1'b1), .ARST_VALUE(2'b01)) dff9 (.CLK(C), .ARST(R), .D(D), .Q(Q[12:11])); endmodule @@ -44,6 +46,8 @@ $_DFF_PN1_ dff5 (.C(C), .D(D[0]), .R(R), .Q(Q[5])); $_DFF_PP0_ dff6 (.C(C), .D(D[0]), .R(R), .Q(Q[6])); $_DFF_PP1_ dff7 (.C(C), .D(D[0]), .R(R), .Q(Q[7])); +assign Q[8] = 0; + $adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) dff8 (.CLK(C), .ARST(R), .D(D), .Q(Q[10:9])); $adff #(.WIDTH(2), .CLK_POLARITY(0), .ARST_POLARITY(1'b1), .ARST_VALUE(2'b01)) dff9 (.CLK(C), .ARST(R), .D(D), .Q(Q[12:11])); endmodule @@ -91,9 +95,8 @@ $_SDFFE_PP1P_ dff23(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[23])); endmodule EOT -#equiv_opt -assert -multiclock zinit -#design -load postopt -zinit +equiv_opt -assert -multiclock zinit +design -load postopt select -assert-count 48 t:$_NOT_ select -assert-count 0 w:Q a:init %i @@ -138,9 +141,8 @@ $_SDFFE_PP1P_ dff23(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[23])); endmodule EOT -#equiv_opt -assert -multiclock zinit -#design -load postopt -zinit +equiv_opt -assert -multiclock zinit +design -load postopt select -assert-count 0 t:$_NOT_ select -assert-count 1 w:Q a:init=24'b0 %i diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh index e4aef9917..f96eb8d71 100755 --- a/tests/tools/autotest.sh +++ b/tests/tools/autotest.sh @@ -1,6 +1,6 @@ #!/usr/bin/env bash -libs="" +libs=() genvcd=false use_xsim=false use_modelsim=false @@ -15,7 +15,7 @@ xinclude_opts="" minclude_opts="" scriptfiles="" scriptopt="" -toolsdir="$(cd $(dirname $0); pwd)" +toolsdir="$(cd "$(dirname "$0")"; pwd)" warn_iverilog_git=false # The following are used in verilog to firrtl regression tests. # Typically these will be passed as environment variables: @@ -25,8 +25,8 @@ firrtl2verilog="" xfirrtl="../xfirrtl" abcprog="$toolsdir/../../yosys-abc" -if [ ! -f $toolsdir/cmp_tbdata -o $toolsdir/cmp_tbdata.c -nt $toolsdir/cmp_tbdata ]; then - ( set -ex; ${CC:-gcc} -Wall -o $toolsdir/cmp_tbdata $toolsdir/cmp_tbdata.c; ) || exit 1 +if [ ! -f "$toolsdir/cmp_tbdata" -o "$toolsdir/cmp_tbdata.c" -nt "$toolsdir/cmp_tbdata" ]; then + ( set -ex; ${CC:-gcc} -Wall -o "$toolsdir/cmp_tbdata" "$toolsdir/cmp_tbdata.c"; ) || exit 1 fi while getopts xmGl:wkjvref:s:p:n:S:I:A:-: opt; do @@ -38,7 +38,7 @@ while getopts xmGl:wkjvref:s:p:n:S:I:A:-: opt; do G) warn_iverilog_git=true ;; l) - libs="$libs $(cd $(dirname $OPTARG); pwd)/$(basename $OPTARG)";; + libs+=("$(cd "$(dirname "$OPTARG")"; pwd)/$(basename "$OPTARG")");; w) genvcd=true ;; k) @@ -162,7 +162,7 @@ do cp ../${bn}_tb.v ${bn}_tb.v fi if $genvcd; then sed -i 's,// \$dump,$dump,g' ${bn}_tb.v; fi - compile_and_run ${bn}_tb_ref ${bn}_out_ref ${bn}_tb.v ${bn}_ref.${refext} $libs \ + compile_and_run ${bn}_tb_ref ${bn}_out_ref ${bn}_tb.v ${bn}_ref.${refext} "${libs[@]}" \ "$toolsdir"/../../techlibs/common/simlib.v \ "$toolsdir"/../../techlibs/common/simcells.v if $genvcd; then mv testbench.vcd ${bn}_ref.vcd; fi @@ -171,11 +171,11 @@ do test_passes() { "$toolsdir"/../../yosys -b "verilog $backend_opts" -o ${bn}_syn${test_count}.v "$@" compile_and_run ${bn}_tb_syn${test_count} ${bn}_out_syn${test_count} \ - ${bn}_tb.v ${bn}_syn${test_count}.v $libs \ + ${bn}_tb.v ${bn}_syn${test_count}.v "${libs[@]}" \ "$toolsdir"/../../techlibs/common/simlib.v \ "$toolsdir"/../../techlibs/common/simcells.v if $genvcd; then mv testbench.vcd ${bn}_syn${test_count}.vcd; fi - $toolsdir/cmp_tbdata ${bn}_out_ref ${bn}_out_syn${test_count} + "$toolsdir/cmp_tbdata" ${bn}_out_ref ${bn}_out_syn${test_count} test_count=$(( test_count + 1 )) } diff --git a/tests/various/aiger_dff.ys b/tests/various/aiger_dff.ys new file mode 100644 index 000000000..057f3d774 --- /dev/null +++ b/tests/various/aiger_dff.ys @@ -0,0 +1,7 @@ +read_verilog -icells <<EOT +module top(input clk, d, output q); +\$_DFF_N_ dffn(.C(clk), .D(d), .Q(q)); +endmodule +EOT +write_aiger -zinit -ywmap aiger_dff.out /dev/null +!grep -qF negedge aiger_dff.out diff --git a/tests/various/bug3462.ys b/tests/various/bug3462.ys new file mode 100644 index 000000000..c85dc9470 --- /dev/null +++ b/tests/various/bug3462.ys @@ -0,0 +1,12 @@ +read_verilog <<EOT +module top(); + wire array[0:0]; + wire out; + sub #(.d(1)) inst( + .in(array[0]), + .out(out) + ); +endmodule +EOT + +hierarchy -top top -libdir . diff --git a/tests/various/cellarray_array_connections.ys b/tests/various/cellarray_array_connections.ys new file mode 100644 index 000000000..ef36a9a45 --- /dev/null +++ b/tests/various/cellarray_array_connections.ys @@ -0,0 +1,45 @@ +# Regression test for #3467 +read_verilog <<EOT + +module bit_buf ( + input wire bit_in, + output wire bit_out +); + assign bit_out = bit_in; +endmodule + +module top ( + input wire [3:0] data_in, + output wire [3:0] data_out +); + + wire [3:0] data [0:4]; + + assign data[0] = data_in; + assign data_out = data[4]; + + genvar i; + generate + for (i=0; i<=3; i=i+1) begin + bit_buf bit_buf_instance[3:0] ( + .bit_in(data[i]), + .bit_out(data[i + 1]) + ); + end + endgenerate +endmodule + +module top2 ( + input wire [3:0] data_in, + output wire [3:0] data_out +); + assign data_out = data_in; +endmodule + +EOT + +hierarchy +proc + +miter -equiv -make_assert -flatten top top2 miter +sat -prove-asserts -verify miter diff --git a/tests/various/equiv_make_make_assert.ys b/tests/various/equiv_make_make_assert.ys new file mode 100644 index 000000000..1c2efa723 --- /dev/null +++ b/tests/various/equiv_make_make_assert.ys @@ -0,0 +1,32 @@ +read_verilog <<EOT +module gold( + input wire [7:0] a, + input wire [7:0] b, + output wire [7:0] c +); + +wire [7:0] b_neg; +assign b_neg = -b; +assign c = a + b_neg; +endmodule + +module gate( + input wire [7:0] a, + input wire [7:0] b, + output wire [7:0] c +); + +wire [7:0] b_neg; +assign b_neg = ~b + 1; +assign c = a + b_neg; +endmodule + +EOT + +equiv_make -make_assert gold gate miter + +select -assert-count 0 t:$equiv +select -assert-count 2 t:$assert + +prep -top miter +sat -prove-asserts -verify diff --git a/tests/various/rename_scramble_name.ys b/tests/various/rename_scramble_name.ys new file mode 100644 index 000000000..9a36d0922 --- /dev/null +++ b/tests/various/rename_scramble_name.ys @@ -0,0 +1,31 @@ +read_verilog <<EOF +module top(); + wire a, b, c; +endmodule +EOF + +proc +hierarchy -top top +rename -seed 2 -scramble-name w:* +select -assert-none w:a w:b w:c +select -assert-count 3 w:$_*_ +select -assert-none w:$_*_ %% %n +design -reset + +read_verilog <<EOF +module foo(input a, b, output c); + assign c = a + b; +endmodule + +module top(); + wire a, b, c; + foo bar(.a(a), .b(b), .c(c)); +endmodule +EOF + +proc +hierarchy -top top +rename -seed 2 -scramble-name c:bar +select -assert-none c:bar +select -assert-count 1 c:$_*_ +select -assert-none c:$_*_ w:* foo/c:$add$<<EOF:2$1 %% %n diff --git a/tests/various/rtlil_z_bits.ys b/tests/various/rtlil_z_bits.ys new file mode 100644 index 000000000..c38669159 --- /dev/null +++ b/tests/various/rtlil_z_bits.ys @@ -0,0 +1,9 @@ +! mkdir -p temp +read_rtlil <<EOT +module \test + wire output 1 \a + connect \a 1'z +end +EOT +write_rtlil temp/rtlil_z_bits.il +! grep -F -q "connect \\a 1'z" temp/rtlil_z_bits.il diff --git a/tests/various/smtlib2_module-expected.smt2 b/tests/various/smtlib2_module-expected.smt2 index ace858ca8..494e7cda0 100644 --- a/tests/various/smtlib2_module-expected.smt2 +++ b/tests/various/smtlib2_module-expected.smt2 @@ -4,11 +4,14 @@ (declare-fun |smtlib2_is| (|smtlib2_s|) Bool) (declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a ; yosys-smt2-input a 8 +; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "smtoffset": 0, "type": "input", "width": 8} (define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state)) (declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b ; yosys-smt2-input b 8 +; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "smtoffset": 0, "type": "input", "width": 8} (define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state)) ; yosys-smt2-output add 8 +; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "smtoffset": 0, "type": "blackbox", "width": 8} (define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let ( (|a| (|smtlib2_n a| state)) (|b| (|smtlib2_n b| state)) @@ -16,6 +19,7 @@ (bvadd a b) )) ; yosys-smt2-output eq 1 +; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "smtoffset": 0, "type": "blackbox", "width": 1} (define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let ( (|a| (|smtlib2_n a| state)) (|b| (|smtlib2_n b| state)) @@ -23,6 +27,7 @@ (= a b) )) ; yosys-smt2-output sub 8 +; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "smtoffset": 0, "type": "blackbox", "width": 8} (define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let ( (|a| (|smtlib2_n a| state)) (|b| (|smtlib2_n b| state)) @@ -38,13 +43,16 @@ (declare-sort |uut_s| 0) (declare-fun |uut_is| (|uut_s|) Bool) ; yosys-smt2-cell smtlib2 s +; yosys-smt2-witness {"path": ["\\s"], "smtname": "s", "type": "cell"} (declare-fun |uut#0| (|uut_s|) (_ BitVec 8)) ; \add (declare-fun |uut#1| (|uut_s|) Bool) ; \eq (declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub (declare-fun |uut_h s| (|uut_s|) |smtlib2_s|) ; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26 +; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "smtoffset": 0, "type": "init", "width": 8} (declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a ; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41 +; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "smtoffset": 0, "type": "init", "width": 8} (declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b (define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2 (define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9 diff --git a/tests/various/sub.v b/tests/various/sub.v new file mode 100644 index 000000000..63422ca5c --- /dev/null +++ b/tests/various/sub.v @@ -0,0 +1,3 @@ +module sub #(parameter d=1) (input in, output out); + assign out = in; +endmodule diff --git a/tests/xprop/.gitignore b/tests/xprop/.gitignore new file mode 100644 index 000000000..ff0b65b54 --- /dev/null +++ b/tests/xprop/.gitignore @@ -0,0 +1,2 @@ +/xprop_* +/run-test.mk diff --git a/tests/xprop/generate.py b/tests/xprop/generate.py new file mode 100644 index 000000000..484f1661c --- /dev/null +++ b/tests/xprop/generate.py @@ -0,0 +1,287 @@ +import os +import re +import sys +import random +import argparse + +parser = argparse.ArgumentParser(formatter_class=argparse.ArgumentDefaultsHelpFormatter) +parser.add_argument('-S', '--seed', type=int, help='seed for PRNG') +parser.add_argument('-m', '--more', action='store_true', help='run more tests') +parser.add_argument('-c', '--count', type=int, default=32, help='number of random patterns to test') +parser.add_argument('-f', '--filter', default='', help='regular expression to filter tests to generate') +args = parser.parse_args() + +if args.seed is None: + args.seed = random.randrange(1 << 32) + +print(f"xprop PRNG seed: {args.seed}") + +makefile = open("run-test.mk", "w") + +def add_test(name, src, seq=False): + if not re.search(args.filter, name): + return + workdir = f"xprop_{name}" + + os.makedirs(workdir, exist_ok=True) + with open(f"{workdir}/uut.v", "w") as uut: + print(src, file=uut) + print(f"all: {workdir}", file=makefile) + print(f".PHONY: {workdir}", file=makefile) + print(f"{workdir}:", file=makefile) + seq_arg = " -s" if seq else "" + print( + f"\t@cd {workdir} && python3 -u ../test.py -S {args.seed} -c {args.count}{seq_arg} > test.log 2>&1 || echo {workdir}: failed > status\n" + f"\t@cat {workdir}/status\n" + f"\t@grep '^.*: ok' {workdir}/status\n" + , + file=makefile, + ) + +def cell_test(name, cell, inputs, outputs, params, initial={}, defclock=False, seq=False): + ports = [] + port_conns = [] + for inport, width in inputs.items(): + ports.append(f"input [{width-1}:0] {inport}") + if defclock and inport in ["C", "CLK"]: + port_conns.append(f".{inport}({inport} !== 0)") + else: + port_conns.append(f".{inport}({inport})") + for outport, width in outputs.items(): + reg = " reg" if outport in initial else "" + ports.append(f"output{reg} [{width-1}:0] {outport}") + port_conns.append(f".{outport}({outport})") + param_defs = [] + for param, value in params.items(): + param_defs.append(f".{param}({value})") + initials = [] + # for port, value in initial.items(): + # initials.append(f"initial {port} = {value};\n") + add_test(name, + f"module uut({', '.join(ports)});\n" + f"\\${cell} #({', '.join(param_defs)}) cell ({', '.join(port_conns)});\n" + f"{''.join(initials)}" + "endmodule", + seq=seq, + ) + +def unary_test(cell, width, signed, out_width): + add_test( + f"{cell}_{width}{'us'[signed]}_{out_width}", + f"module uut(input [{width-1}:0] A, output [{out_width}-1:0] Y);\n" + f"\\${cell} #(.A_WIDTH({width}), .A_SIGNED({int(signed)}), .Y_WIDTH({out_width}))" + " cell (.A(A), .Y(Y));\n" + "endmodule", + ) + +def binary_test(cell, a_width, b_width, signed, out_width): + add_test( + f"{cell}_{a_width}{'us'[signed]}{b_width}_{out_width}", + f"module uut(input [{a_width-1}:0] A, input [{b_width-1}:0] B, output [{out_width}-1:0] Y);\n" + f"\\${cell} #(.A_WIDTH({a_width}), .A_SIGNED({int(signed)}), .B_WIDTH({b_width}), .B_SIGNED({int(signed)}), .Y_WIDTH({out_width}))" + " cell (.A(A), .B(B), .Y(Y));\n" + "endmodule", + ) + +def shift_test(cell, a_width, b_width, a_signed, b_signed, out_width): + add_test( + f"{cell}_{a_width}{'us'[a_signed]}{b_width}{'us'[b_signed]}_{out_width}", + f"module uut(input [{a_width-1}:0] A, input [{b_width-1}:0] B, output [{out_width}-1:0] Y);\n" + f"\\${cell} #(.A_WIDTH({a_width}), .A_SIGNED({int(a_signed)}), .B_WIDTH({b_width}), .B_SIGNED({int(b_signed)}), .Y_WIDTH({out_width}))" + " cell (.A(A), .B(B), .Y(Y));\n" + "endmodule", + ) + +def mux_test(width): + cell_test(f"mux_{width}", 'mux', {"A": width, "B": width, "S": 1}, {"Y": width}, {"WIDTH": width}) + +def bmux_test(width, s_width): + cell_test(f"bmux_{width}_{s_width}", 'bmux', {"A": width << s_width, "S": s_width}, {"Y": width}, {"WIDTH": width, "S_WIDTH": s_width}) + +def demux_test(width, s_width): + cell_test(f"demux_{width}_{s_width}", 'demux', {"A": width, "S": s_width}, {"Y": width << s_width}, {"WIDTH": width, "S_WIDTH": s_width}) + +def pmux_test(width, s_width): + cell_test(f"pmux_{width}_{s_width}", 'pmux', {"A": width, "B": width * s_width, "S": s_width}, {"Y": width}, {"WIDTH": width, "S_WIDTH": s_width}) + +def bwmux_test(width): + cell_test(f"bwmux_{width}", 'bwmux', {"A": width, "B": width, "S": width}, {"Y": width}, {"WIDTH": width}) + +def bweqx_test(width): + cell_test(f"bweqx_{width}", 'bweqx', {"A": width, "B": width}, {"Y": width}, {"WIDTH": width}) + +def ff_test(width): + cell_test(f"ff_{width}", 'ff', {"D": width}, {"Q": width}, {"WIDTH": width}, seq=True) + +def dff_test(width, pol, defclock): + cell_test(f"dff_{width}{'np'[pol]}{'xd'[defclock]}", 'dff', {"CLK": 1, "D": width}, {"Q": width}, {"WIDTH": width, "CLK_POLARITY": int(pol)}, defclock=defclock, seq=True) + +def dffe_test(width, pol, enpol, defclock): + cell_test(f"dffe_{width}{'np'[pol]}{'np'[enpol]}{'xd'[defclock]}", 'dffe', {"CLK": 1, "EN": 1, "D": width}, {"Q": width}, {"WIDTH": width, "CLK_POLARITY": int(pol), "EN_POLARITY": int(enpol)}, defclock=defclock, seq=True) + + +print(".PHONY: all", file=makefile) +print("all:\n\t@echo done\n", file=makefile) + +for cell in ["not", "pos", "neg"]: + if args.more: + unary_test(cell, 1, False, 1) + unary_test(cell, 3, False, 3) + unary_test(cell, 3, True, 3) + unary_test(cell, 3, True, 1) + unary_test(cell, 3, False, 5) + unary_test(cell, 3, True, 5) + +for cell in ["and", "or", "xor", "xnor"]: + binary_test(cell, 1, 1, False, 1) + binary_test(cell, 1, 1, True, 2) + binary_test(cell, 2, 2, False, 2) + if args.more: + binary_test(cell, 2, 2, False, 1) + binary_test(cell, 2, 1, False, 2) + binary_test(cell, 2, 1, False, 1) + +# [, "pow"] are not implemented yet +for cell in ["add", "sub", "mul", "div", "mod", "divfloor", "modfloor"]: + if args.more: + binary_test(cell, 1, 1, False, 1) + binary_test(cell, 1, 1, False, 2) + binary_test(cell, 3, 3, False, 1) + binary_test(cell, 3, 3, False, 3) + binary_test(cell, 3, 3, False, 6) + binary_test(cell, 3, 3, True, 1) + binary_test(cell, 3, 3, True, 3) + binary_test(cell, 3, 3, True, 6) + binary_test(cell, 5, 3, False, 3) + binary_test(cell, 5, 3, True, 3) + +for cell in ["lt", "le", "eq", "ne", "eqx", "nex", "ge", "gt"]: + if args.more: + binary_test(cell, 1, 1, False, 1) + binary_test(cell, 1, 1, False, 2) + binary_test(cell, 3, 3, False, 1) + binary_test(cell, 3, 3, False, 2) + binary_test(cell, 3, 3, True, 1) + binary_test(cell, 3, 3, True, 2) + binary_test(cell, 5, 3, False, 1) + binary_test(cell, 5, 3, True, 1) + binary_test(cell, 5, 3, False, 2) + binary_test(cell, 5, 3, True, 2) + +for cell in ["reduce_and", "reduce_or", "reduce_xor", "reduce_xnor"]: + if args.more: + unary_test(cell, 1, False, 1) + unary_test(cell, 3, False, 1) + unary_test(cell, 3, True, 1) + unary_test(cell, 3, False, 3) + unary_test(cell, 3, True, 3) + +for cell in ["reduce_bool", "logic_not"]: + unary_test(cell, 1, False, 1) + unary_test(cell, 3, False, 3) + unary_test(cell, 3, True, 3) + unary_test(cell, 3, True, 1) + +for cell in ["logic_and", "logic_or"]: + binary_test(cell, 1, 1, False, 1) + binary_test(cell, 3, 3, False, 3) + binary_test(cell, 3, 3, True, 3) + binary_test(cell, 3, 3, True, 1) + +for cell in ["shl", "shr", "sshl", "sshr", "shift"]: + if args.more: + shift_test(cell, 2, 1, False, False, 2) + shift_test(cell, 2, 1, True, False, 2) + shift_test(cell, 2, 1, False, False, 4) + shift_test(cell, 2, 1, True, False, 4) + shift_test(cell, 4, 2, False, False, 4) + shift_test(cell, 4, 2, True, False, 4) + shift_test(cell, 4, 2, False, False, 8) + shift_test(cell, 4, 2, True, False, 8) + shift_test(cell, 4, 3, False, False, 3) + shift_test(cell, 4, 3, True, False, 3) + +for cell in ["shift"]: + if args.more: + shift_test(cell, 2, 1, False, True, 2) + shift_test(cell, 2, 1, True, True, 2) + shift_test(cell, 2, 1, False, True, 4) + shift_test(cell, 2, 1, True, True, 4) + shift_test(cell, 4, 2, False, True, 4) + shift_test(cell, 4, 2, True, True, 4) + shift_test(cell, 4, 2, False, True, 8) + shift_test(cell, 4, 2, True, True, 8) + shift_test(cell, 4, 3, False, True, 3) + shift_test(cell, 4, 3, True, True, 3) + +for cell in ["shiftx"]: + if args.more: + shift_test(cell, 2, 1, False, True, 2) + shift_test(cell, 2, 1, False, True, 4) + shift_test(cell, 4, 2, False, True, 4) + shift_test(cell, 4, 2, False, True, 8) + shift_test(cell, 4, 3, False, True, 3) + +mux_test(1) +mux_test(3) + +bmux_test(1, 2) +bmux_test(2, 2) +bmux_test(3, 1) + +demux_test(1, 2) +demux_test(2, 2) +demux_test(3, 1) + +pmux_test(1, 4) +pmux_test(2, 2) +pmux_test(3, 1) +pmux_test(4, 4) + +bwmux_test(1) +bwmux_test(3) + +bweqx_test(1) +bweqx_test(3) + +ff_test(1) +ff_test(3) + +dff_test(1, True, True) +dff_test(1, False, True) +dff_test(3, True, True) +dff_test(3, False, True) + +# dff_test(1, True, False) # TODO support x clocks +# dff_test(1, False, False) # TODO support x clocks +# dff_test(3, True, False) # TODO support x clocks +# dff_test(3, False, False) # TODO support x clocks + +dffe_test(1, True, False, True) +dffe_test(1, False, False, True) +dffe_test(3, True, False, True) +dffe_test(3, False, False, True) +dffe_test(1, True, True, True) +dffe_test(1, False, True, True) +dffe_test(3, True, True, True) +dffe_test(3, False, True, True) + + + +# TODO "shift", "shiftx" + +# TODO "fa", "lcu", "alu", "macc", "lut", "sop" + +# TODO "slice", "concat" + +# TODO "tribuf", "specify2", "specify3", "specrule" + +# TODO "assert", "assume", "live", "fair", "cover", "initstate", "anyconst", "anyseq", "anyinit", "allconst", "allseq", "equiv", + +# TODO "bweqx", "bwmux" + +# TODO "sr", "ff", "dff", "dffe", "dffsr", "sffsre", "adff", "aldff", "sdff", "adffe", "aldffe", "sdffe", "sdffce", "dlatch", "adlatch", "dlatchsr" + +# TODO "fsm" + +# TODO "memrd", "memrd_v2", "memwr", "memwr_v2", "meminit", "meminit_v2", "mem", "mem_v2" diff --git a/tests/xprop/run-test.sh b/tests/xprop/run-test.sh new file mode 100755 index 000000000..db4b7ca82 --- /dev/null +++ b/tests/xprop/run-test.sh @@ -0,0 +1,5 @@ +#!/bin/bash +set -e + +python3 generate.py $@ +${MAKE:-make} -f run-test.mk diff --git a/tests/xprop/test.py b/tests/xprop/test.py new file mode 100644 index 000000000..a275b0d93 --- /dev/null +++ b/tests/xprop/test.py @@ -0,0 +1,516 @@ +import os +import re +import subprocess +import itertools +import random +import argparse +from pathlib import Path + +parser = argparse.ArgumentParser(formatter_class=argparse.ArgumentDefaultsHelpFormatter) +parser.add_argument('-S', '--seed', type=int, help='seed for PRNG') +parser.add_argument('-c', '--count', type=int, default=32, help='number of random patterns to test') +parser.add_argument('-s', '--seq', action='store_true', help='run a sequential test') +parser.add_argument('steps', nargs='*', help='steps to run') +args = parser.parse_args() + +if args.seed is None: + args.seed = random.randrange(1 << 32) + +print(f"PRNG seed: {args.seed}") +random.seed(args.seed) + +steps = args.steps + +all_outputs = [ + "sim", + "sim_xprop", + "vsim_expr", + "vsim_expr_xprop", + "vsim_noexpr", + "vsim_noexpr_xprop", + "sat", + "sat_xprop", +] + +if not args.seq: + all_outputs += ["opt_expr", "opt_expr_xprop"] + +if not steps: + steps = ["clean", "prepare", "verify", *all_outputs, "compare"] + +if "clean" in steps: + for output in all_outputs: + try: + os.unlink(f"{output}.out") + except FileNotFoundError: + pass + + +def yosys(command): + subprocess.check_call(["../../../yosys", "-Qp", command]) + +def remove(file): + try: + os.unlink(file) + except FileNotFoundError: + pass + + +def vcdextract(signals, on_change, file, output, limit=None): + scope = [] + ids = {} + prefix = [] + + for line in file: + line = prefix + line.split() + if line[-1] != "$end": + prefix = line + continue + prefix = [] + + if not line: + continue + if line[0] == "$scope": + scope.append(line[2].lstrip("\\")) + elif line[0] == "$upscope": + scope.pop() + elif line[0] == "$var": + ids[".".join(scope + [line[4].lstrip("\\")])] = line[3] + elif line[0] == "$enddefinitions": + break + elif line[0] in ["$version", "$date", "$comment"]: + continue + else: + raise RuntimeError(f"unexpected input in vcd {line}") + + dump_pos = {} + + for i, sig in enumerate(signals + on_change): + dump_pos[ids[sig]] = i + + values = [None] * len(signals + on_change) + + last_values = [] + + counter = 0 + + for line in file: + if line.startswith("#"): + if None in values: + continue + + if values != last_values: + last_values = list(values) + if limit is None or counter < limit: + print(*values[:len(signals)], file=output) + counter += 1 + continue + + if line.startswith("b"): + value, id = line[1:].split() + else: + value, id = line[:1], line[1:] + + pos = dump_pos.get(id) + if pos is None: + continue + + values[pos] = value + + if values != last_values: + if limit is None or counter < limit: + print(*values[:len(signals)], file=output) + + +share = Path(__file__).parent / ".." / ".." / "share" + +simlibs = [str(share / "simlib.v"), str(share / "simcells.v")] + +if "prepare" in steps: + yosys( + """ + read_verilog -icells uut.v + hierarchy -top uut; proc -noopt + write_rtlil uut.il + dump -o ports.list uut/x:* + """ + ) + +inputs = [] +outputs = [] + +with open("ports.list") as ports_file: + for line in ports_file: + line = line.split() + if not line or line[0] != "wire": + continue + line = line[1:] + width = 1 + if line[0] == "width": + width = int(line[1]) + line = line[2:] + direction, seq, name = line + assert name.startswith("\\") + name = name[1:] + seq = int(seq) + + if direction == "input": + inputs.append((seq, name, width)) + else: + outputs.append((seq, name, width)) + +inputs.sort() +outputs.sort() + +input_width = sum(width for seq, name, width in inputs) +output_width = sum(width for seq, name, width in outputs) + +if "prepare" in steps: + if args.seq: + patterns = [''.join(random.choices('01x', k=input_width)) for i in range(args.count)] + else: + if 3**input_width <= args.count * 2: + patterns = ["".join(bits) for bits in itertools.product(*["01x"] * input_width)] + else: + patterns = set() + + for bit in '01x': + patterns.add(bit * input_width) + + for bits in itertools.combinations('01x', 2): + for bit1, bit2 in itertools.permutations(bits): + for i in range(input_width): + pattern = [bit1] * input_width + pattern[i] = bit2 + patterns.add(''.join(pattern)) + + for i, j in itertools.combinations(range(input_width), 2): + pattern = [bit1] * input_width + pattern[i] = bit2 + pattern[j] = bit2 + patterns.add(''.join(pattern)) + + for bit1, bit2, bit3 in itertools.permutations('01x'): + for i, j in itertools.combinations(range(input_width), 2): + pattern = [bit1] * input_width + pattern[i] = bit2 + pattern[j] = bit3 + patterns.add(''.join(pattern)) + + if len(patterns) > args.count // 2: + patterns = sorted(patterns) + random.shuffle(patterns) + patterns = set(patterns[:args.count // 2]) + + while len(patterns) < args.count: + pattern = ''.join(random.choices('01x', k=input_width)) + patterns.add(pattern) + + patterns = sorted(patterns) + with open("patterns.list", "w") as f: + for pattern in patterns: + print(pattern, file=f) +else: + with open("patterns.list") as f: + patterns = [pattern.strip() for pattern in f] + + +if "prepare" in steps: + with open("wrapper.v", "w") as wrapper_file: + print( + "module wrapper(" + f"input [{input_width-1}:0] A, " + f"output [{output_width-1}:0] Y);", + file=wrapper_file, + ) + + connections = [] + pos = 0 + for seq, name, width in inputs: + connections.append(f".{name}(A[{pos+width-1}:{pos}])") + pos += width + pos = 0 + for seq, name, width in outputs: + connections.append(f".{name}(Y[{pos+width-1}:{pos}])") + pos += width + + print(f"uut uut({', '.join(connections)});", file=wrapper_file) + print("endmodule", file=wrapper_file) + + yosys( + """ + read_rtlil uut.il + read_verilog wrapper.v + hierarchy -top wrapper; proc -noopt + flatten; clean; + rename wrapper uut + write_rtlil wrapped.il + """ + ) + + try: + yosys( + """ + read_rtlil wrapped.il + dffunmap + xprop -required + check -assert + write_rtlil wrapped_xprop.il + """ + ) + except subprocess.CalledProcessError: + remove("wrapped_xprop.il") + + with open("verilog_sim_tb.v", "w") as tb_file: + print("module top();", file=tb_file) + print(f"reg gclk;", file=tb_file) + print(f"reg [{input_width-1}:0] A;", file=tb_file) + print(f"wire [{output_width-1}:0] Y;", file=tb_file) + print(f"uut uut(.A(A), .Y(Y));", file=tb_file) + print("initial begin", file=tb_file) + + for pattern in patterns: + print( + f' gclk = 1; #0; A[0] = 1\'b{pattern[-1]}; #0; A = {input_width}\'b{pattern}; #5; gclk = 0; $display("%b %b", A, Y); #5', + file=tb_file, + ) + + print(" $finish(0);", file=tb_file) + print("end", file=tb_file) + print("endmodule", file=tb_file) + + with open("synth_tb.v", "w") as tb_file: + print("module top(input clk);", file=tb_file) + print(f"reg [{len(patterns).bit_length() - 1}:0] counter = 0;", file=tb_file) + print(f"reg [{input_width-1}:0] A;", file=tb_file) + print(f"(* gclk *) reg gclk;", file=tb_file) + print(f"wire [{output_width-1}:0] Y;", file=tb_file) + print(f"uut uut(.A(A), .Y(Y));", file=tb_file) + print(f"always @(posedge gclk) counter <= counter + 1;", file=tb_file) + print(f"always @* case (counter)", file=tb_file) + for i, pattern in enumerate(patterns): + print(f" {i:7} : A = {input_width}'b{pattern};", file=tb_file) + print(f" default : A = {input_width}'b{'x' * input_width};", file=tb_file) + print(f"endcase", file=tb_file) + print("endmodule", file=tb_file) + + with open("const_tb.v", "w") as tb_file: + print("module top();", file=tb_file) + for i, pattern in enumerate(patterns): + print( + f"(* keep *) wire [{output_width-1}:0] Y_{i}; " + f"uut uut_{i}(.A({input_width}'b{pattern}), .Y(Y_{i}));", + file=tb_file, + ) + print("endmodule", file=tb_file) + +if "verify" in steps: + try: + seq_args = " -tempinduct -set-init-undef" if args.seq else "" + yosys( + f""" + read_rtlil wrapped.il + copy uut gold + rename uut gate + design -push-copy + dffunmap + xprop -formal -split-inputs -required -debug-asserts gate + clk2fflogic + sat{seq_args} -enable_undef -set-def-inputs -prove-asserts -verify -show-all gate + design -pop + + dffunmap + xprop -required -assume-encoding gate + miter -equiv -make_assert -flatten gold gate miter + clk2fflogic + sat{seq_args} -enable_undef -set-assumes -prove-asserts -verify -show-all miter + """ + ) + with open("verified", "w") as f: + pass + except subprocess.CalledProcessError: + remove("verified") + + +for mode in ["", "_xprop"]: + if not Path(f"wrapped{mode}.il").is_file(): + for expr in [f"expr{mode}", f"noexpr{mode}"]: + remove(f"vsim_{expr}.out") + continue + + if "prepare" in steps: + yosys( + f""" + read_rtlil wrapped{mode}.il + chformal -remove + dffunmap + write_verilog -noexpr vsim_noexpr{mode}.v + write_verilog -noparallelcase vsim_expr{mode}.v + """ + ) + + for expr in [f"expr{mode}", f"noexpr{mode}"]: + if f"vsim_{expr}" in steps: + subprocess.check_call( + [ + "iverilog", + "-DSIMLIB_FF", + "-DSIMLIB_GLOBAL_CLOCK=top.gclk", + f"-DDUMPFILE=\"vsim_{expr}.vcd\"", + "-o", + f"vsim_{expr}", + "verilog_sim_tb.v", + f"vsim_{expr}.v", + *simlibs, + ] + ) + with open(f"vsim_{expr}.out", "w") as f: + subprocess.check_call(["vvp", f"./vsim_{expr}"], stdout=f) + +for mode in ["", "_xprop"]: + if f"sim{mode}" not in steps: + continue + if not Path(f"wrapped{mode}.il").is_file(): + remove(f"sim{mode}.out") + continue + yosys( + f""" + read_verilog synth_tb.v + read_rtlil wrapped{mode}.il + hierarchy -top top; proc -noopt + dffunmap + sim -clock clk -n {len(patterns) // 2} -vcd sim{mode}.vcd top + """ + ) + + with open(f"sim{mode}.vcd") as fin, open(f"sim{mode}.out", "w") as fout: + vcdextract(["top.A", "top.Y"], ["top.counter"], fin, fout, len(patterns)) + +for mode in ["", "_xprop"]: + if f"sat{mode}" not in steps: + continue + if not Path(f"wrapped{mode}.il").is_file(): + remove(f"sat{mode}.out") + continue + chunk_size = len(patterns) if args.seq else 32 + last_progress = 0 + with open(f"sat{mode}.ys", "w") as ys: + for chunk_start in range(0, len(patterns), chunk_size): + chunk = patterns[chunk_start : chunk_start + chunk_size] + progress = (10 * chunk_start) // len(patterns) + if progress > last_progress: + print(f"log sat {progress}0%", file=ys) + last_progress = progress + + append = "-a" if chunk_start else "-o" + print( + end=f"tee -q {append} sat{mode}.log sat -set-init-undef -seq {len(chunk)}" + " -show A -show Y -dump_vcd sat.vcd -enable_undef", + file=ys, + ) + for i, pattern in enumerate(chunk, 1): + ad = pattern.replace("x", "0") + ax = pattern.replace("1", "0").replace("x", "1") + print(end=f" -set-at {i} A {input_width}'b{pattern}", file=ys) + print(file=ys) + print(f"log sat 100%", file=ys) + + try: + yosys( + f""" + read_rtlil wrapped{mode}.il + clk2fflogic + script sat{mode}.ys + """ + ) + except subprocess.CalledProcessError: + remove(f"sat{mode}.out") + else: + sig_re = re.compile( + r" *[0-9]+ +\\([AY]) +(?:--|[0-9]+) +(?:--|[0-9a-f]+) +([01x]+)" + ) + current_input = None + with open(f"sat{mode}.log") as logfile, open(f"sat{mode}.out", "w") as outfile: + for line in logfile: + match = sig_re.match(line) + if match: + if match[1] == "A": + current_input = match[2] + else: + print(current_input, match[2], file=outfile) + +for mode in ["", "_xprop"]: + if f"opt_expr{mode}" not in steps: + continue + if not Path(f"wrapped{mode}.il").is_file(): + remove(f"opt_expr{mode}.out") + continue + yosys( + f""" + read_verilog const_tb.v + read_rtlil wrapped{mode}.il + hierarchy -top top; proc -noopt + flatten + opt_expr -keepdc; clean + dump -o opt_expr{mode}.list */\Y_* + """ + ) + + values = [] + + connect_re = re.compile(r" *connect +\\Y_([0-9]+) +[0-9]+'([01x]+)$") + with open(f"opt_expr{mode}.list") as connections: + for line in connections: + match = connect_re.match(line) + if match: + seq = int(match[1]) + data = match[2] + if len(data) < output_width: + data = data * output_width + values.append((seq, data)) + + values.sort() + + with open(f"opt_expr{mode}.out", "w") as outfile: + for seq, data in values: + print(patterns[seq], data, file=outfile) + + +if "compare" in steps: + groups = {} + missing = [] + + for output in all_outputs: + try: + with open(f"{output}.out") as f: + groups.setdefault(f.read(), []).append(output) + except FileNotFoundError: + missing.append(output) + + verified = Path(f"verified").is_file() + + with open("status", "w") as status: + name = Path('.').absolute().name + + status_list = [] + + if len(groups) > 1: + status_list.append("mismatch") + if not verified: + status_list.append("failed-verify") + if missing: + status_list.append("missing") + if not status_list: + status_list.append("ok") + print(f"{name}: {', '.join(status_list)}", file=status) + + if len(groups) > 1: + print("output differences:", file=status) + for group in groups.values(): + print(" -", *group, file=status) + if missing: + print("missing:", file=status) + print(" -", *missing, file=status) + + with open("status") as status: + print(end=status.read()) |