mirror of
https://github.com/YosysHQ/yosys
synced 2026-06-10 02:47:17 +00:00
Merge branch 'main' into related_load_data
This commit is contained in:
Arnim Läuger
GitHub
commit
f8b5da5058
226 changed files with 16144 additions and 2736 deletions
1
tests/arch/analogdevices/.gitignore
vendored
Normal file
1
tests/arch/analogdevices/.gitignore
vendored
Normal file
|
|
@ -0,0 +1 @@
|
|||
t_*.ys
|
||||
13
tests/arch/analogdevices/add_sub.ys
Normal file
13
tests/arch/analogdevices/add_sub.ys
Normal file
|
|
@ -0,0 +1,13 @@
|
|||
read_verilog ../common/add_sub.v
|
||||
hierarchy -top top
|
||||
proc
|
||||
design -save orig
|
||||
|
||||
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # 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
|
||||
stat
|
||||
select -assert-count 8 t:LUT2
|
||||
select -assert-count 2 t:CRY4
|
||||
select -assert-count 2 t:CRY4INIT
|
||||
select -assert-none t:LUT2 t:CRY4 t:CRY4INIT %% t:* %D
|
||||
47
tests/arch/analogdevices/adffs.ys
Normal file
47
tests/arch/analogdevices/adffs.ys
Normal file
|
|
@ -0,0 +1,47 @@
|
|||
read_verilog ../common/adffs.v
|
||||
design -save read
|
||||
|
||||
hierarchy -top adff
|
||||
proc
|
||||
equiv_opt -async2sync -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd adff # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:FFCE
|
||||
|
||||
select -assert-none t:FFCE %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top adffn
|
||||
proc
|
||||
equiv_opt -async2sync -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd adffn # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:FFCE
|
||||
select -assert-count 1 t:LUT1
|
||||
|
||||
select -assert-none t:FFCE t:LUT1 %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top dffs
|
||||
proc
|
||||
equiv_opt -async2sync -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd dffs # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:FFRE
|
||||
select -assert-count 1 t:LUT2
|
||||
stat
|
||||
select -assert-none t:FFRE t:LUT2 %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top ndffnr
|
||||
proc
|
||||
equiv_opt -async2sync -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd ndffnr # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:FFRE_N
|
||||
select -assert-count 1 t:LUT1
|
||||
|
||||
select -assert-none t:FFRE_N t:LUT1 %% t:* %D
|
||||
50
tests/arch/analogdevices/asym_ram_sdp.ys
Normal file
50
tests/arch/analogdevices/asym_ram_sdp.ys
Normal file
|
|
@ -0,0 +1,50 @@
|
|||
# Memory bits <= 18K; Data width <= 36; Address width <= 14: -> RBRAM2
|
||||
|
||||
# w4b | r16b
|
||||
design -reset
|
||||
read_verilog asym_ram_sdp_read_wider.v
|
||||
synth_analogdevices -top asym_ram_sdp_read_wider -noiopad
|
||||
select -assert-count 1 t:RBRAM2
|
||||
|
||||
# w8b | r16b
|
||||
design -reset
|
||||
read_verilog asym_ram_sdp_read_wider.v
|
||||
chparam -set WIDTHA 8 -set SIZEA 512 -set ADDRWIDTHA 9 asym_ram_sdp_read_wider
|
||||
synth_analogdevices -top asym_ram_sdp_read_wider -noiopad
|
||||
select -assert-count 1 t:RBRAM2
|
||||
|
||||
# w4b | r32b
|
||||
design -reset
|
||||
read_verilog asym_ram_sdp_read_wider.v
|
||||
chparam -set WIDTHB 32 -set SIZEB 128 -set ADDRWIDTHB 7 asym_ram_sdp_read_wider
|
||||
synth_analogdevices -top asym_ram_sdp_read_wider -noiopad
|
||||
select -assert-count 2 t:RBRAM2
|
||||
|
||||
# w16b | r4b
|
||||
design -reset
|
||||
read_verilog asym_ram_sdp_write_wider.v
|
||||
synth_analogdevices -top asym_ram_sdp_write_wider -noiopad
|
||||
select -assert-count 1 t:RBRAM2
|
||||
|
||||
# w16b | r8b
|
||||
design -reset
|
||||
read_verilog asym_ram_sdp_write_wider.v
|
||||
chparam -set WIDTHB 8 -set SIZEB 512 -set ADDRWIDTHB 9 asym_ram_sdp_read_wider
|
||||
synth_analogdevices -top asym_ram_sdp_write_wider -noiopad
|
||||
select -assert-count 1 t:RBRAM2
|
||||
|
||||
# w32b | r4b
|
||||
design -reset
|
||||
read_verilog asym_ram_sdp_write_wider.v
|
||||
chparam -set WIDTHA 32 -set SIZEA 128 -set ADDRWIDTHA 7 asym_ram_sdp_read_wider
|
||||
synth_analogdevices -top asym_ram_sdp_write_wider -noiopad
|
||||
select -assert-count 1 t:RBRAM2
|
||||
|
||||
# w4b | r24b
|
||||
design -reset
|
||||
read_verilog asym_ram_sdp_read_wider.v
|
||||
chparam -set SIZEA 768
|
||||
chparam -set WIDTHB 24 -set SIZEB 128 -set ADDRWIDTHB 7 asym_ram_sdp_read_wider
|
||||
synth_analogdevices -top asym_ram_sdp_read_wider -noiopad
|
||||
select -assert-count 2 t:RBRAM2
|
||||
|
||||
73
tests/arch/analogdevices/asym_ram_sdp_read_wider.v
Normal file
73
tests/arch/analogdevices/asym_ram_sdp_read_wider.v
Normal file
|
|
@ -0,0 +1,73 @@
|
|||
// Asymmetric port RAM
|
||||
// Read Wider than Write. Read Statement in loop
|
||||
//asym_ram_sdp_read_wider.v
|
||||
module asym_ram_sdp_read_wider (clkA, clkB, enaA, weA, enaB, addrA, addrB, diA, doB);
|
||||
parameter WIDTHA = 4;
|
||||
parameter SIZEA = 1024;
|
||||
parameter ADDRWIDTHA = 10;
|
||||
|
||||
parameter WIDTHB = 16;
|
||||
parameter SIZEB = 256;
|
||||
parameter ADDRWIDTHB = 8;
|
||||
|
||||
input clkA;
|
||||
input clkB;
|
||||
input weA;
|
||||
input enaA, enaB;
|
||||
input [ADDRWIDTHA-1:0] addrA;
|
||||
input [ADDRWIDTHB-1:0] addrB;
|
||||
input [WIDTHA-1:0] diA;
|
||||
output [WIDTHB-1:0] doB;
|
||||
|
||||
`define max(a,b) {(a) > (b) ? (a) : (b)}
|
||||
`define min(a,b) {(a) < (b) ? (a) : (b)}
|
||||
|
||||
function integer log2;
|
||||
input integer value;
|
||||
reg [31:0] shifted;
|
||||
integer res;
|
||||
begin
|
||||
if (value < 2)
|
||||
log2 = value;
|
||||
else
|
||||
begin
|
||||
shifted = value-1;
|
||||
for (res=0; shifted>0; res=res+1)
|
||||
shifted = shifted>>1;
|
||||
log2 = res;
|
||||
end
|
||||
end
|
||||
endfunction
|
||||
|
||||
localparam maxSIZE = `max(SIZEA, SIZEB);
|
||||
localparam maxWIDTH = `max(WIDTHA, WIDTHB);
|
||||
localparam minWIDTH = `min(WIDTHA, WIDTHB);
|
||||
|
||||
localparam RATIO = maxWIDTH / minWIDTH;
|
||||
localparam log2RATIO = log2(RATIO);
|
||||
|
||||
(* ram_style="block" *)
|
||||
reg [minWIDTH-1:0] RAM [0:maxSIZE-1];
|
||||
reg [WIDTHB-1:0] readB;
|
||||
|
||||
always @(posedge clkA)
|
||||
begin
|
||||
if (enaA) begin
|
||||
if (weA)
|
||||
RAM[addrA] <= diA;
|
||||
end
|
||||
end
|
||||
|
||||
always @(posedge clkB)
|
||||
begin : ramread
|
||||
integer i;
|
||||
reg [log2RATIO-1:0] lsbaddr;
|
||||
if (enaB) begin
|
||||
for (i = 0; i < RATIO; i = i+1) begin
|
||||
lsbaddr = i;
|
||||
readB[(i+1)*minWIDTH-1 -: minWIDTH] <= RAM[{addrB, lsbaddr}];
|
||||
end
|
||||
end
|
||||
end
|
||||
assign doB = readB;
|
||||
endmodule
|
||||
72
tests/arch/analogdevices/asym_ram_sdp_write_wider.v
Normal file
72
tests/arch/analogdevices/asym_ram_sdp_write_wider.v
Normal file
|
|
@ -0,0 +1,72 @@
|
|||
// Asymmetric port RAM
|
||||
// Write wider than Read. Write Statement in a loop.
|
||||
// asym_ram_sdp_write_wider.v
|
||||
module asym_ram_sdp_write_wider (clkA, clkB, weA, enaA, enaB, addrA, addrB, diA, doB);
|
||||
parameter WIDTHB = 4;
|
||||
parameter SIZEB = 1024;
|
||||
parameter ADDRWIDTHB = 10;
|
||||
|
||||
parameter WIDTHA = 16;
|
||||
parameter SIZEA = 256;
|
||||
parameter ADDRWIDTHA = 8;
|
||||
|
||||
input clkA;
|
||||
input clkB;
|
||||
input weA;
|
||||
input enaA, enaB;
|
||||
input [ADDRWIDTHA-1:0] addrA;
|
||||
input [ADDRWIDTHB-1:0] addrB;
|
||||
input [WIDTHA-1:0] diA;
|
||||
output [WIDTHB-1:0] doB;
|
||||
|
||||
`define max(a,b) {(a) > (b) ? (a) : (b)}
|
||||
`define min(a,b) {(a) < (b) ? (a) : (b)}
|
||||
|
||||
function integer log2;
|
||||
input integer value;
|
||||
reg [31:0] shifted;
|
||||
integer res;
|
||||
begin
|
||||
if (value < 2)
|
||||
log2 = value;
|
||||
else
|
||||
begin
|
||||
shifted = value-1;
|
||||
for (res=0; shifted>0; res=res+1)
|
||||
shifted = shifted>>1;
|
||||
log2 = res;
|
||||
end
|
||||
end
|
||||
endfunction
|
||||
|
||||
localparam maxSIZE = `max(SIZEA, SIZEB);
|
||||
localparam maxWIDTH = `max(WIDTHA, WIDTHB);
|
||||
localparam minWIDTH = `min(WIDTHA, WIDTHB);
|
||||
|
||||
localparam RATIO = maxWIDTH / minWIDTH;
|
||||
localparam log2RATIO = log2(RATIO);
|
||||
|
||||
(* ram_style="block" *)
|
||||
reg [minWIDTH-1:0] RAM [0:maxSIZE-1];
|
||||
reg [WIDTHB-1:0] readB;
|
||||
|
||||
always @(posedge clkB) begin
|
||||
if (enaB) begin
|
||||
readB <= RAM[addrB];
|
||||
end
|
||||
end
|
||||
assign doB = readB;
|
||||
|
||||
always @(posedge clkA)
|
||||
begin : ramwrite
|
||||
integer i;
|
||||
reg [log2RATIO-1:0] lsbaddr;
|
||||
for (i=0; i< RATIO; i= i+ 1) begin : write1
|
||||
lsbaddr = i;
|
||||
if (enaA) begin
|
||||
if (weA)
|
||||
RAM[{addrA, lsbaddr}] <= diA[(i+1)*minWIDTH-1 -: minWIDTH];
|
||||
end
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
39
tests/arch/analogdevices/attributes_test.ys
Normal file
39
tests/arch/analogdevices/attributes_test.ys
Normal file
|
|
@ -0,0 +1,39 @@
|
|||
# Check that blockram memory without parameters is not modified
|
||||
read_verilog ../common/memory_attributes/attributes_test.v
|
||||
hierarchy -top block_ram
|
||||
synth_analogdevices -top block_ram -noiopad
|
||||
cd block_ram # Constrain all select calls below inside the top module
|
||||
# select -assert-count 1 t:RBRAM2 # This currently infers LUTRAM because BRAM is expensive.
|
||||
|
||||
# Check that distributed memory without parameters is not modified
|
||||
design -reset
|
||||
read_verilog ../common/memory_attributes/attributes_test.v
|
||||
hierarchy -top distributed_ram
|
||||
synth_analogdevices -top distributed_ram -noiopad
|
||||
cd distributed_ram # Constrain all select calls below inside the top module
|
||||
select -assert-count 8 t:RAMS64X1
|
||||
select -assert-count 8 t:FFRE
|
||||
|
||||
# Set ram_style distributed to blockram memory; will be implemented as distributed
|
||||
design -reset
|
||||
read_verilog ../common/memory_attributes/attributes_test.v
|
||||
setattr -set ram_style "distributed" block_ram/m:*
|
||||
synth_analogdevices -top block_ram -noiopad
|
||||
cd block_ram # Constrain all select calls below inside the top module
|
||||
select -assert-count 64 t:RAMS64X1
|
||||
select -assert-count 4 t:FFRE
|
||||
|
||||
# Set synthesis, logic_block to blockram memory; will be implemented as distributed
|
||||
design -reset
|
||||
read_verilog ../common/memory_attributes/attributes_test.v
|
||||
setattr -set logic_block 1 block_ram/m:*
|
||||
synth_analogdevices -top block_ram -noiopad
|
||||
cd block_ram # Constrain all select calls below inside the top module
|
||||
select -assert-count 0 t:RBRAM2
|
||||
|
||||
# Set ram_style block to a distributed memory; will be implemented as blockram
|
||||
design -reset
|
||||
read_verilog ../common/memory_attributes/attributes_test.v
|
||||
synth_analogdevices -top distributed_ram_manual -noiopad
|
||||
cd distributed_ram_manual # Constrain all select calls below inside the top module
|
||||
# select -assert-count 1 t:RBRAM2 # This gets implemented in logic instead
|
||||
77
tests/arch/analogdevices/blockram.ys
Normal file
77
tests/arch/analogdevices/blockram.ys
Normal file
|
|
@ -0,0 +1,77 @@
|
|||
### TODO: Not running equivalence checking because BRAM models does not exists
|
||||
### currently. Checking instance counts instead.
|
||||
# Memory bits <= 18K; Data width <= 36; Address width <= 14: -> RBRAM2
|
||||
read_verilog ../common/blockram.v
|
||||
chparam -set ADDRESS_WIDTH 12 -set DATA_WIDTH 1 sync_ram_sdp
|
||||
setattr -set ram_style "block" sync_ram_sdp
|
||||
synth_analogdevices -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RBRAM2
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 18 sync_ram_sdp
|
||||
setattr -set ram_style "block" sync_ram_sdp
|
||||
synth_analogdevices -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RBRAM2
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
chparam -set ADDRESS_WIDTH 14 -set DATA_WIDTH 1 sync_ram_sdp
|
||||
setattr -set ram_style "block" sync_ram_sdp
|
||||
synth_analogdevices -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RBRAM2
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 sync_ram_sdp
|
||||
synth_analogdevices -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RBRAM2
|
||||
|
||||
# Anything memory bits < 1024 -> LUTRAM
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 2 sync_ram_sdp
|
||||
synth_analogdevices -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 0 t:RBRAM2
|
||||
select -assert-count 8 t:RAMD64X1
|
||||
select -assert-count 2 t:FFRE
|
||||
|
||||
# More than 18K bits, data width <= 36 (TDP), and address width from 10 to 15b (non-cascaded) -> RAMB36E1
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 36 sync_ram_sdp
|
||||
synth_analogdevices -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RBRAM2
|
||||
|
||||
|
||||
### With parameters
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 12 -chparam DATA_WIDTH 1
|
||||
setattr -set ram_style "block" m:memory
|
||||
synth_analogdevices -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RBRAM2
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 12 -chparam DATA_WIDTH 1
|
||||
setattr -set logic_block 1 m:memory
|
||||
synth_analogdevices -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 0 t:RBRAM2
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1
|
||||
setattr -set ram_style "block" m:memory
|
||||
synth_analogdevices -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RBRAM2
|
||||
34
tests/arch/analogdevices/bug1460.ys
Normal file
34
tests/arch/analogdevices/bug1460.ys
Normal file
|
|
@ -0,0 +1,34 @@
|
|||
read_verilog <<EOT
|
||||
module register_file(
|
||||
input wire clk,
|
||||
input wire write_enable,
|
||||
input wire [63:0] write_data,
|
||||
input wire [4:0] write_reg,
|
||||
input wire [4:0] read1_reg,
|
||||
input wire [4:0] read2_reg,
|
||||
input wire [4:0] read3_reg,
|
||||
output reg [63:0] read1_data,
|
||||
output reg [63:0] read2_data,
|
||||
output reg [63:0] read3_data
|
||||
);
|
||||
|
||||
reg [63:0] registers[0:31];
|
||||
|
||||
always @(posedge clk) begin
|
||||
if (write_enable == 1'b1) begin
|
||||
registers[write_reg] <= write_data;
|
||||
end
|
||||
end
|
||||
|
||||
always @(all) begin
|
||||
read1_data <= registers[read1_reg];
|
||||
read2_data <= registers[read2_reg];
|
||||
read3_data <= registers[read3_reg];
|
||||
end
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
synth_analogdevices -noiopad
|
||||
cd register_file
|
||||
select -assert-count 192 t:RAMD32X1
|
||||
select -assert-none t:RAMD32X1 %% t:* %D
|
||||
11
tests/arch/analogdevices/bug1462.ys
Normal file
11
tests/arch/analogdevices/bug1462.ys
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
read_verilog << EOF
|
||||
module top(...);
|
||||
input wire [31:0] A;
|
||||
output wire [31:0] P;
|
||||
|
||||
assign P = A * 32'h12300000;
|
||||
|
||||
endmodule
|
||||
EOF
|
||||
|
||||
synth_analogdevices
|
||||
18
tests/arch/analogdevices/bug1480.ys
Normal file
18
tests/arch/analogdevices/bug1480.ys
Normal file
|
|
@ -0,0 +1,18 @@
|
|||
read_verilog << EOF
|
||||
module top(...);
|
||||
|
||||
input signed [17:0] A;
|
||||
input signed [17:0] B;
|
||||
output X;
|
||||
output Y;
|
||||
|
||||
wire [35:0] P;
|
||||
assign P = A * B;
|
||||
|
||||
assign X = P[0];
|
||||
assign Y = P[35];
|
||||
|
||||
endmodule
|
||||
EOF
|
||||
|
||||
synth_analogdevices
|
||||
16
tests/arch/analogdevices/bug1598.ys
Normal file
16
tests/arch/analogdevices/bug1598.ys
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
read_verilog <<EOT
|
||||
module led_blink (
|
||||
input clk,
|
||||
output ledc
|
||||
);
|
||||
|
||||
reg [6:0] led_counter = 0;
|
||||
always @( posedge clk ) begin
|
||||
led_counter <= led_counter + 1;
|
||||
end
|
||||
assign ledc = !led_counter[ 6:3 ];
|
||||
|
||||
endmodule
|
||||
EOT
|
||||
proc
|
||||
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices
|
||||
13
tests/arch/analogdevices/counter.ys
Normal file
13
tests/arch/analogdevices/counter.ys
Normal file
|
|
@ -0,0 +1,13 @@
|
|||
read_verilog ../common/counter.v
|
||||
hierarchy -top top
|
||||
proc
|
||||
flatten
|
||||
equiv_opt -async2sync -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # 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
|
||||
stat
|
||||
select -assert-count 8 t:FFCE
|
||||
select -assert-count 1 t:LUT1
|
||||
select -assert-count 2 t:CRY4
|
||||
select -assert-count 1 t:CRY4INIT
|
||||
select -assert-none t:FFCE t:LUT1 t:CRY4 t:CRY4INIT %% t:* %D
|
||||
41
tests/arch/analogdevices/dffs.ys
Normal file
41
tests/arch/analogdevices/dffs.ys
Normal file
|
|
@ -0,0 +1,41 @@
|
|||
read_verilog ../common/dffs.v
|
||||
design -save read
|
||||
|
||||
hierarchy -top dff
|
||||
proc
|
||||
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd dff # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:FFRE
|
||||
select -assert-none t:FFRE %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top dffe
|
||||
proc
|
||||
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd dffe # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:FFRE
|
||||
select -assert-none t:FFRE %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top dff
|
||||
proc
|
||||
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -dff -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd dff # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:FFRE
|
||||
select -assert-none t:FFRE %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top dffe
|
||||
proc
|
||||
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -dff -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd dffe # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:FFRE
|
||||
select -assert-none t:FFRE %% t:* %D
|
||||
|
||||
42
tests/arch/analogdevices/dsp_abc9.ys
Normal file
42
tests/arch/analogdevices/dsp_abc9.ys
Normal file
|
|
@ -0,0 +1,42 @@
|
|||
logger -nowarn "Yosys has only limited support for tri-state logic at the moment\. .*"
|
||||
logger -nowarn "Ignoring boxed module .*\."
|
||||
|
||||
read_verilog <<EOT
|
||||
module top(input [24:0] A, input [17:0] B, output [47:0] P);
|
||||
DSP48E1 #(.PREG(0)) dsp(.A(A), .B(B), .P(P));
|
||||
endmodule
|
||||
EOT
|
||||
techmap -autoproc -wb -map +/analogdevices/cells_sim.v
|
||||
opt
|
||||
scc -expect 0
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input signed [24:0] A, input signed [17:0] B, output [47:0] P);
|
||||
assign P = A * B;
|
||||
endmodule
|
||||
EOT
|
||||
synth_analogdevices
|
||||
techmap -autoproc -wb -map +/analogdevices/cells_sim.v
|
||||
opt -full -fine
|
||||
select -assert-count 2 t:$mul
|
||||
select -assert-count 0 t:* t:$mul %D
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog -icells -formal <<EOT
|
||||
module top(output [43:0] P);
|
||||
\$__MUL22X22 mul (.A(42), .B(42), .Y(P));
|
||||
assert property (P == 42*42);
|
||||
endmodule
|
||||
EOT
|
||||
async2sync
|
||||
techmap -map +/analogdevices/dsp_map.v
|
||||
verilog_defaults -add -D ALLOW_WHITEBOX_DSP48E1
|
||||
synth_analogdevices
|
||||
techmap -autoproc -wb -map +/analogdevices/cells_sim.v
|
||||
opt -full -fine
|
||||
select -assert-count 0 t:* t:$assert %d
|
||||
sat -verify -prove-asserts
|
||||
|
||||
20
tests/arch/analogdevices/fsm.ys
Normal file
20
tests/arch/analogdevices/fsm.ys
Normal file
|
|
@ -0,0 +1,20 @@
|
|||
read_verilog ../common/fsm.v
|
||||
hierarchy -top fsm
|
||||
proc
|
||||
flatten
|
||||
|
||||
design -save orig
|
||||
|
||||
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
|
||||
miter -equiv -make_assert -flatten gold gate miter
|
||||
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
|
||||
stat
|
||||
select -assert-count 6 t:FFRE
|
||||
select -assert-count 1 t:LUT1
|
||||
select -assert-count 1 t:LUT3
|
||||
select -assert-count 1 t:LUT4
|
||||
select -assert-count 5 t:LUT5
|
||||
select -assert-none t:FFRE t:LUT1 t:LUT3 t:LUT4 t:LUT5 %% t:* %D
|
||||
11
tests/arch/analogdevices/logic.ys
Normal file
11
tests/arch/analogdevices/logic.ys
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
read_verilog ../common/logic.v
|
||||
hierarchy -top top
|
||||
proc
|
||||
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # 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:LUT1
|
||||
select -assert-count 6 t:LUT2
|
||||
select -assert-count 2 t:LUT4
|
||||
select -assert-none t:LUT1 t:LUT2 t:LUT4 %% t:* %D
|
||||
113
tests/arch/analogdevices/lutram.ys
Normal file
113
tests/arch/analogdevices/lutram.ys
Normal file
|
|
@ -0,0 +1,113 @@
|
|||
design -reset
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r -chparam A_WIDTH 5
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
|
||||
memory
|
||||
opt -full
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd lutram_1w1r
|
||||
select -assert-count 8 t:FFRE
|
||||
select -assert-count 8 t:RAMS64X1
|
||||
select -assert-none t:FFRE t:RAMS64X1 %% t:* %D
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
|
||||
memory
|
||||
opt -full
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd lutram_1w1r
|
||||
dump
|
||||
select -assert-count 8 t:FFRE
|
||||
select -assert-count 8 t:RAMS64X1
|
||||
select -assert-none t:FFRE t:RAMS64X1 %% t:* %D
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w3r
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
|
||||
memory
|
||||
opt -full
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd lutram_1w3r
|
||||
select -assert-count 24 t:FFRE
|
||||
select -assert-count 16 t:RAMD32X1
|
||||
select -assert-none t:FFRE t:RAMD32X1 %% t:* %D
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w3r -chparam A_WIDTH 6
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
|
||||
memory
|
||||
opt -full
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd lutram_1w3r
|
||||
select -assert-count 24 t:FFRE
|
||||
select -assert-count 16 t:RAMD64X1
|
||||
select -assert-none t:FFRE t:RAMD64X1 %% t:* %D
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 6
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
|
||||
memory
|
||||
opt -full
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd lutram_1w1r
|
||||
select -assert-count 6 t:FFRE
|
||||
select -assert-count 6 t:RAMS64X1
|
||||
select -assert-none t:FFRE t:RAMS64X1 %% t:* %D
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 6
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
|
||||
memory
|
||||
opt -full
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd lutram_1w1r
|
||||
select -assert-count 6 t:FFRE
|
||||
select -assert-count 6 t:RAMS64X1
|
||||
select -assert-none t:FFRE t:RAMS64X1 %% t:* %D
|
||||
121
tests/arch/analogdevices/mem_gen.py
Normal file
121
tests/arch/analogdevices/mem_gen.py
Normal file
|
|
@ -0,0 +1,121 @@
|
|||
from __future__ import annotations
|
||||
|
||||
from dataclasses import dataclass
|
||||
|
||||
|
||||
blockram_template = """# ======================================
|
||||
log ** GENERATING TEST {top} WITH PARAMS{param_str}
|
||||
design -reset; read_verilog -defer ../common/blockram.v
|
||||
chparam{param_str} {top}
|
||||
hierarchy -top {top}
|
||||
echo on
|
||||
debug synth_analogdevices -tech {tech} -top {top} {opts} -run :map_ffram
|
||||
stat; echo off
|
||||
"""
|
||||
inference_tests: "list[tuple[str, list[tuple[str, int]], str, list[str], list[str]]]" = [
|
||||
# RBRAM2 has TDP and SDP for 8192x5bit, 4096x9bit, and 2048x40bit
|
||||
("t16ffc", [("ADDRESS_WIDTH", 13), ("DATA_WIDTH", 5)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
|
||||
("t16ffc", [("ADDRESS_WIDTH", 12), ("DATA_WIDTH", 9)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
|
||||
("t16ffc", [("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 40)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
|
||||
# LUTRAM is generally cheaper than BRAM for undersized (SDP) memories
|
||||
("t16ffc", [("ADDRESS_WIDTH", 6), ("DATA_WIDTH", 1)], "sync_ram_sdp", ["-assert-count 1 t:RAMD64X1"], []),
|
||||
("t16ffc", [("ADDRESS_WIDTH", 6), ("DATA_WIDTH", 8)], "sync_ram_sdp", ["-assert-count 8 t:RAMD64X1"], []),
|
||||
("t16ffc", [("ADDRESS_WIDTH", 10), ("DATA_WIDTH", 8)], "sync_ram_sdp", ["-assert-count 128 t:RAMD64X1"], []),
|
||||
("t16ffc", [("ADDRESS_WIDTH", 10), ("DATA_WIDTH", 16)], "sync_ram_sdp", ["-assert-count 256 t:RAMD64X1"], []),
|
||||
# RBRAM is half the depth of RBRAM2, and doesn't have TDP, also LUTRAM is cheaper, so we need to specify not to use it
|
||||
("t40lp", [("ADDRESS_WIDTH", 13), ("DATA_WIDTH", 5)], "sync_ram_sdp", ["-assert-count 2 t:RBRAM"], ["-nolutram"]),
|
||||
("t40lp", [("ADDRESS_WIDTH", 12), ("DATA_WIDTH", 5)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
|
||||
("t40lp", [("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 9)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
|
||||
("t40lp", [("ADDRESS_WIDTH", 10), ("DATA_WIDTH", 40)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
|
||||
# 2048x32 and 2048x36bit are also valid
|
||||
("t16ffc", [("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 32)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
|
||||
("t16ffc", [("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 36)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
|
||||
("t40lp", [("ADDRESS_WIDTH", 10), ("DATA_WIDTH", 32)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
|
||||
("t40lp", [("ADDRESS_WIDTH", 10), ("DATA_WIDTH", 36)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
|
||||
|
||||
# 4096x16/18bit can be mapped to a single 2048x32/36bit
|
||||
("t16ffc", [("ADDRESS_WIDTH", 12), ("DATA_WIDTH", 16)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
|
||||
("t16ffc", [("ADDRESS_WIDTH", 12), ("DATA_WIDTH", 18)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
|
||||
("t40lp", [("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 16)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
|
||||
("t40lp", [("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 18)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
|
||||
# same for 8192x8/9bit
|
||||
("t16ffc", [("ADDRESS_WIDTH", 13), ("DATA_WIDTH", 8)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
|
||||
("t16ffc", [("ADDRESS_WIDTH", 13), ("DATA_WIDTH", 9)], "sync_ram_*dp", ["-assert-count 1 t:RBRAM2"], []),
|
||||
("t40lp", [("ADDRESS_WIDTH", 12), ("DATA_WIDTH", 8)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
|
||||
("t40lp", [("ADDRESS_WIDTH", 12), ("DATA_WIDTH", 9)], "sync_ram_sdp", ["-assert-count 1 t:RBRAM"], ["-nolutram"]),
|
||||
# but 4096x20bit requires extra memories because 2048x40bit has 8bit byte enables (which doesn't divide 20bit evenly)
|
||||
("t16ffc", [("ADDRESS_WIDTH", 12), ("DATA_WIDTH", 20)], "sync_ram_sdp", ["-assert-count 2 t:RBRAM2"], []),
|
||||
("t40lp", [("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 20)], "sync_ram_sdp", ["-assert-count 2 t:RBRAM"], ["-nolutram"]),
|
||||
]
|
||||
|
||||
@dataclass
|
||||
class TestClass:
|
||||
params: dict[str, int]
|
||||
top: str
|
||||
assertions: list[str]
|
||||
test_steps: None | list[dict[str, int]]
|
||||
opts: list[str]
|
||||
tech: str = "t16ffc"
|
||||
|
||||
sim_tests: list[TestClass] = []
|
||||
|
||||
for (tech, params, top, assertions, opts) in inference_tests:
|
||||
sim_test = TestClass(
|
||||
params=dict(params),
|
||||
top=top,
|
||||
assertions=assertions,
|
||||
test_steps=None,
|
||||
opts=opts,
|
||||
tech=tech,
|
||||
)
|
||||
sim_tests.append(sim_test)
|
||||
|
||||
i = 0
|
||||
j = 0
|
||||
max_j = 16
|
||||
f = None
|
||||
for sim_test in sim_tests:
|
||||
# format params
|
||||
param_str = ""
|
||||
for (key, val) in sim_test.params.items():
|
||||
param_str += f" -set {key} {val}"
|
||||
|
||||
# resolve top module wildcards
|
||||
top_list = [sim_test.top]
|
||||
if "*dp" in sim_test.top:
|
||||
top_list += [
|
||||
sim_test.top.replace("*dp", dp_sub) for dp_sub in ["sdp", "tdp"]
|
||||
]
|
||||
if "w*r" in sim_test.top:
|
||||
top_list += [
|
||||
sim_test.top.replace("w*r", wr_sub) for wr_sub in ["wwr", "wrr"]
|
||||
]
|
||||
if len(top_list) > 1:
|
||||
top_list.pop(0)
|
||||
|
||||
# iterate over string substitutions
|
||||
for top in top_list:
|
||||
# limit number of tests per file to allow parallel make
|
||||
if not f:
|
||||
fn = f"t_mem{i}.ys"
|
||||
f = open(fn, mode="w")
|
||||
j = 0
|
||||
|
||||
# output yosys script test file
|
||||
print(
|
||||
blockram_template.format(param_str=param_str, top=top, tech=sim_test.tech, opts=" ".join(sim_test.opts)),
|
||||
file=f
|
||||
)
|
||||
for assertion in sim_test.assertions:
|
||||
print(f"log ** CHECKING CELL COUNTS FOR TEST {top} WITH PARAMS{param_str} ON TECH {sim_test.tech}", file=f)
|
||||
print(f"select {assertion}", file=f)
|
||||
print("", file=f)
|
||||
|
||||
# increment test counter
|
||||
j += 1
|
||||
if j >= max_j:
|
||||
f = f.close()
|
||||
i += 1
|
||||
|
||||
if f:
|
||||
f.close()
|
||||
9
tests/arch/analogdevices/mul.ys
Normal file
9
tests/arch/analogdevices/mul.ys
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
read_verilog ../common/mul.v
|
||||
hierarchy -top top
|
||||
proc
|
||||
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # 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:RBBDSP
|
||||
select -assert-none t:RBBDSP %% t:* %D
|
||||
30
tests/arch/analogdevices/mul_unsigned.v
Normal file
30
tests/arch/analogdevices/mul_unsigned.v
Normal file
|
|
@ -0,0 +1,30 @@
|
|||
/*
|
||||
Example from: https://www.xilinx.com/support/documentation/sw_manuals/xilinx2019_1/ug901-vivado-synthesis.pdf [p. 89].
|
||||
*/
|
||||
|
||||
// Unsigned 16x24-bit Multiplier
|
||||
// 1 latency stage on operands
|
||||
// 3 latency stage after the multiplication
|
||||
// File: multipliers2.v
|
||||
//
|
||||
module mul_unsigned (clk, A, B, RES);
|
||||
parameter WIDTHA = /*16*/ 6;
|
||||
parameter WIDTHB = /*24*/ 9;
|
||||
input clk;
|
||||
input [WIDTHA-1:0] A;
|
||||
input [WIDTHB-1:0] B;
|
||||
output [WIDTHA+WIDTHB-1:0] RES;
|
||||
reg [WIDTHA-1:0] rA;
|
||||
reg [WIDTHB-1:0] rB;
|
||||
reg [WIDTHA+WIDTHB-1:0] M [3:0];
|
||||
integer i;
|
||||
always @(posedge clk)
|
||||
begin
|
||||
rA <= A;
|
||||
rB <= B;
|
||||
M[0] <= rA * rB;
|
||||
for (i = 0; i < 3; i = i+1)
|
||||
M[i+1] <= M[i];
|
||||
end
|
||||
assign RES = M[3];
|
||||
endmodule
|
||||
10
tests/arch/analogdevices/mul_unsigned.ys
Normal file
10
tests/arch/analogdevices/mul_unsigned.ys
Normal file
|
|
@ -0,0 +1,10 @@
|
|||
read_verilog mul_unsigned.v
|
||||
hierarchy -top mul_unsigned
|
||||
proc
|
||||
|
||||
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd mul_unsigned # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:RBBDSP
|
||||
select -assert-count 75 t:FFRE
|
||||
select -assert-none t:RBBDSP t:FFRE %% t:* %D
|
||||
50
tests/arch/analogdevices/mux.ys
Normal file
50
tests/arch/analogdevices/mux.ys
Normal file
|
|
@ -0,0 +1,50 @@
|
|||
read_verilog ../common/mux.v
|
||||
design -save read
|
||||
|
||||
hierarchy -top mux2
|
||||
proc
|
||||
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd mux2 # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:LUT3
|
||||
|
||||
select -assert-none t:LUT3 %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top mux4
|
||||
proc
|
||||
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd mux4 # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:LUT6
|
||||
|
||||
select -assert-none t:LUT6 %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top mux8
|
||||
proc
|
||||
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd mux8 # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:LUT3
|
||||
select -assert-count 2 t:LUT6
|
||||
|
||||
select -assert-none t:LUT3 t:LUT6 %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top mux16
|
||||
proc
|
||||
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd mux16 # Constrain all select calls below inside the top module
|
||||
select -assert-max 2 t:LUT3
|
||||
select -assert-max 2 t:LUT4
|
||||
select -assert-min 4 t:LUT6
|
||||
select -assert-max 7 t:LUT6
|
||||
select -assert-max 2 t:LUTMUX7
|
||||
dump
|
||||
|
||||
select -assert-none t:LUT6 t:LUT4 t:LUT3 t:LUTMUX7 %% t:* %D
|
||||
26
tests/arch/analogdevices/opt_lut_ins.ys
Normal file
26
tests/arch/analogdevices/opt_lut_ins.ys
Normal file
|
|
@ -0,0 +1,26 @@
|
|||
read_rtlil << EOF
|
||||
|
||||
module \top
|
||||
|
||||
wire width 4 input 1 \A
|
||||
|
||||
wire output 2 \O
|
||||
|
||||
cell \LUT4 $0
|
||||
parameter \INIT 16'1111110011000000
|
||||
connect \I0 \A [0]
|
||||
connect \I1 \A [1]
|
||||
connect \I2 \A [2]
|
||||
connect \I3 \A [3]
|
||||
connect \O \O
|
||||
end
|
||||
end
|
||||
|
||||
EOF
|
||||
|
||||
read_verilog -lib +/analogdevices/cells_sim.v
|
||||
equiv_opt -assert -map +/analogdevices/cells_sim.v opt_lut_ins -tech analogdevices
|
||||
|
||||
design -load postopt
|
||||
|
||||
select -assert-count 1 t:LUT3
|
||||
5
tests/arch/analogdevices/run-test.sh
Executable file
5
tests/arch/analogdevices/run-test.sh
Executable file
|
|
@ -0,0 +1,5 @@
|
|||
#!/usr/bin/env bash
|
||||
set -eu
|
||||
python3 mem_gen.py
|
||||
source ../../gen-tests-makefile.sh
|
||||
generate_mk --yosys-scripts --bash
|
||||
10
tests/arch/analogdevices/shifter.ys
Normal file
10
tests/arch/analogdevices/shifter.ys
Normal file
|
|
@ -0,0 +1,10 @@
|
|||
read_verilog ../common/shifter.v
|
||||
hierarchy -top top
|
||||
proc
|
||||
flatten
|
||||
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # 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 8 t:FFRE
|
||||
select -assert-none t:FFRE %% t:* %D
|
||||
|
|
@ -22,6 +22,30 @@ module sync_ram_sp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10)
|
|||
endmodule // sync_ram_sp
|
||||
|
||||
|
||||
module sync_ram_sp_nochange #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10)
|
||||
(input wire write_enable, clk,
|
||||
input wire [DATA_WIDTH-1:0] data_in,
|
||||
input wire [ADDRESS_WIDTH-1:0] address_in,
|
||||
output wire [DATA_WIDTH-1:0] data_out);
|
||||
|
||||
localparam WORD = (DATA_WIDTH-1);
|
||||
localparam DEPTH = (2**ADDRESS_WIDTH-1);
|
||||
|
||||
reg [WORD:0] data_out_r;
|
||||
reg [WORD:0] memory [0:DEPTH];
|
||||
|
||||
always @(posedge clk) begin
|
||||
if (write_enable)
|
||||
memory[address_in] <= data_in;
|
||||
else
|
||||
data_out_r <= memory[address_in];
|
||||
end
|
||||
|
||||
assign data_out = data_out_r;
|
||||
|
||||
endmodule // sync_ram_sp_nochange
|
||||
|
||||
|
||||
module sync_ram_sdp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10)
|
||||
(input wire clk, write_enable,
|
||||
input wire [DATA_WIDTH-1:0] data_in,
|
||||
|
|
@ -112,6 +136,62 @@ module sync_ram_sdp_wrr #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10, SHIFT_VAL=1)
|
|||
endmodule // sync_ram_sdp_wrr
|
||||
|
||||
|
||||
module double_sync_ram_sp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10, USE_TDP=0)
|
||||
(
|
||||
input wire write_enable_a, clk_a,
|
||||
input wire [DATA_WIDTH-1:0] data_in_a,
|
||||
input wire [ADDRESS_WIDTH-1:0] address_in_a,
|
||||
output wire [DATA_WIDTH-1:0] data_out_a,
|
||||
|
||||
input wire write_enable_b, clk_b,
|
||||
input wire [DATA_WIDTH-1:0] data_in_b,
|
||||
input wire [ADDRESS_WIDTH-1:0] address_in_b,
|
||||
output wire [DATA_WIDTH-1:0] data_out_b
|
||||
);
|
||||
|
||||
generate
|
||||
if (USE_TDP) begin
|
||||
|
||||
sync_ram_tdp #(
|
||||
.DATA_WIDTH(DATA_WIDTH),
|
||||
.ADDRESS_WIDTH(ADDRESS_WIDTH+1)
|
||||
) ram (
|
||||
.clk_a(clk_a), .clk_b(clk_b),
|
||||
.write_enable_a(write_enable_a), .write_enable_b(write_enable_b),
|
||||
.write_data_a(data_in_a), .write_data_b(data_in_b),
|
||||
.addr_a({1'b0, address_in_a}), .addr_b({1'b1, address_in_b}),
|
||||
.read_data_a(data_out_a), .read_data_b(data_out_b)
|
||||
);
|
||||
|
||||
end else begin
|
||||
|
||||
sync_ram_sp #(
|
||||
.DATA_WIDTH(DATA_WIDTH),
|
||||
.ADDRESS_WIDTH(ADDRESS_WIDTH)
|
||||
) a_ram (
|
||||
.write_enable(write_enable_a),
|
||||
.clk(clk_a),
|
||||
.data_in(data_in_a),
|
||||
.address_in(address_in_a),
|
||||
.data_out(data_out_a)
|
||||
);
|
||||
|
||||
sync_ram_sp #(
|
||||
.DATA_WIDTH(DATA_WIDTH),
|
||||
.ADDRESS_WIDTH(ADDRESS_WIDTH)
|
||||
) b_ram (
|
||||
.write_enable(write_enable_b),
|
||||
.clk(clk_b),
|
||||
.data_in(data_in_b),
|
||||
.address_in(address_in_b),
|
||||
.data_out(data_out_b)
|
||||
);
|
||||
end
|
||||
endgenerate
|
||||
|
||||
endmodule // double_sync_ram_sp
|
||||
|
||||
|
||||
module double_sync_ram_sdp #(parameter DATA_WIDTH_A=8, ADDRESS_WIDTH_A=10, DATA_WIDTH_B=8, ADDRESS_WIDTH_B=10)
|
||||
(
|
||||
input wire write_enable_a, clk_a,
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ EOF
|
|||
|
||||
read_verilog -lib +/ecp5/cells_sim.v
|
||||
|
||||
equiv_opt -assert -map +/ecp5/cells_sim.v opt_lut_ins -tech ecp5
|
||||
equiv_opt -assert -map +/ecp5/cells_sim.v opt_lut_ins -tech lattice
|
||||
|
||||
design -load postopt
|
||||
|
||||
|
|
|
|||
31
tests/arch/gowin/bug5688.ys
Normal file
31
tests/arch/gowin/bug5688.ys
Normal file
|
|
@ -0,0 +1,31 @@
|
|||
read_verilog << EOT
|
||||
`default_nettype none
|
||||
|
||||
module top (
|
||||
input wire clk,
|
||||
input wire [9:0] rd_addr,
|
||||
output reg [15:0] rd_data,
|
||||
input wire [9:0] wr_addr,
|
||||
input wire [15:0] wr_data,
|
||||
input wire wr_en
|
||||
);
|
||||
|
||||
(* ram_style = "block" *) reg [15:0] mem [0:1023];
|
||||
|
||||
// Read port — separate always block
|
||||
always @(posedge clk) begin
|
||||
rd_data <= mem[rd_addr];
|
||||
end
|
||||
|
||||
// Write port — separate always block
|
||||
always @(posedge clk) begin
|
||||
if (wr_en)
|
||||
mem[wr_addr] <= wr_data;
|
||||
end
|
||||
|
||||
endmodule
|
||||
|
||||
EOT
|
||||
synth_gowin -top top
|
||||
splitnets
|
||||
select -assert-any top/mem.0.0 %ci*:+DPX9B[ADA]:+DFF:+IBUF i:wr_en %i
|
||||
53
tests/arch/gowin/mul_gw1n.ys
Normal file
53
tests/arch/gowin/mul_gw1n.ys
Normal file
|
|
@ -0,0 +1,53 @@
|
|||
read_verilog ../common/mul.v
|
||||
chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
|
||||
hierarchy -top top
|
||||
proc
|
||||
# equivalence checking is somewhat slow (and missing simulation models)
|
||||
synth_gowin -family gw1n
|
||||
cd top # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:MULT9X9
|
||||
|
||||
|
||||
# Make sure that DSPs are not inferred with -nodsp option
|
||||
design -reset
|
||||
read_verilog ../common/mul.v
|
||||
chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
|
||||
hierarchy -top top
|
||||
proc
|
||||
synth_gowin -family gw1n -nodsp
|
||||
cd top # Constrain all select calls below inside the top module
|
||||
select -assert-none t:MULT9X9
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/mul.v
|
||||
chparam -set X_WIDTH 16 -set Y_WIDTH 16 -set A_WIDTH 32
|
||||
hierarchy -top top
|
||||
proc
|
||||
synth_gowin -family gw1n
|
||||
cd top # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:MULT18X18
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/mul.v
|
||||
chparam -set X_WIDTH 32 -set Y_WIDTH 32 -set A_WIDTH 64
|
||||
hierarchy -top top
|
||||
proc
|
||||
# equivalence checking is too slow here
|
||||
synth_gowin
|
||||
cd top # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:MULT36X36
|
||||
|
||||
|
||||
# We end up with two 18x18 multipliers
|
||||
# 36x36 min width is 22
|
||||
design -reset
|
||||
read_verilog ../common/mul.v
|
||||
chparam -set X_WIDTH 32 -set Y_WIDTH 16 -set A_WIDTH 48
|
||||
hierarchy -top top
|
||||
proc
|
||||
# equivalence checking is too slow here
|
||||
synth_gowin
|
||||
cd top # Constrain all select calls below inside the top module
|
||||
select -assert-count 2 t:MULT18X18
|
||||
53
tests/arch/gowin/mul_gw2a.ys
Normal file
53
tests/arch/gowin/mul_gw2a.ys
Normal file
|
|
@ -0,0 +1,53 @@
|
|||
read_verilog ../common/mul.v
|
||||
chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
|
||||
hierarchy -top top
|
||||
proc
|
||||
# equivalence checking is somewhat slow (and missing simulation models)
|
||||
synth_gowin -family gw2a
|
||||
cd top # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:MULT9X9
|
||||
|
||||
|
||||
# Make sure that DSPs are not inferred with -nodsp option
|
||||
design -reset
|
||||
read_verilog ../common/mul.v
|
||||
chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
|
||||
hierarchy -top top
|
||||
proc
|
||||
synth_gowin -family gw2a -nodsp
|
||||
cd top # Constrain all select calls below inside the top module
|
||||
select -assert-none t:MULT9X9
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/mul.v
|
||||
chparam -set X_WIDTH 16 -set Y_WIDTH 16 -set A_WIDTH 32
|
||||
hierarchy -top top
|
||||
proc
|
||||
synth_gowin -family gw2a
|
||||
cd top # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:MULT18X18
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/mul.v
|
||||
chparam -set X_WIDTH 32 -set Y_WIDTH 32 -set A_WIDTH 64
|
||||
hierarchy -top top
|
||||
proc
|
||||
# equivalence checking is too slow here
|
||||
synth_gowin -family gw2a
|
||||
cd top # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:MULT36X36
|
||||
|
||||
|
||||
# We end up with two 18x18 multipliers
|
||||
# 36x36 min width is 22
|
||||
design -reset
|
||||
read_verilog ../common/mul.v
|
||||
chparam -set X_WIDTH 32 -set Y_WIDTH 16 -set A_WIDTH 48
|
||||
hierarchy -top top
|
||||
proc
|
||||
# equivalence checking is too slow here
|
||||
synth_gowin -family gw2a
|
||||
cd top # Constrain all select calls below inside the top module
|
||||
select -assert-count 2 t:MULT18X18
|
||||
|
|
@ -12,5 +12,5 @@ cd fsm # Constrain all select calls below inside the top module
|
|||
|
||||
select -assert-count 4 t:SB_DFF
|
||||
select -assert-count 2 t:SB_DFFESR
|
||||
select -assert-max 15 t:SB_LUT4
|
||||
select -assert-max 16 t:SB_LUT4
|
||||
select -assert-none t:SB_DFFESR t:SB_DFF t:SB_LUT4 %% t:* %D
|
||||
|
|
|
|||
|
|
@ -74,6 +74,7 @@ EOT
|
|||
|
||||
techmap -wb -D EQUIV -autoproc -map +/ice40/cells_sim.v
|
||||
|
||||
async2sync
|
||||
equiv_make top ref equiv
|
||||
select -assert-any -module equiv t:$equiv
|
||||
equiv_induct
|
||||
|
|
|
|||
29
tests/arch/xilinx/dsp_preadder_sub.ys
Normal file
29
tests/arch/xilinx/dsp_preadder_sub.ys
Normal file
|
|
@ -0,0 +1,29 @@
|
|||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [7:0] A,
|
||||
input signed [7:0] D,
|
||||
input signed [7:0] B,
|
||||
output signed [16:0] P
|
||||
);
|
||||
assign P = (A - D) * B;
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
proc
|
||||
design -save gold
|
||||
synth_xilinx -noiopad
|
||||
design -save gate
|
||||
cd top
|
||||
select -assert-count 1 t:DSP48E1
|
||||
select -assert-count 1 t:DSP48E1 r:USE_DPORT=TRUE %i
|
||||
select -assert-none t:DSP48E1 %% t:* %D
|
||||
|
||||
# Now prove functional equivalence of the mapped netlist against the original
|
||||
# (saved as `gold` above).
|
||||
design -reset
|
||||
design -copy-from gold -as gold top
|
||||
design -copy-from gate -as gate top
|
||||
techmap -wb -D EQUIV -autoproc -map +/xilinx/cells_sim.v
|
||||
equiv_make gold gate equiv
|
||||
equiv_induct equiv
|
||||
equiv_status -assert equiv
|
||||
1
tests/blif/.gitignore
vendored
Normal file
1
tests/blif/.gitignore
vendored
Normal file
|
|
@ -0,0 +1 @@
|
|||
/*.out
|
||||
480
tests/blif/gatesi.blif
Normal file
480
tests/blif/gatesi.blif
Normal file
|
|
@ -0,0 +1,480 @@
|
|||
# Generated by Yosys 0.60+88 (git sha1 69b604104, g++ 15.2.1 -fPIC -O3)
|
||||
|
||||
.model test
|
||||
.inputs clk in_a_var[0] in_a_var[1] in_a_var[2] in_a_var[3] in_a_var[4] in_a_var[5] in_a_var[6] in_a_var[7] in_b_var[0] in_b_var[1] in_b_var[2] in_b_var[3] in_b_var[4] in_b_var[5] in_b_var[6] in_b_var[7]
|
||||
.outputs out_var[0] out_var[1] out_var[2] out_var[3] out_var[4] out_var[5] out_var[6] out_var[7]
|
||||
.gate ORNOT A=:1.test_1[0] B=in_a_var[0] Y=$abc$2385$new_n57
|
||||
.gate ORNOT A=in_a_var[0] B=:1.test_1[0] Y=$abc$2385$new_n58
|
||||
.gate XNOR A=:1.test_1[0] B=in_a_var[0] Y=$abc$2385$new_n59
|
||||
.gate NAND A=in_b_var[0] B=$abc$2385$new_n59 Y=$abc$2385$new_n60
|
||||
.gate XOR A=in_b_var[0] B=$abc$2385$new_n59 Y=$abc$2385$auto$maccmap.cc:114:fulladd$252.Y[0]
|
||||
.gate NAND A=$abc$2385$new_n57 B=$abc$2385$new_n60 Y=$abc$2385$new_n62
|
||||
.gate NOR A=:1.test_1[0] B=:1.test_1[1] Y=$abc$2385$new_n63
|
||||
.gate AND A=:1.test_1[0] B=:1.test_1[1] Y=$abc$2385$new_n64
|
||||
.gate XOR A=:1.test_1[0] B=:1.test_1[1] Y=$abc$2385$new_n65
|
||||
.gate NOT A=$abc$2385$new_n65 Y=$abc$2385$new_n66
|
||||
.gate AND A=:1.test_1[2] B=$abc$2385$new_n64 Y=$abc$2385$new_n67
|
||||
.gate AND A=:1.test_1[3] B=$abc$2385$new_n67 Y=$abc$2385$new_n68
|
||||
.gate AND A=:1.test_1[4] B=$abc$2385$new_n68 Y=$abc$2385$new_n69
|
||||
.gate AND A=:1.test_1[5] B=$abc$2385$new_n69 Y=$abc$2385$new_n70
|
||||
.gate AND A=:1.test_1[6] B=$abc$2385$new_n70 Y=$abc$2385$new_n71
|
||||
.gate XNOR A=:1.test_1[6] B=$abc$2385$new_n70 Y=$abc$2385$new_n72
|
||||
.gate NOT A=$abc$2385$new_n72 Y=$abc$2385$new_n73
|
||||
.gate AND A=:1.test_1[7] B=$abc$2385$new_n71 Y=$abc$2385$new_n74
|
||||
.gate XNOR A=:1.test_1[7] B=$abc$2385$new_n71 Y=$abc$2385$new_n75
|
||||
.gate ANDNOT A=:1.test_1[5] B=$abc$2385$new_n69 Y=$abc$2385$new_n76
|
||||
.gate XNOR A=:1.test_1[5] B=$abc$2385$new_n69 Y=$abc$2385$new_n77
|
||||
.gate NOR A=:1.test_1[3] B=:1.test_1[4] Y=$abc$2385$new_n78
|
||||
.gate AND A=$abc$2385$new_n63 B=$abc$2385$new_n78 Y=$abc$2385$new_n79
|
||||
.gate ANDNOT A=$abc$2385$new_n79 B=:1.test_1[2] Y=$abc$2385$new_n80
|
||||
.gate AND A=$abc$2385$new_n77 B=$abc$2385$new_n80 Y=$abc$2385$new_n81
|
||||
.gate NAND A=$abc$2385$new_n75 B=$abc$2385$new_n81 Y=$abc$2385$new_n82
|
||||
.gate OR A=$abc$2385$new_n73 B=$abc$2385$new_n82 Y=$abc$2385$new_n83
|
||||
.gate AND A=$abc$2385$new_n66 B=$abc$2385$new_n83 Y=$abc$2385$new_n84
|
||||
.gate ORNOT A=$abc$2385$new_n84 B=in_a_var[1] Y=$abc$2385$new_n85
|
||||
.gate XNOR A=in_a_var[1] B=$abc$2385$new_n84 Y=$abc$2385$new_n86
|
||||
.gate NAND A=in_b_var[1] B=$abc$2385$new_n86 Y=$abc$2385$new_n87
|
||||
.gate XNOR A=in_b_var[1] B=$abc$2385$new_n86 Y=$abc$2385$new_n88
|
||||
.gate ANDNOT A=$abc$2385$new_n62 B=$abc$2385$new_n88 Y=$abc$2385$new_n89
|
||||
.gate AND A=$abc$2385$new_n85 B=$abc$2385$new_n87 Y=$abc$2385$new_n90
|
||||
.gate XNOR A=:1.test_1[2] B=$abc$2385$new_n64 Y=$abc$2385$new_n91
|
||||
.gate AND A=$abc$2385$new_n83 B=$abc$2385$new_n91 Y=$abc$2385$new_n92
|
||||
.gate ORNOT A=$abc$2385$new_n92 B=in_a_var[2] Y=$abc$2385$new_n93
|
||||
.gate XNOR A=in_a_var[2] B=$abc$2385$new_n92 Y=$abc$2385$new_n94
|
||||
.gate NAND A=in_b_var[2] B=$abc$2385$new_n94 Y=$abc$2385$new_n95
|
||||
.gate XNOR A=in_b_var[2] B=$abc$2385$new_n94 Y=$abc$2385$new_n96
|
||||
.gate OR A=$abc$2385$new_n90 B=$abc$2385$new_n96 Y=$abc$2385$new_n97
|
||||
.gate XOR A=$abc$2385$new_n90 B=$abc$2385$new_n96 Y=$abc$2385$new_n98
|
||||
.gate NAND A=$abc$2385$new_n89 B=$abc$2385$new_n98 Y=$abc$2385$new_n99
|
||||
.gate XOR A=$abc$2385$new_n89 B=$abc$2385$new_n98 Y=$abc$2385$auto$maccmap.cc:240:synth$253.Y[2]
|
||||
.gate NAND A=$abc$2385$new_n97 B=$abc$2385$new_n99 Y=$abc$2385$new_n101
|
||||
.gate AND A=$abc$2385$new_n93 B=$abc$2385$new_n95 Y=$abc$2385$new_n102
|
||||
.gate XNOR A=:1.test_1[3] B=$abc$2385$new_n67 Y=$abc$2385$new_n103
|
||||
.gate AND A=$abc$2385$new_n83 B=$abc$2385$new_n103 Y=$abc$2385$new_n104
|
||||
.gate ORNOT A=$abc$2385$new_n104 B=in_a_var[3] Y=$abc$2385$new_n105
|
||||
.gate XNOR A=in_a_var[3] B=$abc$2385$new_n104 Y=$abc$2385$new_n106
|
||||
.gate NAND A=in_b_var[3] B=$abc$2385$new_n106 Y=$abc$2385$new_n107
|
||||
.gate XNOR A=in_b_var[3] B=$abc$2385$new_n106 Y=$abc$2385$new_n108
|
||||
.gate OR A=$abc$2385$new_n102 B=$abc$2385$new_n108 Y=$abc$2385$new_n109
|
||||
.gate XOR A=$abc$2385$new_n102 B=$abc$2385$new_n108 Y=$abc$2385$new_n110
|
||||
.gate NAND A=$abc$2385$new_n101 B=$abc$2385$new_n110 Y=$abc$2385$new_n111
|
||||
.gate XOR A=$abc$2385$new_n101 B=$abc$2385$new_n110 Y=$abc$2385$auto$maccmap.cc:240:synth$253.Y[3]
|
||||
.gate NAND A=$abc$2385$new_n109 B=$abc$2385$new_n111 Y=$abc$2385$new_n113
|
||||
.gate AND A=$abc$2385$new_n105 B=$abc$2385$new_n107 Y=$abc$2385$new_n114
|
||||
.gate XNOR A=:1.test_1[4] B=$abc$2385$new_n68 Y=$abc$2385$new_n115
|
||||
.gate AND A=$abc$2385$new_n83 B=$abc$2385$new_n115 Y=$abc$2385$new_n116
|
||||
.gate ORNOT A=$abc$2385$new_n116 B=in_a_var[4] Y=$abc$2385$new_n117
|
||||
.gate XNOR A=in_a_var[4] B=$abc$2385$new_n116 Y=$abc$2385$new_n118
|
||||
.gate NAND A=in_b_var[4] B=$abc$2385$new_n118 Y=$abc$2385$new_n119
|
||||
.gate XNOR A=in_b_var[4] B=$abc$2385$new_n118 Y=$abc$2385$new_n120
|
||||
.gate OR A=$abc$2385$new_n114 B=$abc$2385$new_n120 Y=$abc$2385$new_n121
|
||||
.gate XOR A=$abc$2385$new_n114 B=$abc$2385$new_n120 Y=$abc$2385$new_n122
|
||||
.gate NAND A=$abc$2385$new_n113 B=$abc$2385$new_n122 Y=$abc$2385$new_n123
|
||||
.gate XOR A=$abc$2385$new_n113 B=$abc$2385$new_n122 Y=$abc$2385$auto$maccmap.cc:240:synth$253.Y[4]
|
||||
.gate AND A=$abc$2385$new_n121 B=$abc$2385$new_n123 Y=$abc$2385$new_n125
|
||||
.gate AND A=$abc$2385$new_n117 B=$abc$2385$new_n119 Y=$abc$2385$new_n126
|
||||
.gate AND A=$abc$2385$new_n77 B=$abc$2385$new_n83 Y=$abc$2385$new_n127
|
||||
.gate ORNOT A=$abc$2385$new_n127 B=in_a_var[5] Y=$abc$2385$new_n128
|
||||
.gate XNOR A=in_a_var[5] B=$abc$2385$new_n127 Y=$abc$2385$new_n129
|
||||
.gate NAND A=in_b_var[5] B=$abc$2385$new_n129 Y=$abc$2385$new_n130
|
||||
.gate XNOR A=in_b_var[5] B=$abc$2385$new_n129 Y=$abc$2385$new_n131
|
||||
.gate OR A=$abc$2385$new_n126 B=$abc$2385$new_n131 Y=$abc$2385$new_n132
|
||||
.gate NAND A=$abc$2385$new_n126 B=$abc$2385$new_n131 Y=$abc$2385$new_n133
|
||||
.gate XOR A=$abc$2385$new_n126 B=$abc$2385$new_n131 Y=$abc$2385$new_n134
|
||||
.gate XNOR A=$abc$2385$new_n125 B=$abc$2385$new_n134 Y=$abc$2385$auto$maccmap.cc:240:synth$253.Y[5]
|
||||
.gate AND A=$abc$2385$new_n128 B=$abc$2385$new_n130 Y=$abc$2385$new_n136
|
||||
.gate AND A=$abc$2385$new_n72 B=$abc$2385$new_n82 Y=$abc$2385$new_n137
|
||||
.gate ORNOT A=$abc$2385$new_n137 B=in_a_var[6] Y=$abc$2385$new_n138
|
||||
.gate XNOR A=in_a_var[6] B=$abc$2385$new_n137 Y=$abc$2385$new_n139
|
||||
.gate NAND A=in_b_var[6] B=$abc$2385$new_n139 Y=$abc$2385$new_n140
|
||||
.gate XNOR A=in_b_var[6] B=$abc$2385$new_n139 Y=$abc$2385$new_n141
|
||||
.gate OR A=$abc$2385$new_n136 B=$abc$2385$new_n141 Y=$abc$2385$new_n142
|
||||
.gate XOR A=$abc$2385$new_n136 B=$abc$2385$new_n141 Y=$abc$2385$new_n143
|
||||
.gate NAND A=$abc$2385$new_n125 B=$abc$2385$new_n132 Y=$abc$2385$new_n144
|
||||
.gate AND A=$abc$2385$new_n133 B=$abc$2385$new_n144 Y=$abc$2385$new_n145
|
||||
.gate NAND A=$abc$2385$new_n143 B=$abc$2385$new_n145 Y=$abc$2385$new_n146
|
||||
.gate XOR A=$abc$2385$new_n143 B=$abc$2385$new_n145 Y=$abc$2385$auto$maccmap.cc:240:synth$253.Y[6]
|
||||
.gate AND A=$abc$2385$new_n142 B=$abc$2385$new_n146 Y=$abc$2385$new_n148
|
||||
.gate AND A=$abc$2385$new_n138 B=$abc$2385$new_n140 Y=$abc$2385$new_n149
|
||||
.gate AND A=$abc$2385$new_n75 B=$abc$2385$new_n83 Y=$abc$2385$new_n150
|
||||
.gate NOR A=in_b_var[7] B=in_a_var[7] Y=$abc$2385$new_n151
|
||||
.gate XOR A=in_b_var[7] B=in_a_var[7] Y=$abc$2385$new_n152
|
||||
.gate XNOR A=$abc$2385$new_n150 B=$abc$2385$new_n152 Y=$abc$2385$new_n153
|
||||
.gate XNOR A=$abc$2385$new_n149 B=$abc$2385$new_n153 Y=$abc$2385$new_n154
|
||||
.gate XNOR A=$abc$2385$new_n148 B=$abc$2385$new_n154 Y=$abc$2385$auto$maccmap.cc:240:synth$253.Y[7]
|
||||
.gate XNOR A=$abc$2385$new_n62 B=$abc$2385$new_n88 Y=$abc$2385$auto$maccmap.cc:240:synth$253.P[1]
|
||||
.gate NAND A=:1.test_1[0] B=:1.test_2[0] Y=$abc$2385$new_n157
|
||||
.gate ANDNOT A=:1.test_2[0] B=$abc$2385$new_n91 Y=$abc$2385$new_n158
|
||||
.gate ANDNOT A=:1.test_2[1] B=$abc$2385$new_n64 Y=$abc$2385$new_n159
|
||||
.gate AND A=:1.test_2[1] B=$abc$2385$new_n65 Y=$abc$2385$new_n160
|
||||
.gate ORNOT A=$abc$2385$new_n160 B=:1.test_1[0] Y=$abc$2385$new_n161
|
||||
.gate AND A=:1.test_2[2] B=$abc$2385$new_n161 Y=$abc$2385$new_n162
|
||||
.gate ANDNOT A=:1.test_1[1] B=:1.test_1[0] Y=$abc$2385$new_n163
|
||||
.gate ANDNOT A=:1.test_2[2] B=:1.test_1[0] Y=$abc$2385$new_n164
|
||||
.gate XNOR A=$abc$2385$new_n160 B=$abc$2385$new_n164 Y=$abc$2385$new_n165
|
||||
.gate MUX A=$abc$2385$new_n160 B=$abc$2385$new_n165 S=:1.test_2[2] Y=$abc$2385$new_n166
|
||||
.gate ORNOT A=:1.test_2[0] B=:1.test_1[0] Y=$abc$2385$new_n167
|
||||
.gate AND A=$abc$2385$new_n159 B=$abc$2385$new_n167 Y=$abc$2385$new_n168
|
||||
.gate AND A=$abc$2385$new_n166 B=$abc$2385$new_n168 Y=$abc$2385$new_n169
|
||||
.gate XOR A=$abc$2385$new_n166 B=$abc$2385$new_n168 Y=$abc$2385$new_n170
|
||||
.gate AND A=$abc$2385$new_n158 B=$abc$2385$new_n170 Y=$abc$2385$new_n171
|
||||
.gate ANDNOT A=:1.test_2[0] B=$abc$2385$new_n103 Y=$abc$2385$new_n172
|
||||
.gate ANDNOT A=:1.test_2[1] B=$abc$2385$new_n91 Y=$abc$2385$new_n173
|
||||
.gate ANDNOT A=:1.test_2[1] B=$abc$2385$new_n103 Y=$abc$2385$new_n174
|
||||
.gate AND A=$abc$2385$new_n158 B=$abc$2385$new_n174 Y=$abc$2385$new_n175
|
||||
.gate XOR A=$abc$2385$new_n172 B=$abc$2385$new_n173 Y=$abc$2385$new_n176
|
||||
.gate NAND A=:1.test_2[2] B=$abc$2385$new_n65 Y=$abc$2385$new_n177
|
||||
.gate AND A=:1.test_1[0] B=:1.test_2[3] Y=$abc$2385$new_n178
|
||||
.gate NAND A=:1.test_1[0] B=$abc$2385$new_n177 Y=$abc$2385$new_n179
|
||||
.gate XNOR A=$abc$2385$new_n177 B=$abc$2385$new_n178 Y=$abc$2385$new_n180
|
||||
.gate NAND A=$abc$2385$new_n162 B=$abc$2385$new_n180 Y=$abc$2385$new_n181
|
||||
.gate XOR A=$abc$2385$new_n162 B=$abc$2385$new_n180 Y=$abc$2385$new_n182
|
||||
.gate NAND A=$abc$2385$new_n176 B=$abc$2385$new_n182 Y=$abc$2385$new_n183
|
||||
.gate XOR A=$abc$2385$new_n176 B=$abc$2385$new_n182 Y=$abc$2385$new_n184
|
||||
.gate NAND A=$abc$2385$new_n171 B=$abc$2385$new_n184 Y=$abc$2385$new_n185
|
||||
.gate XOR A=$abc$2385$new_n171 B=$abc$2385$new_n184 Y=$abc$2385$new_n186
|
||||
.gate NAND A=$abc$2385$new_n169 B=$abc$2385$new_n186 Y=$abc$2385$new_n187
|
||||
.gate NAND A=$abc$2385$new_n185 B=$abc$2385$new_n187 Y=$abc$2385$new_n188
|
||||
.gate ANDNOT A=:1.test_2[0] B=$abc$2385$new_n115 Y=$abc$2385$new_n189
|
||||
.gate ANDNOT A=:1.test_2[1] B=$abc$2385$new_n115 Y=$abc$2385$new_n190
|
||||
.gate NAND A=$abc$2385$new_n172 B=$abc$2385$new_n190 Y=$abc$2385$new_n191
|
||||
.gate XOR A=$abc$2385$new_n174 B=$abc$2385$new_n189 Y=$abc$2385$new_n192
|
||||
.gate ANDNOT A=:1.test_2[2] B=$abc$2385$new_n91 Y=$abc$2385$new_n193
|
||||
.gate NAND A=$abc$2385$new_n192 B=$abc$2385$new_n193 Y=$abc$2385$new_n194
|
||||
.gate XOR A=$abc$2385$new_n192 B=$abc$2385$new_n193 Y=$abc$2385$new_n195
|
||||
.gate AND A=:1.test_2[3] B=$abc$2385$new_n179 Y=$abc$2385$new_n196
|
||||
.gate NAND A=:1.test_2[3] B=$abc$2385$new_n65 Y=$abc$2385$new_n197
|
||||
.gate NAND A=:1.test_1[0] B=$abc$2385$new_n197 Y=$abc$2385$new_n198
|
||||
.gate AND A=:1.test_2[4] B=$abc$2385$new_n198 Y=$abc$2385$new_n199
|
||||
.gate NAND A=:1.test_2[3] B=$abc$2385$new_n163 Y=$abc$2385$new_n200
|
||||
.gate NAND A=$abc$2385$new_n199 B=$abc$2385$new_n200 Y=$abc$2385$new_n201
|
||||
.gate ORNOT A=:1.test_2[4] B=$abc$2385$new_n197 Y=$abc$2385$new_n202
|
||||
.gate AND A=$abc$2385$new_n201 B=$abc$2385$new_n202 Y=$abc$2385$new_n203
|
||||
.gate NAND A=$abc$2385$new_n175 B=$abc$2385$new_n203 Y=$abc$2385$new_n204
|
||||
.gate XOR A=$abc$2385$new_n175 B=$abc$2385$new_n203 Y=$abc$2385$new_n205
|
||||
.gate NAND A=$abc$2385$new_n196 B=$abc$2385$new_n205 Y=$abc$2385$new_n206
|
||||
.gate XOR A=$abc$2385$new_n196 B=$abc$2385$new_n205 Y=$abc$2385$new_n207
|
||||
.gate AND A=$abc$2385$new_n195 B=$abc$2385$new_n207 Y=$abc$2385$new_n208
|
||||
.gate XOR A=$abc$2385$new_n195 B=$abc$2385$new_n207 Y=$abc$2385$new_n209
|
||||
.gate NAND A=$abc$2385$new_n181 B=$abc$2385$new_n183 Y=$abc$2385$new_n210
|
||||
.gate AND A=$abc$2385$new_n209 B=$abc$2385$new_n210 Y=$abc$2385$new_n211
|
||||
.gate XOR A=$abc$2385$new_n209 B=$abc$2385$new_n210 Y=$abc$2385$new_n212
|
||||
.gate AND A=$abc$2385$new_n188 B=$abc$2385$new_n212 Y=$abc$2385$new_n213
|
||||
.gate ANDNOT A=:1.test_2[0] B=$abc$2385$new_n77 Y=$abc$2385$new_n214
|
||||
.gate ANDNOT A=:1.test_2[3] B=$abc$2385$new_n91 Y=$abc$2385$new_n215
|
||||
.gate ANDNOT A=:1.test_2[2] B=$abc$2385$new_n103 Y=$abc$2385$new_n216
|
||||
.gate ANDNOT A=:1.test_2[2] B=$abc$2385$new_n115 Y=$abc$2385$new_n217
|
||||
.gate NAND A=$abc$2385$new_n174 B=$abc$2385$new_n217 Y=$abc$2385$new_n218
|
||||
.gate XOR A=$abc$2385$new_n190 B=$abc$2385$new_n216 Y=$abc$2385$new_n219
|
||||
.gate NAND A=$abc$2385$new_n215 B=$abc$2385$new_n219 Y=$abc$2385$new_n220
|
||||
.gate XOR A=$abc$2385$new_n215 B=$abc$2385$new_n219 Y=$abc$2385$new_n221
|
||||
.gate AND A=$abc$2385$new_n214 B=$abc$2385$new_n221 Y=$abc$2385$new_n222
|
||||
.gate XOR A=$abc$2385$new_n214 B=$abc$2385$new_n221 Y=$abc$2385$new_n223
|
||||
.gate NAND A=:1.test_2[4] B=$abc$2385$new_n65 Y=$abc$2385$new_n224
|
||||
.gate NAND A=:1.test_1[0] B=$abc$2385$new_n224 Y=$abc$2385$new_n225
|
||||
.gate AND A=:1.test_2[5] B=$abc$2385$new_n225 Y=$abc$2385$new_n226
|
||||
.gate NAND A=:1.test_2[4] B=$abc$2385$new_n163 Y=$abc$2385$new_n227
|
||||
.gate NAND A=$abc$2385$new_n226 B=$abc$2385$new_n227 Y=$abc$2385$new_n228
|
||||
.gate ORNOT A=:1.test_2[5] B=$abc$2385$new_n224 Y=$abc$2385$new_n229
|
||||
.gate AND A=$abc$2385$new_n228 B=$abc$2385$new_n229 Y=$abc$2385$new_n230
|
||||
.gate NAND A=$abc$2385$new_n191 B=$abc$2385$new_n194 Y=$abc$2385$new_n231
|
||||
.gate NAND A=$abc$2385$new_n230 B=$abc$2385$new_n231 Y=$abc$2385$new_n232
|
||||
.gate XOR A=$abc$2385$new_n230 B=$abc$2385$new_n231 Y=$abc$2385$new_n233
|
||||
.gate NAND A=$abc$2385$new_n199 B=$abc$2385$new_n233 Y=$abc$2385$new_n234
|
||||
.gate XOR A=$abc$2385$new_n199 B=$abc$2385$new_n233 Y=$abc$2385$new_n235
|
||||
.gate AND A=$abc$2385$new_n223 B=$abc$2385$new_n235 Y=$abc$2385$new_n236
|
||||
.gate XOR A=$abc$2385$new_n223 B=$abc$2385$new_n235 Y=$abc$2385$new_n237
|
||||
.gate NAND A=$abc$2385$new_n208 B=$abc$2385$new_n237 Y=$abc$2385$new_n238
|
||||
.gate XOR A=$abc$2385$new_n208 B=$abc$2385$new_n237 Y=$abc$2385$new_n239
|
||||
.gate NAND A=$abc$2385$new_n204 B=$abc$2385$new_n206 Y=$abc$2385$new_n240
|
||||
.gate NAND A=$abc$2385$new_n239 B=$abc$2385$new_n240 Y=$abc$2385$new_n241
|
||||
.gate XOR A=$abc$2385$new_n239 B=$abc$2385$new_n240 Y=$abc$2385$new_n242
|
||||
.gate AND A=$abc$2385$new_n211 B=$abc$2385$new_n242 Y=$abc$2385$new_n243
|
||||
.gate XOR A=$abc$2385$new_n211 B=$abc$2385$new_n242 Y=$abc$2385$new_n244
|
||||
.gate NAND A=$abc$2385$new_n213 B=$abc$2385$new_n244 Y=$abc$2385$new_n245
|
||||
.gate AND A=:1.test_2[0] B=$abc$2385$new_n163 Y=$abc$2385$new_n246
|
||||
.gate NAND A=:1.test_2[0] B=$abc$2385$new_n163 Y=$abc$2385$new_n247
|
||||
.gate XOR A=$abc$2385$new_n158 B=$abc$2385$new_n170 Y=$abc$2385$new_n248
|
||||
.gate AND A=$abc$2385$new_n246 B=$abc$2385$new_n248 Y=$abc$2385$new_n249
|
||||
.gate XOR A=$abc$2385$new_n169 B=$abc$2385$new_n186 Y=$abc$2385$new_n250
|
||||
.gate AND A=$abc$2385$new_n249 B=$abc$2385$new_n250 Y=$abc$2385$new_n251
|
||||
.gate XOR A=$abc$2385$new_n188 B=$abc$2385$new_n212 Y=$abc$2385$new_n252
|
||||
.gate AND A=$abc$2385$new_n251 B=$abc$2385$new_n252 Y=$abc$2385$new_n253
|
||||
.gate NAND A=$abc$2385$new_n244 B=$abc$2385$new_n253 Y=$abc$2385$new_n254
|
||||
.gate XNOR A=$abc$2385$new_n213 B=$abc$2385$new_n244 Y=$abc$2385$new_n255
|
||||
.gate NAND A=$abc$2385$new_n245 B=$abc$2385$new_n254 Y=$abc$2385$new_n256
|
||||
.gate NAND A=$abc$2385$new_n238 B=$abc$2385$new_n241 Y=$abc$2385$new_n257
|
||||
.gate ANDNOT A=:1.test_2[0] B=$abc$2385$new_n72 Y=$abc$2385$new_n258
|
||||
.gate ORNOT A=$abc$2385$new_n77 B=:1.test_2[1] Y=$abc$2385$new_n259
|
||||
.gate ANDNOT A=:1.test_2[1] B=$abc$2385$new_n72 Y=$abc$2385$new_n260
|
||||
.gate NAND A=$abc$2385$new_n214 B=$abc$2385$new_n260 Y=$abc$2385$new_n261
|
||||
.gate XNOR A=$abc$2385$new_n258 B=$abc$2385$new_n259 Y=$abc$2385$new_n262
|
||||
.gate ANDNOT A=:1.test_2[4] B=$abc$2385$new_n91 Y=$abc$2385$new_n263
|
||||
.gate ANDNOT A=:1.test_2[3] B=$abc$2385$new_n103 Y=$abc$2385$new_n264
|
||||
.gate ANDNOT A=:1.test_2[3] B=$abc$2385$new_n115 Y=$abc$2385$new_n265
|
||||
.gate NAND A=$abc$2385$new_n216 B=$abc$2385$new_n265 Y=$abc$2385$new_n266
|
||||
.gate XOR A=$abc$2385$new_n217 B=$abc$2385$new_n264 Y=$abc$2385$new_n267
|
||||
.gate NAND A=$abc$2385$new_n263 B=$abc$2385$new_n267 Y=$abc$2385$new_n268
|
||||
.gate XOR A=$abc$2385$new_n263 B=$abc$2385$new_n267 Y=$abc$2385$new_n269
|
||||
.gate AND A=$abc$2385$new_n262 B=$abc$2385$new_n269 Y=$abc$2385$new_n270
|
||||
.gate XOR A=$abc$2385$new_n262 B=$abc$2385$new_n269 Y=$abc$2385$new_n271
|
||||
.gate NAND A=$abc$2385$new_n222 B=$abc$2385$new_n271 Y=$abc$2385$new_n272
|
||||
.gate XOR A=$abc$2385$new_n222 B=$abc$2385$new_n271 Y=$abc$2385$new_n273
|
||||
.gate NAND A=:1.test_2[5] B=$abc$2385$new_n65 Y=$abc$2385$new_n274
|
||||
.gate NAND A=:1.test_1[0] B=$abc$2385$new_n274 Y=$abc$2385$new_n275
|
||||
.gate AND A=:1.test_2[6] B=$abc$2385$new_n275 Y=$abc$2385$new_n276
|
||||
.gate NAND A=:1.test_2[5] B=$abc$2385$new_n163 Y=$abc$2385$new_n277
|
||||
.gate NAND A=:1.test_2[6] B=$abc$2385$new_n65 Y=$abc$2385$new_n278
|
||||
.gate NAND A=$abc$2385$new_n276 B=$abc$2385$new_n277 Y=$abc$2385$new_n279
|
||||
.gate ORNOT A=:1.test_2[6] B=$abc$2385$new_n274 Y=$abc$2385$new_n280
|
||||
.gate AND A=$abc$2385$new_n279 B=$abc$2385$new_n280 Y=$abc$2385$new_n281
|
||||
.gate NAND A=$abc$2385$new_n218 B=$abc$2385$new_n220 Y=$abc$2385$new_n282
|
||||
.gate NAND A=$abc$2385$new_n281 B=$abc$2385$new_n282 Y=$abc$2385$new_n283
|
||||
.gate XOR A=$abc$2385$new_n281 B=$abc$2385$new_n282 Y=$abc$2385$new_n284
|
||||
.gate NAND A=$abc$2385$new_n226 B=$abc$2385$new_n284 Y=$abc$2385$new_n285
|
||||
.gate XOR A=$abc$2385$new_n226 B=$abc$2385$new_n284 Y=$abc$2385$new_n286
|
||||
.gate NAND A=$abc$2385$new_n273 B=$abc$2385$new_n286 Y=$abc$2385$new_n287
|
||||
.gate XOR A=$abc$2385$new_n273 B=$abc$2385$new_n286 Y=$abc$2385$new_n288
|
||||
.gate NAND A=$abc$2385$new_n236 B=$abc$2385$new_n288 Y=$abc$2385$new_n289
|
||||
.gate XOR A=$abc$2385$new_n236 B=$abc$2385$new_n288 Y=$abc$2385$new_n290
|
||||
.gate NAND A=$abc$2385$new_n232 B=$abc$2385$new_n234 Y=$abc$2385$new_n291
|
||||
.gate NAND A=$abc$2385$new_n290 B=$abc$2385$new_n291 Y=$abc$2385$new_n292
|
||||
.gate XOR A=$abc$2385$new_n290 B=$abc$2385$new_n291 Y=$abc$2385$new_n293
|
||||
.gate NAND A=$abc$2385$new_n257 B=$abc$2385$new_n293 Y=$abc$2385$new_n294
|
||||
.gate XOR A=$abc$2385$new_n257 B=$abc$2385$new_n293 Y=$abc$2385$new_n295
|
||||
.gate NAND A=$abc$2385$new_n243 B=$abc$2385$new_n295 Y=$abc$2385$new_n296
|
||||
.gate XOR A=$abc$2385$new_n243 B=$abc$2385$new_n295 Y=$abc$2385$new_n297
|
||||
.gate NAND A=$abc$2385$new_n256 B=$abc$2385$new_n297 Y=$abc$2385$new_n298
|
||||
.gate XNOR A=$abc$2385$new_n256 B=$abc$2385$new_n297 Y=$abc$2385$new_n299
|
||||
.gate NAND A=$abc$2385$new_n73 B=$abc$2385$new_n299 Y=$abc$2385$new_n300
|
||||
.gate OR A=$abc$2385$new_n73 B=$abc$2385$new_n299 Y=$abc$2385$new_n301
|
||||
.gate XOR A=$abc$2385$new_n253 B=$abc$2385$new_n255 Y=$abc$2385$new_n302
|
||||
.gate XNOR A=$abc$2385$new_n251 B=$abc$2385$new_n252 Y=$abc$2385$new_n303
|
||||
.gate XOR A=$abc$2385$new_n249 B=$abc$2385$new_n250 Y=$abc$2385$new_n304
|
||||
.gate XNOR A=$abc$2385$new_n249 B=$abc$2385$new_n250 Y=$abc$2385$new_n305
|
||||
.gate NAND A=$abc$2385$new_n103 B=$abc$2385$new_n304 Y=$abc$2385$new_n306
|
||||
.gate OR A=$abc$2385$new_n103 B=$abc$2385$new_n304 Y=$abc$2385$new_n307
|
||||
.gate XNOR A=$abc$2385$new_n247 B=$abc$2385$new_n248 Y=$abc$2385$new_n308
|
||||
.gate NAND A=:1.test_1[0] B=:1.test_2[1] Y=$abc$2385$new_n309
|
||||
.gate ANDNOT A=:1.test_2[0] B=$abc$2385$new_n64 Y=$abc$2385$new_n310
|
||||
.gate XNOR A=$abc$2385$new_n309 B=$abc$2385$new_n310 Y=$abc$2385$new_n311
|
||||
.gate NAND A=$abc$2385$new_n66 B=$abc$2385$new_n311 Y=$abc$2385$new_n312
|
||||
.gate OR A=:1.test_2[1] B=$abc$2385$new_n157 Y=$abc$2385$new_n313
|
||||
.gate NAND A=$abc$2385$new_n312 B=$abc$2385$new_n313 Y=$abc$2385$new_n314
|
||||
.gate OR A=$abc$2385$new_n308 B=$abc$2385$new_n314 Y=$abc$2385$new_n315
|
||||
.gate NAND A=$abc$2385$new_n91 B=$abc$2385$new_n315 Y=$abc$2385$new_n316
|
||||
.gate NAND A=$abc$2385$new_n308 B=$abc$2385$new_n314 Y=$abc$2385$new_n317
|
||||
.gate NAND A=$abc$2385$new_n316 B=$abc$2385$new_n317 Y=$abc$2385$new_n318
|
||||
.gate NAND A=$abc$2385$new_n307 B=$abc$2385$new_n318 Y=$abc$2385$new_n319
|
||||
.gate NAND A=$abc$2385$new_n247 B=$abc$2385$new_n311 Y=$abc$2385$new_n320
|
||||
.gate NAND A=$abc$2385$new_n306 B=$abc$2385$new_n319 Y=$abc$2385$new_n321
|
||||
.gate ORNOT A=$abc$2385$new_n115 B=$abc$2385$new_n303 Y=$abc$2385$new_n322
|
||||
.gate ORNOT A=$abc$2385$new_n303 B=$abc$2385$new_n115 Y=$abc$2385$new_n323
|
||||
.gate NAND A=$abc$2385$new_n321 B=$abc$2385$new_n322 Y=$abc$2385$new_n324
|
||||
.gate NAND A=$abc$2385$new_n323 B=$abc$2385$new_n324 Y=$abc$2385$new_n325
|
||||
.gate NAND A=$abc$2385$new_n77 B=$abc$2385$new_n325 Y=$abc$2385$new_n326
|
||||
.gate NAND A=$abc$2385$new_n302 B=$abc$2385$new_n326 Y=$abc$2385$new_n327
|
||||
.gate OR A=$abc$2385$new_n77 B=$abc$2385$new_n325 Y=$abc$2385$new_n328
|
||||
.gate AND A=$abc$2385$new_n327 B=$abc$2385$new_n328 Y=$abc$2385$new_n329
|
||||
.gate NAND A=$abc$2385$new_n300 B=$abc$2385$new_n329 Y=$abc$2385$new_n330
|
||||
.gate AND A=$abc$2385$new_n301 B=$abc$2385$new_n330 Y=$abc$2385$new_n331
|
||||
.gate NAND A=$abc$2385$new_n75 B=$abc$2385$new_n331 Y=$abc$2385$new_n332
|
||||
.gate OR A=in_b_var[5] B=$abc$2385$new_n302 Y=$abc$2385$new_n333
|
||||
.gate NAND A=in_b_var[4] B=$abc$2385$new_n303 Y=$abc$2385$new_n334
|
||||
.gate OR A=in_b_var[4] B=$abc$2385$new_n303 Y=$abc$2385$new_n335
|
||||
.gate AND A=in_b_var[1] B=$abc$2385$new_n320 Y=$abc$2385$new_n336
|
||||
.gate OR A=in_b_var[3] B=$abc$2385$new_n305 Y=$abc$2385$new_n337
|
||||
.gate ANDNOT A=in_b_var[2] B=$abc$2385$new_n308 Y=$abc$2385$new_n338
|
||||
.gate XNOR A=in_b_var[2] B=$abc$2385$new_n308 Y=$abc$2385$new_n339
|
||||
.gate NAND A=in_b_var[3] B=$abc$2385$new_n305 Y=$abc$2385$new_n340
|
||||
.gate XNOR A=in_b_var[3] B=$abc$2385$new_n304 Y=$abc$2385$new_n341
|
||||
.gate AND A=$abc$2385$new_n339 B=$abc$2385$new_n341 Y=$abc$2385$new_n342
|
||||
.gate NAND A=$abc$2385$new_n336 B=$abc$2385$new_n342 Y=$abc$2385$new_n343
|
||||
.gate NAND A=$abc$2385$new_n337 B=$abc$2385$new_n338 Y=$abc$2385$new_n344
|
||||
.gate AND A=$abc$2385$new_n340 B=$abc$2385$new_n344 Y=$abc$2385$new_n345
|
||||
.gate AND A=$abc$2385$new_n343 B=$abc$2385$new_n345 Y=$abc$2385$new_n346
|
||||
.gate AND A=in_b_var[0] B=$abc$2385$new_n157 Y=$abc$2385$new_n347
|
||||
.gate XOR A=in_b_var[1] B=$abc$2385$new_n320 Y=$abc$2385$new_n348
|
||||
.gate AND A=$abc$2385$new_n342 B=$abc$2385$new_n348 Y=$abc$2385$new_n349
|
||||
.gate NAND A=$abc$2385$new_n347 B=$abc$2385$new_n349 Y=$abc$2385$new_n350
|
||||
.gate NAND A=$abc$2385$new_n346 B=$abc$2385$new_n350 Y=$abc$2385$new_n351
|
||||
.gate NAND A=$abc$2385$new_n335 B=$abc$2385$new_n351 Y=$abc$2385$new_n352
|
||||
.gate NAND A=$abc$2385$new_n334 B=$abc$2385$new_n352 Y=$abc$2385$new_n353
|
||||
.gate NAND A=$abc$2385$new_n333 B=$abc$2385$new_n353 Y=$abc$2385$new_n354
|
||||
.gate NAND A=in_b_var[6] B=$abc$2385$new_n299 Y=$abc$2385$new_n355
|
||||
.gate NAND A=in_b_var[5] B=$abc$2385$new_n302 Y=$abc$2385$new_n356
|
||||
.gate AND A=$abc$2385$new_n355 B=$abc$2385$new_n356 Y=$abc$2385$new_n357
|
||||
.gate NAND A=$abc$2385$new_n354 B=$abc$2385$new_n357 Y=$abc$2385$new_n358
|
||||
.gate AND A=$abc$2385$new_n157 B=$abc$2385$new_n320 Y=$abc$2385$new_n359
|
||||
.gate ANDNOT A=$abc$2385$new_n359 B=$abc$2385$new_n308 Y=$abc$2385$new_n360
|
||||
.gate AND A=$abc$2385$new_n305 B=$abc$2385$new_n360 Y=$abc$2385$new_n361
|
||||
.gate AND A=$abc$2385$new_n303 B=$abc$2385$new_n361 Y=$abc$2385$new_n362
|
||||
.gate AND A=$abc$2385$new_n302 B=$abc$2385$new_n362 Y=$abc$2385$new_n363
|
||||
.gate NAND A=$abc$2385$new_n299 B=$abc$2385$new_n363 Y=$abc$2385$new_n364
|
||||
.gate AND A=$abc$2385$new_n296 B=$abc$2385$new_n298 Y=$abc$2385$new_n365
|
||||
.gate AND A=$abc$2385$new_n289 B=$abc$2385$new_n292 Y=$abc$2385$new_n366
|
||||
.gate OR A=:1.test_2[0] B=$abc$2385$new_n75 Y=$abc$2385$new_n367
|
||||
.gate AND A=$abc$2385$new_n261 B=$abc$2385$new_n367 Y=$abc$2385$new_n368
|
||||
.gate XNOR A=$abc$2385$new_n270 B=$abc$2385$new_n368 Y=$abc$2385$new_n369
|
||||
.gate XNOR A=$abc$2385$new_n276 B=$abc$2385$new_n369 Y=$abc$2385$new_n370
|
||||
.gate ANDNOT A=:1.test_2[2] B=$abc$2385$new_n77 Y=$abc$2385$new_n371
|
||||
.gate ANDNOT A=:1.test_2[5] B=$abc$2385$new_n91 Y=$abc$2385$new_n372
|
||||
.gate ANDNOT A=:1.test_2[4] B=$abc$2385$new_n103 Y=$abc$2385$new_n373
|
||||
.gate XNOR A=$abc$2385$new_n372 B=$abc$2385$new_n373 Y=$abc$2385$new_n374
|
||||
.gate XNOR A=$abc$2385$new_n371 B=$abc$2385$new_n374 Y=$abc$2385$new_n375
|
||||
.gate XOR A=$abc$2385$new_n260 B=$abc$2385$new_n265 Y=$abc$2385$new_n376
|
||||
.gate XNOR A=$abc$2385$new_n375 B=$abc$2385$new_n376 Y=$abc$2385$new_n377
|
||||
.gate NAND A=$abc$2385$new_n266 B=$abc$2385$new_n268 Y=$abc$2385$new_n378
|
||||
.gate ANDNOT A=:1.test_2[7] B=:1.test_1[0] Y=$abc$2385$new_n379
|
||||
.gate XNOR A=$abc$2385$new_n278 B=$abc$2385$new_n379 Y=$abc$2385$new_n380
|
||||
.gate XNOR A=$abc$2385$new_n75 B=$abc$2385$new_n380 Y=$abc$2385$new_n381
|
||||
.gate XNOR A=$abc$2385$new_n378 B=$abc$2385$new_n381 Y=$abc$2385$new_n382
|
||||
.gate XNOR A=$abc$2385$new_n377 B=$abc$2385$new_n382 Y=$abc$2385$new_n383
|
||||
.gate XNOR A=$abc$2385$new_n370 B=$abc$2385$new_n383 Y=$abc$2385$new_n384
|
||||
.gate NAND A=$abc$2385$new_n283 B=$abc$2385$new_n285 Y=$abc$2385$new_n385
|
||||
.gate AND A=$abc$2385$new_n272 B=$abc$2385$new_n287 Y=$abc$2385$new_n386
|
||||
.gate XNOR A=$abc$2385$new_n385 B=$abc$2385$new_n386 Y=$abc$2385$new_n387
|
||||
.gate XNOR A=$abc$2385$new_n384 B=$abc$2385$new_n387 Y=$abc$2385$new_n388
|
||||
.gate XNOR A=$abc$2385$new_n366 B=$abc$2385$new_n388 Y=$abc$2385$new_n389
|
||||
.gate XNOR A=:1.test_2[7] B=$abc$2385$new_n294 Y=$abc$2385$new_n390
|
||||
.gate XNOR A=$abc$2385$new_n389 B=$abc$2385$new_n390 Y=$abc$2385$new_n391
|
||||
.gate XNOR A=$abc$2385$new_n365 B=$abc$2385$new_n391 Y=$abc$2385$new_n392
|
||||
.gate OR A=in_b_var[6] B=$abc$2385$new_n299 Y=$abc$2385$new_n393
|
||||
.gate ORNOT A=in_b_var[6] B=in_a_var[6] Y=$abc$2385$new_n394
|
||||
.gate ORNOT A=in_a_var[5] B=in_b_var[5] Y=$abc$2385$new_n395
|
||||
.gate ORNOT A=in_b_var[5] B=in_a_var[5] Y=$abc$2385$new_n396
|
||||
.gate ORNOT A=in_b_var[4] B=in_a_var[4] Y=$abc$2385$new_n397
|
||||
.gate AND A=$abc$2385$new_n396 B=$abc$2385$new_n397 Y=$abc$2385$new_n398
|
||||
.gate ORNOT A=in_b_var[2] B=in_a_var[2] Y=$abc$2385$new_n399
|
||||
.gate ORNOT A=in_b_var[3] B=in_a_var[3] Y=$abc$2385$new_n400
|
||||
.gate NAND A=$abc$2385$new_n399 B=$abc$2385$new_n400 Y=$abc$2385$new_n401
|
||||
.gate ORNOT A=in_a_var[3] B=in_b_var[3] Y=$abc$2385$new_n402
|
||||
.gate NAND A=$abc$2385$new_n401 B=$abc$2385$new_n402 Y=$abc$2385$new_n403
|
||||
.gate ORNOT A=in_a_var[2] B=in_b_var[2] Y=$abc$2385$new_n404
|
||||
.gate NAND A=$abc$2385$new_n402 B=$abc$2385$new_n404 Y=$abc$2385$new_n405
|
||||
.gate NOR A=$abc$2385$new_n401 B=$abc$2385$new_n405 Y=$abc$2385$new_n406
|
||||
.gate ORNOT A=in_a_var[0] B=in_b_var[0] Y=$abc$2385$new_n407
|
||||
.gate ORNOT A=in_a_var[1] B=in_b_var[1] Y=$abc$2385$new_n408
|
||||
.gate NAND A=$abc$2385$new_n407 B=$abc$2385$new_n408 Y=$abc$2385$new_n409
|
||||
.gate ORNOT A=in_b_var[1] B=in_a_var[1] Y=$abc$2385$new_n410
|
||||
.gate NAND A=$abc$2385$new_n409 B=$abc$2385$new_n410 Y=$abc$2385$new_n411
|
||||
.gate NAND A=$abc$2385$new_n406 B=$abc$2385$new_n411 Y=$abc$2385$new_n412
|
||||
.gate NAND A=$abc$2385$new_n403 B=$abc$2385$new_n412 Y=$abc$2385$new_n413
|
||||
.gate ORNOT A=in_a_var[4] B=in_b_var[4] Y=$abc$2385$new_n414
|
||||
.gate NAND A=$abc$2385$new_n413 B=$abc$2385$new_n414 Y=$abc$2385$new_n415
|
||||
.gate NAND A=$abc$2385$new_n398 B=$abc$2385$new_n415 Y=$abc$2385$new_n416
|
||||
.gate NAND A=$abc$2385$new_n395 B=$abc$2385$new_n416 Y=$abc$2385$new_n417
|
||||
.gate NAND A=$abc$2385$new_n394 B=$abc$2385$new_n417 Y=$abc$2385$new_n418
|
||||
.gate NAND A=$abc$2385$new_n394 B=$abc$2385$new_n395 Y=$abc$2385$new_n419
|
||||
.gate NOR A=$abc$2385$new_n409 B=$abc$2385$new_n419 Y=$abc$2385$new_n420
|
||||
.gate AND A=$abc$2385$new_n398 B=$abc$2385$new_n420 Y=$abc$2385$new_n421
|
||||
.gate ORNOT A=in_b_var[0] B=in_a_var[0] Y=$abc$2385$new_n422
|
||||
.gate AND A=$abc$2385$new_n410 B=$abc$2385$new_n414 Y=$abc$2385$new_n423
|
||||
.gate AND A=$abc$2385$new_n422 B=$abc$2385$new_n423 Y=$abc$2385$new_n424
|
||||
.gate AND A=$abc$2385$new_n406 B=$abc$2385$new_n424 Y=$abc$2385$new_n425
|
||||
.gate NAND A=$abc$2385$new_n421 B=$abc$2385$new_n425 Y=$abc$2385$new_n426
|
||||
.gate ORNOT A=in_a_var[6] B=in_b_var[6] Y=$abc$2385$new_n427
|
||||
.gate AND A=$abc$2385$new_n151 B=$abc$2385$new_n427 Y=$abc$2385$new_n428
|
||||
.gate AND A=$abc$2385$new_n426 B=$abc$2385$new_n428 Y=$abc$2385$new_n429
|
||||
.gate AND A=$abc$2385$new_n418 B=$abc$2385$new_n429 Y=$abc$2385$new_n430
|
||||
.gate AND A=$abc$2385$new_n393 B=$abc$2385$new_n430 Y=$abc$2385$new_n431
|
||||
.gate AND A=$abc$2385$new_n392 B=$abc$2385$new_n431 Y=$abc$2385$new_n432
|
||||
.gate AND A=$abc$2385$new_n364 B=$abc$2385$new_n432 Y=$abc$2385$new_n433
|
||||
.gate AND A=$abc$2385$new_n358 B=$abc$2385$new_n433 Y=$abc$2385$new_n434
|
||||
.gate AND A=$abc$2385$new_n332 B=$abc$2385$new_n434 Y=$abc$2385$new_n435
|
||||
.gate AND A=$abc$2385$new_n157 B=$abc$2385$new_n435 Y=$abc$2385$new_n436
|
||||
.gate XNOR A=$abc$2385$new_n157 B=$abc$2385$new_n435 Y=$abc$2385$new_n437
|
||||
.gate ORNOT A=$abc$2385$new_n74 B=:1.test_1[0] Y=$abc$2385$new_n438
|
||||
.gate MUX A=:1.test_1[0] B=$abc$2385$new_n437 S=$abc$2385$new_n74 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[0]
|
||||
.gate ORNOT A=:1.test_1[1] B=$abc$2385$new_n83 Y=$abc$2385$new_n440
|
||||
.gate XNOR A=$abc$2385$new_n320 B=$abc$2385$new_n436 Y=$abc$2385$new_n441
|
||||
.gate MUX A=$abc$2385$new_n440 B=$abc$2385$new_n441 S=$abc$2385$new_n74 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[1]
|
||||
.gate ORNOT A=:1.test_1[2] B=$abc$2385$new_n83 Y=$abc$2385$new_n443
|
||||
.gate ANDNOT A=$abc$2385$new_n308 B=$abc$2385$new_n359 Y=$abc$2385$new_n444
|
||||
.gate XNOR A=$abc$2385$new_n308 B=$abc$2385$new_n359 Y=$abc$2385$new_n445
|
||||
.gate NAND A=$abc$2385$new_n435 B=$abc$2385$new_n445 Y=$abc$2385$new_n446
|
||||
.gate ORNOT A=$abc$2385$new_n435 B=$abc$2385$new_n308 Y=$abc$2385$new_n447
|
||||
.gate AND A=$abc$2385$new_n74 B=$abc$2385$new_n446 Y=$abc$2385$new_n448
|
||||
.gate NAND A=$abc$2385$new_n447 B=$abc$2385$new_n448 Y=$abc$2385$new_n449
|
||||
.gate AND A=$abc$2385$new_n443 B=$abc$2385$new_n449 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[2]
|
||||
.gate ORNOT A=:1.test_1[3] B=$abc$2385$new_n83 Y=$abc$2385$new_n451
|
||||
.gate AND A=$abc$2385$new_n435 B=$abc$2385$new_n444 Y=$abc$2385$new_n452
|
||||
.gate AND A=$abc$2385$new_n304 B=$abc$2385$new_n452 Y=$abc$2385$new_n453
|
||||
.gate XNOR A=$abc$2385$new_n305 B=$abc$2385$new_n452 Y=$abc$2385$new_n454
|
||||
.gate MUX A=$abc$2385$new_n451 B=$abc$2385$new_n454 S=$abc$2385$new_n74 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[3]
|
||||
.gate ORNOT A=:1.test_1[4] B=$abc$2385$new_n83 Y=$abc$2385$new_n456
|
||||
.gate ORNOT A=$abc$2385$new_n303 B=$abc$2385$new_n453 Y=$abc$2385$new_n457
|
||||
.gate XNOR A=$abc$2385$new_n303 B=$abc$2385$new_n453 Y=$abc$2385$new_n458
|
||||
.gate MUX A=$abc$2385$new_n456 B=$abc$2385$new_n458 S=$abc$2385$new_n74 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[4]
|
||||
.gate ORNOT A=:1.test_1[5] B=$abc$2385$new_n83 Y=$abc$2385$new_n460
|
||||
.gate OR A=$abc$2385$new_n302 B=$abc$2385$new_n457 Y=$abc$2385$new_n461
|
||||
.gate XOR A=$abc$2385$new_n302 B=$abc$2385$new_n457 Y=$abc$2385$new_n462
|
||||
.gate NAND A=$abc$2385$new_n74 B=$abc$2385$new_n462 Y=$abc$2385$new_n463
|
||||
.gate NAND A=$abc$2385$new_n460 B=$abc$2385$new_n463 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[5]
|
||||
.gate NAND A=$abc$2385$new_n299 B=$abc$2385$new_n461 Y=$abc$2385$new_n465
|
||||
.gate OR A=$abc$2385$new_n299 B=$abc$2385$new_n461 Y=$abc$2385$new_n466
|
||||
.gate AND A=$abc$2385$new_n74 B=$abc$2385$new_n466 Y=$abc$2385$new_n467
|
||||
.gate NAND A=$abc$2385$new_n465 B=$abc$2385$new_n467 Y=$abc$2385$new_n468
|
||||
.gate MUX A=$abc$2385$new_n73 B=$abc$2385$new_n137 S=$abc$2385$new_n76 Y=$abc$2385$new_n469
|
||||
.gate OR A=$abc$2385$new_n74 B=$abc$2385$new_n469 Y=$abc$2385$new_n470
|
||||
.gate NAND A=$abc$2385$new_n468 B=$abc$2385$new_n470 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[6]
|
||||
.gate NAND A=$abc$2385$new_n392 B=$abc$2385$new_n467 Y=$abc$2385$new_n472
|
||||
.gate ANDNOT A=$abc$2385$new_n137 B=$abc$2385$new_n76 Y=$abc$2385$new_n473
|
||||
.gate XNOR A=$abc$2385$new_n150 B=$abc$2385$new_n473 Y=$abc$2385$new_n474
|
||||
.gate AND A=$abc$2385$new_n472 B=$abc$2385$new_n474 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[7]
|
||||
.gate AND A=$abc$2385$new_n58 B=$abc$2385$new_n438 Y=:38.Y[0]
|
||||
.gate NAND A=in_a_var[1] B=$abc$2385$new_n74 Y=$abc$2385$new_n477
|
||||
.gate NAND A=$abc$2385$new_n84 B=$abc$2385$new_n477 Y=:38.Y[1]
|
||||
.gate NAND A=in_a_var[2] B=$abc$2385$new_n74 Y=$abc$2385$new_n479
|
||||
.gate NAND A=$abc$2385$new_n92 B=$abc$2385$new_n479 Y=:38.Y[2]
|
||||
.gate NAND A=in_a_var[3] B=$abc$2385$new_n74 Y=$abc$2385$new_n481
|
||||
.gate NAND A=$abc$2385$new_n104 B=$abc$2385$new_n481 Y=:38.Y[3]
|
||||
.gate NAND A=in_a_var[4] B=$abc$2385$new_n74 Y=$abc$2385$new_n483
|
||||
.gate NAND A=$abc$2385$new_n116 B=$abc$2385$new_n483 Y=:38.Y[4]
|
||||
.gate NAND A=in_a_var[5] B=$abc$2385$new_n74 Y=$abc$2385$new_n485
|
||||
.gate NAND A=$abc$2385$new_n127 B=$abc$2385$new_n485 Y=:38.Y[5]
|
||||
.gate NAND A=in_a_var[6] B=$abc$2385$new_n74 Y=$abc$2385$new_n487
|
||||
.gate NAND A=$abc$2385$new_n137 B=$abc$2385$new_n487 Y=:38.Y[6]
|
||||
.gate NAND A=in_a_var[7] B=$abc$2385$new_n74 Y=$abc$2385$new_n489
|
||||
.gate NAND A=$abc$2385$new_n150 B=$abc$2385$new_n489 Y=:38.Y[7]
|
||||
.gate DFF C=clk D=$abc$2385$auto$maccmap.cc:114:fulladd$252.Y[0] Q=out_var[0]
|
||||
.gate DFF C=clk D=$abc$2385$auto$maccmap.cc:240:synth$253.P[1] Q=out_var[1]
|
||||
.gate DFF C=clk D=$abc$2385$auto$maccmap.cc:240:synth$253.Y[2] Q=out_var[2]
|
||||
.gate DFF C=clk D=$abc$2385$auto$maccmap.cc:240:synth$253.Y[3] Q=out_var[3]
|
||||
.gate DFF C=clk D=$abc$2385$auto$maccmap.cc:240:synth$253.Y[4] Q=out_var[4]
|
||||
.gate DFF C=clk D=$abc$2385$auto$maccmap.cc:240:synth$253.Y[5] Q=out_var[5]
|
||||
.gate DFF C=clk D=$abc$2385$auto$maccmap.cc:240:synth$253.Y[6] Q=out_var[6]
|
||||
.gate DFF C=clk D=$abc$2385$auto$maccmap.cc:240:synth$253.Y[7] Q=out_var[7]
|
||||
.gate DFF C=clk D=:38.Y[0] Q=:1.test_1[0]
|
||||
.gate DFF C=clk D=:38.Y[1] Q=:1.test_1[1]
|
||||
.gate DFF C=clk D=:38.Y[2] Q=:1.test_1[2]
|
||||
.gate DFF C=clk D=:38.Y[3] Q=:1.test_1[3]
|
||||
.gate DFF C=clk D=:38.Y[4] Q=:1.test_1[4]
|
||||
.gate DFF C=clk D=:38.Y[5] Q=:1.test_1[5]
|
||||
.gate DFF C=clk D=:38.Y[6] Q=:1.test_1[6]
|
||||
.gate DFF C=clk D=:38.Y[7] Q=:1.test_1[7]
|
||||
.gate DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[0] Q=:1.test_2[0]
|
||||
.gate DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[1] Q=:1.test_2[1]
|
||||
.gate DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[2] Q=:1.test_2[2]
|
||||
.gate DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[3] Q=:1.test_2[3]
|
||||
.gate DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[4] Q=:1.test_2[4]
|
||||
.gate DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[5] Q=:1.test_2[5]
|
||||
.gate DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[6] Q=:1.test_2[6]
|
||||
.gate DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[7] Q=:1.test_2[7]
|
||||
.gateinit :1.test_2[7]=0
|
||||
.gateinit :1.test_2[6]=0
|
||||
.gateinit :1.test_2[5]=0
|
||||
.gateinit :1.test_2[4]=0
|
||||
.gateinit :1.test_2[3]=0
|
||||
.gateinit :1.test_2[2]=0
|
||||
.gateinit :1.test_2[1]=0
|
||||
.gateinit :1.test_2[0]=0
|
||||
.gateinit :1.test_1[7]=1
|
||||
.gateinit :1.test_1[6]=1
|
||||
.gateinit :1.test_1[5]=1
|
||||
.gateinit :1.test_1[4]=1
|
||||
.gateinit :1.test_1[3]=1
|
||||
.gateinit :1.test_1[2]=1
|
||||
.gateinit :1.test_1[1]=1
|
||||
.gateinit :1.test_1[0]=1
|
||||
.end
|
||||
484
tests/blif/gatesi.blif.ok
Normal file
484
tests/blif/gatesi.blif.ok
Normal file
|
|
@ -0,0 +1,484 @@
|
|||
# Generated by Yosys
|
||||
|
||||
.model test
|
||||
.inputs clk in_a_var[0] in_a_var[1] in_a_var[2] in_a_var[3] in_a_var[4] in_a_var[5] in_a_var[6] in_a_var[7] in_b_var[0] in_b_var[1] in_b_var[2] in_b_var[3] in_b_var[4] in_b_var[5] in_b_var[6] in_b_var[7]
|
||||
.outputs out_var[0] out_var[1] out_var[2] out_var[3] out_var[4] out_var[5] out_var[6] out_var[7]
|
||||
.names $false
|
||||
.names $true
|
||||
1
|
||||
.names $undef
|
||||
.subckt ORNOT A=:1.test_1[0] B=in_a_var[0] Y=$abc$2385$new_n57
|
||||
.subckt NOT A=$abc$2385$new_n65 Y=$abc$2385$new_n66
|
||||
.subckt XNOR A=$abc$2385$new_n62 B=$abc$2385$new_n88 Y=$abc$2385$auto$maccmap.cc:240:synth$253.P[1]
|
||||
.subckt NAND A=:1.test_1[0] B=:1.test_2[0] Y=$abc$2385$new_n157
|
||||
.subckt ANDNOT A=:1.test_2[0] B=$abc$2385$new_n91 Y=$abc$2385$new_n158
|
||||
.subckt ANDNOT A=:1.test_2[1] B=$abc$2385$new_n64 Y=$abc$2385$new_n159
|
||||
.subckt AND A=:1.test_2[1] B=$abc$2385$new_n65 Y=$abc$2385$new_n160
|
||||
.subckt ORNOT A=$abc$2385$new_n160 B=:1.test_1[0] Y=$abc$2385$new_n161
|
||||
.subckt AND A=:1.test_2[2] B=$abc$2385$new_n161 Y=$abc$2385$new_n162
|
||||
.subckt ANDNOT A=:1.test_1[1] B=:1.test_1[0] Y=$abc$2385$new_n163
|
||||
.subckt ANDNOT A=:1.test_2[2] B=:1.test_1[0] Y=$abc$2385$new_n164
|
||||
.subckt XNOR A=$abc$2385$new_n160 B=$abc$2385$new_n164 Y=$abc$2385$new_n165
|
||||
.subckt AND A=:1.test_1[2] B=$abc$2385$new_n64 Y=$abc$2385$new_n67
|
||||
.subckt MUX A=$abc$2385$new_n160 B=$abc$2385$new_n165 S=:1.test_2[2] Y=$abc$2385$new_n166
|
||||
.subckt ORNOT A=:1.test_2[0] B=:1.test_1[0] Y=$abc$2385$new_n167
|
||||
.subckt AND A=$abc$2385$new_n159 B=$abc$2385$new_n167 Y=$abc$2385$new_n168
|
||||
.subckt AND A=$abc$2385$new_n166 B=$abc$2385$new_n168 Y=$abc$2385$new_n169
|
||||
.subckt XOR A=$abc$2385$new_n166 B=$abc$2385$new_n168 Y=$abc$2385$new_n170
|
||||
.subckt AND A=$abc$2385$new_n158 B=$abc$2385$new_n170 Y=$abc$2385$new_n171
|
||||
.subckt ANDNOT A=:1.test_2[0] B=$abc$2385$new_n103 Y=$abc$2385$new_n172
|
||||
.subckt ANDNOT A=:1.test_2[1] B=$abc$2385$new_n91 Y=$abc$2385$new_n173
|
||||
.subckt ANDNOT A=:1.test_2[1] B=$abc$2385$new_n103 Y=$abc$2385$new_n174
|
||||
.subckt AND A=$abc$2385$new_n158 B=$abc$2385$new_n174 Y=$abc$2385$new_n175
|
||||
.subckt AND A=:1.test_1[3] B=$abc$2385$new_n67 Y=$abc$2385$new_n68
|
||||
.subckt XOR A=$abc$2385$new_n172 B=$abc$2385$new_n173 Y=$abc$2385$new_n176
|
||||
.subckt NAND A=:1.test_2[2] B=$abc$2385$new_n65 Y=$abc$2385$new_n177
|
||||
.subckt AND A=:1.test_1[0] B=:1.test_2[3] Y=$abc$2385$new_n178
|
||||
.subckt NAND A=:1.test_1[0] B=$abc$2385$new_n177 Y=$abc$2385$new_n179
|
||||
.subckt XNOR A=$abc$2385$new_n177 B=$abc$2385$new_n178 Y=$abc$2385$new_n180
|
||||
.subckt NAND A=$abc$2385$new_n162 B=$abc$2385$new_n180 Y=$abc$2385$new_n181
|
||||
.subckt XOR A=$abc$2385$new_n162 B=$abc$2385$new_n180 Y=$abc$2385$new_n182
|
||||
.subckt NAND A=$abc$2385$new_n176 B=$abc$2385$new_n182 Y=$abc$2385$new_n183
|
||||
.subckt XOR A=$abc$2385$new_n176 B=$abc$2385$new_n182 Y=$abc$2385$new_n184
|
||||
.subckt NAND A=$abc$2385$new_n171 B=$abc$2385$new_n184 Y=$abc$2385$new_n185
|
||||
.subckt AND A=:1.test_1[4] B=$abc$2385$new_n68 Y=$abc$2385$new_n69
|
||||
.subckt XOR A=$abc$2385$new_n171 B=$abc$2385$new_n184 Y=$abc$2385$new_n186
|
||||
.subckt NAND A=$abc$2385$new_n169 B=$abc$2385$new_n186 Y=$abc$2385$new_n187
|
||||
.subckt NAND A=$abc$2385$new_n185 B=$abc$2385$new_n187 Y=$abc$2385$new_n188
|
||||
.subckt ANDNOT A=:1.test_2[0] B=$abc$2385$new_n115 Y=$abc$2385$new_n189
|
||||
.subckt ANDNOT A=:1.test_2[1] B=$abc$2385$new_n115 Y=$abc$2385$new_n190
|
||||
.subckt NAND A=$abc$2385$new_n172 B=$abc$2385$new_n190 Y=$abc$2385$new_n191
|
||||
.subckt XOR A=$abc$2385$new_n174 B=$abc$2385$new_n189 Y=$abc$2385$new_n192
|
||||
.subckt ANDNOT A=:1.test_2[2] B=$abc$2385$new_n91 Y=$abc$2385$new_n193
|
||||
.subckt NAND A=$abc$2385$new_n192 B=$abc$2385$new_n193 Y=$abc$2385$new_n194
|
||||
.subckt XOR A=$abc$2385$new_n192 B=$abc$2385$new_n193 Y=$abc$2385$new_n195
|
||||
.subckt AND A=:1.test_1[5] B=$abc$2385$new_n69 Y=$abc$2385$new_n70
|
||||
.subckt AND A=:1.test_2[3] B=$abc$2385$new_n179 Y=$abc$2385$new_n196
|
||||
.subckt NAND A=:1.test_2[3] B=$abc$2385$new_n65 Y=$abc$2385$new_n197
|
||||
.subckt NAND A=:1.test_1[0] B=$abc$2385$new_n197 Y=$abc$2385$new_n198
|
||||
.subckt AND A=:1.test_2[4] B=$abc$2385$new_n198 Y=$abc$2385$new_n199
|
||||
.subckt NAND A=:1.test_2[3] B=$abc$2385$new_n163 Y=$abc$2385$new_n200
|
||||
.subckt NAND A=$abc$2385$new_n199 B=$abc$2385$new_n200 Y=$abc$2385$new_n201
|
||||
.subckt ORNOT A=:1.test_2[4] B=$abc$2385$new_n197 Y=$abc$2385$new_n202
|
||||
.subckt AND A=$abc$2385$new_n201 B=$abc$2385$new_n202 Y=$abc$2385$new_n203
|
||||
.subckt NAND A=$abc$2385$new_n175 B=$abc$2385$new_n203 Y=$abc$2385$new_n204
|
||||
.subckt XOR A=$abc$2385$new_n175 B=$abc$2385$new_n203 Y=$abc$2385$new_n205
|
||||
.subckt AND A=:1.test_1[6] B=$abc$2385$new_n70 Y=$abc$2385$new_n71
|
||||
.subckt NAND A=$abc$2385$new_n196 B=$abc$2385$new_n205 Y=$abc$2385$new_n206
|
||||
.subckt XOR A=$abc$2385$new_n196 B=$abc$2385$new_n205 Y=$abc$2385$new_n207
|
||||
.subckt AND A=$abc$2385$new_n195 B=$abc$2385$new_n207 Y=$abc$2385$new_n208
|
||||
.subckt XOR A=$abc$2385$new_n195 B=$abc$2385$new_n207 Y=$abc$2385$new_n209
|
||||
.subckt NAND A=$abc$2385$new_n181 B=$abc$2385$new_n183 Y=$abc$2385$new_n210
|
||||
.subckt AND A=$abc$2385$new_n209 B=$abc$2385$new_n210 Y=$abc$2385$new_n211
|
||||
.subckt XOR A=$abc$2385$new_n209 B=$abc$2385$new_n210 Y=$abc$2385$new_n212
|
||||
.subckt AND A=$abc$2385$new_n188 B=$abc$2385$new_n212 Y=$abc$2385$new_n213
|
||||
.subckt ANDNOT A=:1.test_2[0] B=$abc$2385$new_n77 Y=$abc$2385$new_n214
|
||||
.subckt ANDNOT A=:1.test_2[3] B=$abc$2385$new_n91 Y=$abc$2385$new_n215
|
||||
.subckt XNOR A=:1.test_1[6] B=$abc$2385$new_n70 Y=$abc$2385$new_n72
|
||||
.subckt ANDNOT A=:1.test_2[2] B=$abc$2385$new_n103 Y=$abc$2385$new_n216
|
||||
.subckt ANDNOT A=:1.test_2[2] B=$abc$2385$new_n115 Y=$abc$2385$new_n217
|
||||
.subckt NAND A=$abc$2385$new_n174 B=$abc$2385$new_n217 Y=$abc$2385$new_n218
|
||||
.subckt XOR A=$abc$2385$new_n190 B=$abc$2385$new_n216 Y=$abc$2385$new_n219
|
||||
.subckt NAND A=$abc$2385$new_n215 B=$abc$2385$new_n219 Y=$abc$2385$new_n220
|
||||
.subckt XOR A=$abc$2385$new_n215 B=$abc$2385$new_n219 Y=$abc$2385$new_n221
|
||||
.subckt AND A=$abc$2385$new_n214 B=$abc$2385$new_n221 Y=$abc$2385$new_n222
|
||||
.subckt XOR A=$abc$2385$new_n214 B=$abc$2385$new_n221 Y=$abc$2385$new_n223
|
||||
.subckt NAND A=:1.test_2[4] B=$abc$2385$new_n65 Y=$abc$2385$new_n224
|
||||
.subckt NAND A=:1.test_1[0] B=$abc$2385$new_n224 Y=$abc$2385$new_n225
|
||||
.subckt NOT A=$abc$2385$new_n72 Y=$abc$2385$new_n73
|
||||
.subckt AND A=:1.test_2[5] B=$abc$2385$new_n225 Y=$abc$2385$new_n226
|
||||
.subckt NAND A=:1.test_2[4] B=$abc$2385$new_n163 Y=$abc$2385$new_n227
|
||||
.subckt NAND A=$abc$2385$new_n226 B=$abc$2385$new_n227 Y=$abc$2385$new_n228
|
||||
.subckt ORNOT A=:1.test_2[5] B=$abc$2385$new_n224 Y=$abc$2385$new_n229
|
||||
.subckt AND A=$abc$2385$new_n228 B=$abc$2385$new_n229 Y=$abc$2385$new_n230
|
||||
.subckt NAND A=$abc$2385$new_n191 B=$abc$2385$new_n194 Y=$abc$2385$new_n231
|
||||
.subckt NAND A=$abc$2385$new_n230 B=$abc$2385$new_n231 Y=$abc$2385$new_n232
|
||||
.subckt XOR A=$abc$2385$new_n230 B=$abc$2385$new_n231 Y=$abc$2385$new_n233
|
||||
.subckt NAND A=$abc$2385$new_n199 B=$abc$2385$new_n233 Y=$abc$2385$new_n234
|
||||
.subckt XOR A=$abc$2385$new_n199 B=$abc$2385$new_n233 Y=$abc$2385$new_n235
|
||||
.subckt AND A=:1.test_1[7] B=$abc$2385$new_n71 Y=$abc$2385$new_n74
|
||||
.subckt AND A=$abc$2385$new_n223 B=$abc$2385$new_n235 Y=$abc$2385$new_n236
|
||||
.subckt XOR A=$abc$2385$new_n223 B=$abc$2385$new_n235 Y=$abc$2385$new_n237
|
||||
.subckt NAND A=$abc$2385$new_n208 B=$abc$2385$new_n237 Y=$abc$2385$new_n238
|
||||
.subckt XOR A=$abc$2385$new_n208 B=$abc$2385$new_n237 Y=$abc$2385$new_n239
|
||||
.subckt NAND A=$abc$2385$new_n204 B=$abc$2385$new_n206 Y=$abc$2385$new_n240
|
||||
.subckt NAND A=$abc$2385$new_n239 B=$abc$2385$new_n240 Y=$abc$2385$new_n241
|
||||
.subckt XOR A=$abc$2385$new_n239 B=$abc$2385$new_n240 Y=$abc$2385$new_n242
|
||||
.subckt AND A=$abc$2385$new_n211 B=$abc$2385$new_n242 Y=$abc$2385$new_n243
|
||||
.subckt XOR A=$abc$2385$new_n211 B=$abc$2385$new_n242 Y=$abc$2385$new_n244
|
||||
.subckt NAND A=$abc$2385$new_n213 B=$abc$2385$new_n244 Y=$abc$2385$new_n245
|
||||
.subckt XNOR A=:1.test_1[7] B=$abc$2385$new_n71 Y=$abc$2385$new_n75
|
||||
.subckt AND A=:1.test_2[0] B=$abc$2385$new_n163 Y=$abc$2385$new_n246
|
||||
.subckt NAND A=:1.test_2[0] B=$abc$2385$new_n163 Y=$abc$2385$new_n247
|
||||
.subckt XOR A=$abc$2385$new_n158 B=$abc$2385$new_n170 Y=$abc$2385$new_n248
|
||||
.subckt AND A=$abc$2385$new_n246 B=$abc$2385$new_n248 Y=$abc$2385$new_n249
|
||||
.subckt XOR A=$abc$2385$new_n169 B=$abc$2385$new_n186 Y=$abc$2385$new_n250
|
||||
.subckt AND A=$abc$2385$new_n249 B=$abc$2385$new_n250 Y=$abc$2385$new_n251
|
||||
.subckt XOR A=$abc$2385$new_n188 B=$abc$2385$new_n212 Y=$abc$2385$new_n252
|
||||
.subckt AND A=$abc$2385$new_n251 B=$abc$2385$new_n252 Y=$abc$2385$new_n253
|
||||
.subckt NAND A=$abc$2385$new_n244 B=$abc$2385$new_n253 Y=$abc$2385$new_n254
|
||||
.subckt XNOR A=$abc$2385$new_n213 B=$abc$2385$new_n244 Y=$abc$2385$new_n255
|
||||
.subckt ORNOT A=in_a_var[0] B=:1.test_1[0] Y=$abc$2385$new_n58
|
||||
.subckt ANDNOT A=:1.test_1[5] B=$abc$2385$new_n69 Y=$abc$2385$new_n76
|
||||
.subckt NAND A=$abc$2385$new_n245 B=$abc$2385$new_n254 Y=$abc$2385$new_n256
|
||||
.subckt NAND A=$abc$2385$new_n238 B=$abc$2385$new_n241 Y=$abc$2385$new_n257
|
||||
.subckt ANDNOT A=:1.test_2[0] B=$abc$2385$new_n72 Y=$abc$2385$new_n258
|
||||
.subckt ORNOT A=$abc$2385$new_n77 B=:1.test_2[1] Y=$abc$2385$new_n259
|
||||
.subckt ANDNOT A=:1.test_2[1] B=$abc$2385$new_n72 Y=$abc$2385$new_n260
|
||||
.subckt NAND A=$abc$2385$new_n214 B=$abc$2385$new_n260 Y=$abc$2385$new_n261
|
||||
.subckt XNOR A=$abc$2385$new_n258 B=$abc$2385$new_n259 Y=$abc$2385$new_n262
|
||||
.subckt ANDNOT A=:1.test_2[4] B=$abc$2385$new_n91 Y=$abc$2385$new_n263
|
||||
.subckt ANDNOT A=:1.test_2[3] B=$abc$2385$new_n103 Y=$abc$2385$new_n264
|
||||
.subckt ANDNOT A=:1.test_2[3] B=$abc$2385$new_n115 Y=$abc$2385$new_n265
|
||||
.subckt XNOR A=:1.test_1[5] B=$abc$2385$new_n69 Y=$abc$2385$new_n77
|
||||
.subckt NAND A=$abc$2385$new_n216 B=$abc$2385$new_n265 Y=$abc$2385$new_n266
|
||||
.subckt XOR A=$abc$2385$new_n217 B=$abc$2385$new_n264 Y=$abc$2385$new_n267
|
||||
.subckt NAND A=$abc$2385$new_n263 B=$abc$2385$new_n267 Y=$abc$2385$new_n268
|
||||
.subckt XOR A=$abc$2385$new_n263 B=$abc$2385$new_n267 Y=$abc$2385$new_n269
|
||||
.subckt AND A=$abc$2385$new_n262 B=$abc$2385$new_n269 Y=$abc$2385$new_n270
|
||||
.subckt XOR A=$abc$2385$new_n262 B=$abc$2385$new_n269 Y=$abc$2385$new_n271
|
||||
.subckt NAND A=$abc$2385$new_n222 B=$abc$2385$new_n271 Y=$abc$2385$new_n272
|
||||
.subckt XOR A=$abc$2385$new_n222 B=$abc$2385$new_n271 Y=$abc$2385$new_n273
|
||||
.subckt NAND A=:1.test_2[5] B=$abc$2385$new_n65 Y=$abc$2385$new_n274
|
||||
.subckt NAND A=:1.test_1[0] B=$abc$2385$new_n274 Y=$abc$2385$new_n275
|
||||
.subckt NOR A=:1.test_1[3] B=:1.test_1[4] Y=$abc$2385$new_n78
|
||||
.subckt AND A=:1.test_2[6] B=$abc$2385$new_n275 Y=$abc$2385$new_n276
|
||||
.subckt NAND A=:1.test_2[5] B=$abc$2385$new_n163 Y=$abc$2385$new_n277
|
||||
.subckt NAND A=:1.test_2[6] B=$abc$2385$new_n65 Y=$abc$2385$new_n278
|
||||
.subckt NAND A=$abc$2385$new_n276 B=$abc$2385$new_n277 Y=$abc$2385$new_n279
|
||||
.subckt ORNOT A=:1.test_2[6] B=$abc$2385$new_n274 Y=$abc$2385$new_n280
|
||||
.subckt AND A=$abc$2385$new_n279 B=$abc$2385$new_n280 Y=$abc$2385$new_n281
|
||||
.subckt NAND A=$abc$2385$new_n218 B=$abc$2385$new_n220 Y=$abc$2385$new_n282
|
||||
.subckt NAND A=$abc$2385$new_n281 B=$abc$2385$new_n282 Y=$abc$2385$new_n283
|
||||
.subckt XOR A=$abc$2385$new_n281 B=$abc$2385$new_n282 Y=$abc$2385$new_n284
|
||||
.subckt NAND A=$abc$2385$new_n226 B=$abc$2385$new_n284 Y=$abc$2385$new_n285
|
||||
.subckt AND A=$abc$2385$new_n63 B=$abc$2385$new_n78 Y=$abc$2385$new_n79
|
||||
.subckt XOR A=$abc$2385$new_n226 B=$abc$2385$new_n284 Y=$abc$2385$new_n286
|
||||
.subckt NAND A=$abc$2385$new_n273 B=$abc$2385$new_n286 Y=$abc$2385$new_n287
|
||||
.subckt XOR A=$abc$2385$new_n273 B=$abc$2385$new_n286 Y=$abc$2385$new_n288
|
||||
.subckt NAND A=$abc$2385$new_n236 B=$abc$2385$new_n288 Y=$abc$2385$new_n289
|
||||
.subckt XOR A=$abc$2385$new_n236 B=$abc$2385$new_n288 Y=$abc$2385$new_n290
|
||||
.subckt NAND A=$abc$2385$new_n232 B=$abc$2385$new_n234 Y=$abc$2385$new_n291
|
||||
.subckt NAND A=$abc$2385$new_n290 B=$abc$2385$new_n291 Y=$abc$2385$new_n292
|
||||
.subckt XOR A=$abc$2385$new_n290 B=$abc$2385$new_n291 Y=$abc$2385$new_n293
|
||||
.subckt NAND A=$abc$2385$new_n257 B=$abc$2385$new_n293 Y=$abc$2385$new_n294
|
||||
.subckt XOR A=$abc$2385$new_n257 B=$abc$2385$new_n293 Y=$abc$2385$new_n295
|
||||
.subckt ANDNOT A=$abc$2385$new_n79 B=:1.test_1[2] Y=$abc$2385$new_n80
|
||||
.subckt NAND A=$abc$2385$new_n243 B=$abc$2385$new_n295 Y=$abc$2385$new_n296
|
||||
.subckt XOR A=$abc$2385$new_n243 B=$abc$2385$new_n295 Y=$abc$2385$new_n297
|
||||
.subckt NAND A=$abc$2385$new_n256 B=$abc$2385$new_n297 Y=$abc$2385$new_n298
|
||||
.subckt XNOR A=$abc$2385$new_n256 B=$abc$2385$new_n297 Y=$abc$2385$new_n299
|
||||
.subckt NAND A=$abc$2385$new_n73 B=$abc$2385$new_n299 Y=$abc$2385$new_n300
|
||||
.subckt OR A=$abc$2385$new_n73 B=$abc$2385$new_n299 Y=$abc$2385$new_n301
|
||||
.subckt XOR A=$abc$2385$new_n253 B=$abc$2385$new_n255 Y=$abc$2385$new_n302
|
||||
.subckt XNOR A=$abc$2385$new_n251 B=$abc$2385$new_n252 Y=$abc$2385$new_n303
|
||||
.subckt XOR A=$abc$2385$new_n249 B=$abc$2385$new_n250 Y=$abc$2385$new_n304
|
||||
.subckt XNOR A=$abc$2385$new_n249 B=$abc$2385$new_n250 Y=$abc$2385$new_n305
|
||||
.subckt AND A=$abc$2385$new_n77 B=$abc$2385$new_n80 Y=$abc$2385$new_n81
|
||||
.subckt NAND A=$abc$2385$new_n103 B=$abc$2385$new_n304 Y=$abc$2385$new_n306
|
||||
.subckt OR A=$abc$2385$new_n103 B=$abc$2385$new_n304 Y=$abc$2385$new_n307
|
||||
.subckt XNOR A=$abc$2385$new_n247 B=$abc$2385$new_n248 Y=$abc$2385$new_n308
|
||||
.subckt NAND A=:1.test_1[0] B=:1.test_2[1] Y=$abc$2385$new_n309
|
||||
.subckt ANDNOT A=:1.test_2[0] B=$abc$2385$new_n64 Y=$abc$2385$new_n310
|
||||
.subckt XNOR A=$abc$2385$new_n309 B=$abc$2385$new_n310 Y=$abc$2385$new_n311
|
||||
.subckt NAND A=$abc$2385$new_n66 B=$abc$2385$new_n311 Y=$abc$2385$new_n312
|
||||
.subckt OR A=:1.test_2[1] B=$abc$2385$new_n157 Y=$abc$2385$new_n313
|
||||
.subckt NAND A=$abc$2385$new_n312 B=$abc$2385$new_n313 Y=$abc$2385$new_n314
|
||||
.subckt OR A=$abc$2385$new_n308 B=$abc$2385$new_n314 Y=$abc$2385$new_n315
|
||||
.subckt NAND A=$abc$2385$new_n75 B=$abc$2385$new_n81 Y=$abc$2385$new_n82
|
||||
.subckt NAND A=$abc$2385$new_n91 B=$abc$2385$new_n315 Y=$abc$2385$new_n316
|
||||
.subckt NAND A=$abc$2385$new_n308 B=$abc$2385$new_n314 Y=$abc$2385$new_n317
|
||||
.subckt NAND A=$abc$2385$new_n316 B=$abc$2385$new_n317 Y=$abc$2385$new_n318
|
||||
.subckt NAND A=$abc$2385$new_n307 B=$abc$2385$new_n318 Y=$abc$2385$new_n319
|
||||
.subckt NAND A=$abc$2385$new_n247 B=$abc$2385$new_n311 Y=$abc$2385$new_n320
|
||||
.subckt NAND A=$abc$2385$new_n306 B=$abc$2385$new_n319 Y=$abc$2385$new_n321
|
||||
.subckt ORNOT A=$abc$2385$new_n115 B=$abc$2385$new_n303 Y=$abc$2385$new_n322
|
||||
.subckt ORNOT A=$abc$2385$new_n303 B=$abc$2385$new_n115 Y=$abc$2385$new_n323
|
||||
.subckt NAND A=$abc$2385$new_n321 B=$abc$2385$new_n322 Y=$abc$2385$new_n324
|
||||
.subckt NAND A=$abc$2385$new_n323 B=$abc$2385$new_n324 Y=$abc$2385$new_n325
|
||||
.subckt OR A=$abc$2385$new_n73 B=$abc$2385$new_n82 Y=$abc$2385$new_n83
|
||||
.subckt NAND A=$abc$2385$new_n77 B=$abc$2385$new_n325 Y=$abc$2385$new_n326
|
||||
.subckt NAND A=$abc$2385$new_n302 B=$abc$2385$new_n326 Y=$abc$2385$new_n327
|
||||
.subckt OR A=$abc$2385$new_n77 B=$abc$2385$new_n325 Y=$abc$2385$new_n328
|
||||
.subckt AND A=$abc$2385$new_n327 B=$abc$2385$new_n328 Y=$abc$2385$new_n329
|
||||
.subckt NAND A=$abc$2385$new_n300 B=$abc$2385$new_n329 Y=$abc$2385$new_n330
|
||||
.subckt AND A=$abc$2385$new_n301 B=$abc$2385$new_n330 Y=$abc$2385$new_n331
|
||||
.subckt NAND A=$abc$2385$new_n75 B=$abc$2385$new_n331 Y=$abc$2385$new_n332
|
||||
.subckt OR A=in_b_var[5] B=$abc$2385$new_n302 Y=$abc$2385$new_n333
|
||||
.subckt NAND A=in_b_var[4] B=$abc$2385$new_n303 Y=$abc$2385$new_n334
|
||||
.subckt OR A=in_b_var[4] B=$abc$2385$new_n303 Y=$abc$2385$new_n335
|
||||
.subckt AND A=$abc$2385$new_n66 B=$abc$2385$new_n83 Y=$abc$2385$new_n84
|
||||
.subckt AND A=in_b_var[1] B=$abc$2385$new_n320 Y=$abc$2385$new_n336
|
||||
.subckt OR A=in_b_var[3] B=$abc$2385$new_n305 Y=$abc$2385$new_n337
|
||||
.subckt ANDNOT A=in_b_var[2] B=$abc$2385$new_n308 Y=$abc$2385$new_n338
|
||||
.subckt XNOR A=in_b_var[2] B=$abc$2385$new_n308 Y=$abc$2385$new_n339
|
||||
.subckt NAND A=in_b_var[3] B=$abc$2385$new_n305 Y=$abc$2385$new_n340
|
||||
.subckt XNOR A=in_b_var[3] B=$abc$2385$new_n304 Y=$abc$2385$new_n341
|
||||
.subckt AND A=$abc$2385$new_n339 B=$abc$2385$new_n341 Y=$abc$2385$new_n342
|
||||
.subckt NAND A=$abc$2385$new_n336 B=$abc$2385$new_n342 Y=$abc$2385$new_n343
|
||||
.subckt NAND A=$abc$2385$new_n337 B=$abc$2385$new_n338 Y=$abc$2385$new_n344
|
||||
.subckt AND A=$abc$2385$new_n340 B=$abc$2385$new_n344 Y=$abc$2385$new_n345
|
||||
.subckt ORNOT A=$abc$2385$new_n84 B=in_a_var[1] Y=$abc$2385$new_n85
|
||||
.subckt AND A=$abc$2385$new_n343 B=$abc$2385$new_n345 Y=$abc$2385$new_n346
|
||||
.subckt AND A=in_b_var[0] B=$abc$2385$new_n157 Y=$abc$2385$new_n347
|
||||
.subckt XOR A=in_b_var[1] B=$abc$2385$new_n320 Y=$abc$2385$new_n348
|
||||
.subckt AND A=$abc$2385$new_n342 B=$abc$2385$new_n348 Y=$abc$2385$new_n349
|
||||
.subckt NAND A=$abc$2385$new_n347 B=$abc$2385$new_n349 Y=$abc$2385$new_n350
|
||||
.subckt NAND A=$abc$2385$new_n346 B=$abc$2385$new_n350 Y=$abc$2385$new_n351
|
||||
.subckt NAND A=$abc$2385$new_n335 B=$abc$2385$new_n351 Y=$abc$2385$new_n352
|
||||
.subckt NAND A=$abc$2385$new_n334 B=$abc$2385$new_n352 Y=$abc$2385$new_n353
|
||||
.subckt NAND A=$abc$2385$new_n333 B=$abc$2385$new_n353 Y=$abc$2385$new_n354
|
||||
.subckt NAND A=in_b_var[6] B=$abc$2385$new_n299 Y=$abc$2385$new_n355
|
||||
.subckt XNOR A=:1.test_1[0] B=in_a_var[0] Y=$abc$2385$new_n59
|
||||
.subckt XNOR A=in_a_var[1] B=$abc$2385$new_n84 Y=$abc$2385$new_n86
|
||||
.subckt NAND A=in_b_var[5] B=$abc$2385$new_n302 Y=$abc$2385$new_n356
|
||||
.subckt AND A=$abc$2385$new_n355 B=$abc$2385$new_n356 Y=$abc$2385$new_n357
|
||||
.subckt NAND A=$abc$2385$new_n354 B=$abc$2385$new_n357 Y=$abc$2385$new_n358
|
||||
.subckt AND A=$abc$2385$new_n157 B=$abc$2385$new_n320 Y=$abc$2385$new_n359
|
||||
.subckt ANDNOT A=$abc$2385$new_n359 B=$abc$2385$new_n308 Y=$abc$2385$new_n360
|
||||
.subckt AND A=$abc$2385$new_n305 B=$abc$2385$new_n360 Y=$abc$2385$new_n361
|
||||
.subckt AND A=$abc$2385$new_n303 B=$abc$2385$new_n361 Y=$abc$2385$new_n362
|
||||
.subckt AND A=$abc$2385$new_n302 B=$abc$2385$new_n362 Y=$abc$2385$new_n363
|
||||
.subckt NAND A=$abc$2385$new_n299 B=$abc$2385$new_n363 Y=$abc$2385$new_n364
|
||||
.subckt AND A=$abc$2385$new_n296 B=$abc$2385$new_n298 Y=$abc$2385$new_n365
|
||||
.subckt NAND A=in_b_var[1] B=$abc$2385$new_n86 Y=$abc$2385$new_n87
|
||||
.subckt AND A=$abc$2385$new_n289 B=$abc$2385$new_n292 Y=$abc$2385$new_n366
|
||||
.subckt OR A=:1.test_2[0] B=$abc$2385$new_n75 Y=$abc$2385$new_n367
|
||||
.subckt AND A=$abc$2385$new_n261 B=$abc$2385$new_n367 Y=$abc$2385$new_n368
|
||||
.subckt XNOR A=$abc$2385$new_n270 B=$abc$2385$new_n368 Y=$abc$2385$new_n369
|
||||
.subckt XNOR A=$abc$2385$new_n276 B=$abc$2385$new_n369 Y=$abc$2385$new_n370
|
||||
.subckt ANDNOT A=:1.test_2[2] B=$abc$2385$new_n77 Y=$abc$2385$new_n371
|
||||
.subckt ANDNOT A=:1.test_2[5] B=$abc$2385$new_n91 Y=$abc$2385$new_n372
|
||||
.subckt ANDNOT A=:1.test_2[4] B=$abc$2385$new_n103 Y=$abc$2385$new_n373
|
||||
.subckt XNOR A=$abc$2385$new_n372 B=$abc$2385$new_n373 Y=$abc$2385$new_n374
|
||||
.subckt XNOR A=$abc$2385$new_n371 B=$abc$2385$new_n374 Y=$abc$2385$new_n375
|
||||
.subckt XNOR A=in_b_var[1] B=$abc$2385$new_n86 Y=$abc$2385$new_n88
|
||||
.subckt XOR A=$abc$2385$new_n260 B=$abc$2385$new_n265 Y=$abc$2385$new_n376
|
||||
.subckt XNOR A=$abc$2385$new_n375 B=$abc$2385$new_n376 Y=$abc$2385$new_n377
|
||||
.subckt NAND A=$abc$2385$new_n266 B=$abc$2385$new_n268 Y=$abc$2385$new_n378
|
||||
.subckt ANDNOT A=:1.test_2[7] B=:1.test_1[0] Y=$abc$2385$new_n379
|
||||
.subckt XNOR A=$abc$2385$new_n278 B=$abc$2385$new_n379 Y=$abc$2385$new_n380
|
||||
.subckt XNOR A=$abc$2385$new_n75 B=$abc$2385$new_n380 Y=$abc$2385$new_n381
|
||||
.subckt XNOR A=$abc$2385$new_n378 B=$abc$2385$new_n381 Y=$abc$2385$new_n382
|
||||
.subckt XNOR A=$abc$2385$new_n377 B=$abc$2385$new_n382 Y=$abc$2385$new_n383
|
||||
.subckt XNOR A=$abc$2385$new_n370 B=$abc$2385$new_n383 Y=$abc$2385$new_n384
|
||||
.subckt NAND A=$abc$2385$new_n283 B=$abc$2385$new_n285 Y=$abc$2385$new_n385
|
||||
.subckt ANDNOT A=$abc$2385$new_n62 B=$abc$2385$new_n88 Y=$abc$2385$new_n89
|
||||
.subckt AND A=$abc$2385$new_n272 B=$abc$2385$new_n287 Y=$abc$2385$new_n386
|
||||
.subckt XNOR A=$abc$2385$new_n385 B=$abc$2385$new_n386 Y=$abc$2385$new_n387
|
||||
.subckt XNOR A=$abc$2385$new_n384 B=$abc$2385$new_n387 Y=$abc$2385$new_n388
|
||||
.subckt XNOR A=$abc$2385$new_n366 B=$abc$2385$new_n388 Y=$abc$2385$new_n389
|
||||
.subckt XNOR A=:1.test_2[7] B=$abc$2385$new_n294 Y=$abc$2385$new_n390
|
||||
.subckt XNOR A=$abc$2385$new_n389 B=$abc$2385$new_n390 Y=$abc$2385$new_n391
|
||||
.subckt XNOR A=$abc$2385$new_n365 B=$abc$2385$new_n391 Y=$abc$2385$new_n392
|
||||
.subckt OR A=in_b_var[6] B=$abc$2385$new_n299 Y=$abc$2385$new_n393
|
||||
.subckt ORNOT A=in_b_var[6] B=in_a_var[6] Y=$abc$2385$new_n394
|
||||
.subckt ORNOT A=in_a_var[5] B=in_b_var[5] Y=$abc$2385$new_n395
|
||||
.subckt AND A=$abc$2385$new_n85 B=$abc$2385$new_n87 Y=$abc$2385$new_n90
|
||||
.subckt ORNOT A=in_b_var[5] B=in_a_var[5] Y=$abc$2385$new_n396
|
||||
.subckt ORNOT A=in_b_var[4] B=in_a_var[4] Y=$abc$2385$new_n397
|
||||
.subckt AND A=$abc$2385$new_n396 B=$abc$2385$new_n397 Y=$abc$2385$new_n398
|
||||
.subckt ORNOT A=in_b_var[2] B=in_a_var[2] Y=$abc$2385$new_n399
|
||||
.subckt ORNOT A=in_b_var[3] B=in_a_var[3] Y=$abc$2385$new_n400
|
||||
.subckt NAND A=$abc$2385$new_n399 B=$abc$2385$new_n400 Y=$abc$2385$new_n401
|
||||
.subckt ORNOT A=in_a_var[3] B=in_b_var[3] Y=$abc$2385$new_n402
|
||||
.subckt NAND A=$abc$2385$new_n401 B=$abc$2385$new_n402 Y=$abc$2385$new_n403
|
||||
.subckt ORNOT A=in_a_var[2] B=in_b_var[2] Y=$abc$2385$new_n404
|
||||
.subckt NAND A=$abc$2385$new_n402 B=$abc$2385$new_n404 Y=$abc$2385$new_n405
|
||||
.subckt XNOR A=:1.test_1[2] B=$abc$2385$new_n64 Y=$abc$2385$new_n91
|
||||
.subckt NOR A=$abc$2385$new_n401 B=$abc$2385$new_n405 Y=$abc$2385$new_n406
|
||||
.subckt ORNOT A=in_a_var[0] B=in_b_var[0] Y=$abc$2385$new_n407
|
||||
.subckt ORNOT A=in_a_var[1] B=in_b_var[1] Y=$abc$2385$new_n408
|
||||
.subckt NAND A=$abc$2385$new_n407 B=$abc$2385$new_n408 Y=$abc$2385$new_n409
|
||||
.subckt ORNOT A=in_b_var[1] B=in_a_var[1] Y=$abc$2385$new_n410
|
||||
.subckt NAND A=$abc$2385$new_n409 B=$abc$2385$new_n410 Y=$abc$2385$new_n411
|
||||
.subckt NAND A=$abc$2385$new_n406 B=$abc$2385$new_n411 Y=$abc$2385$new_n412
|
||||
.subckt NAND A=$abc$2385$new_n403 B=$abc$2385$new_n412 Y=$abc$2385$new_n413
|
||||
.subckt ORNOT A=in_a_var[4] B=in_b_var[4] Y=$abc$2385$new_n414
|
||||
.subckt NAND A=$abc$2385$new_n413 B=$abc$2385$new_n414 Y=$abc$2385$new_n415
|
||||
.subckt AND A=$abc$2385$new_n83 B=$abc$2385$new_n91 Y=$abc$2385$new_n92
|
||||
.subckt NAND A=$abc$2385$new_n398 B=$abc$2385$new_n415 Y=$abc$2385$new_n416
|
||||
.subckt NAND A=$abc$2385$new_n395 B=$abc$2385$new_n416 Y=$abc$2385$new_n417
|
||||
.subckt NAND A=$abc$2385$new_n394 B=$abc$2385$new_n417 Y=$abc$2385$new_n418
|
||||
.subckt NAND A=$abc$2385$new_n394 B=$abc$2385$new_n395 Y=$abc$2385$new_n419
|
||||
.subckt NOR A=$abc$2385$new_n409 B=$abc$2385$new_n419 Y=$abc$2385$new_n420
|
||||
.subckt AND A=$abc$2385$new_n398 B=$abc$2385$new_n420 Y=$abc$2385$new_n421
|
||||
.subckt ORNOT A=in_b_var[0] B=in_a_var[0] Y=$abc$2385$new_n422
|
||||
.subckt AND A=$abc$2385$new_n410 B=$abc$2385$new_n414 Y=$abc$2385$new_n423
|
||||
.subckt AND A=$abc$2385$new_n422 B=$abc$2385$new_n423 Y=$abc$2385$new_n424
|
||||
.subckt AND A=$abc$2385$new_n406 B=$abc$2385$new_n424 Y=$abc$2385$new_n425
|
||||
.subckt ORNOT A=$abc$2385$new_n92 B=in_a_var[2] Y=$abc$2385$new_n93
|
||||
.subckt NAND A=$abc$2385$new_n421 B=$abc$2385$new_n425 Y=$abc$2385$new_n426
|
||||
.subckt ORNOT A=in_a_var[6] B=in_b_var[6] Y=$abc$2385$new_n427
|
||||
.subckt AND A=$abc$2385$new_n151 B=$abc$2385$new_n427 Y=$abc$2385$new_n428
|
||||
.subckt AND A=$abc$2385$new_n426 B=$abc$2385$new_n428 Y=$abc$2385$new_n429
|
||||
.subckt AND A=$abc$2385$new_n418 B=$abc$2385$new_n429 Y=$abc$2385$new_n430
|
||||
.subckt AND A=$abc$2385$new_n393 B=$abc$2385$new_n430 Y=$abc$2385$new_n431
|
||||
.subckt AND A=$abc$2385$new_n392 B=$abc$2385$new_n431 Y=$abc$2385$new_n432
|
||||
.subckt AND A=$abc$2385$new_n364 B=$abc$2385$new_n432 Y=$abc$2385$new_n433
|
||||
.subckt AND A=$abc$2385$new_n358 B=$abc$2385$new_n433 Y=$abc$2385$new_n434
|
||||
.subckt AND A=$abc$2385$new_n332 B=$abc$2385$new_n434 Y=$abc$2385$new_n435
|
||||
.subckt XNOR A=in_a_var[2] B=$abc$2385$new_n92 Y=$abc$2385$new_n94
|
||||
.subckt AND A=$abc$2385$new_n157 B=$abc$2385$new_n435 Y=$abc$2385$new_n436
|
||||
.subckt XNOR A=$abc$2385$new_n157 B=$abc$2385$new_n435 Y=$abc$2385$new_n437
|
||||
.subckt ORNOT A=$abc$2385$new_n74 B=:1.test_1[0] Y=$abc$2385$new_n438
|
||||
.subckt MUX A=:1.test_1[0] B=$abc$2385$new_n437 S=$abc$2385$new_n74 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[0]
|
||||
.subckt ORNOT A=:1.test_1[1] B=$abc$2385$new_n83 Y=$abc$2385$new_n440
|
||||
.subckt XNOR A=$abc$2385$new_n320 B=$abc$2385$new_n436 Y=$abc$2385$new_n441
|
||||
.subckt MUX A=$abc$2385$new_n440 B=$abc$2385$new_n441 S=$abc$2385$new_n74 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[1]
|
||||
.subckt ORNOT A=:1.test_1[2] B=$abc$2385$new_n83 Y=$abc$2385$new_n443
|
||||
.subckt ANDNOT A=$abc$2385$new_n308 B=$abc$2385$new_n359 Y=$abc$2385$new_n444
|
||||
.subckt XNOR A=$abc$2385$new_n308 B=$abc$2385$new_n359 Y=$abc$2385$new_n445
|
||||
.subckt NAND A=in_b_var[2] B=$abc$2385$new_n94 Y=$abc$2385$new_n95
|
||||
.subckt NAND A=$abc$2385$new_n435 B=$abc$2385$new_n445 Y=$abc$2385$new_n446
|
||||
.subckt ORNOT A=$abc$2385$new_n435 B=$abc$2385$new_n308 Y=$abc$2385$new_n447
|
||||
.subckt AND A=$abc$2385$new_n74 B=$abc$2385$new_n446 Y=$abc$2385$new_n448
|
||||
.subckt NAND A=$abc$2385$new_n447 B=$abc$2385$new_n448 Y=$abc$2385$new_n449
|
||||
.subckt AND A=$abc$2385$new_n443 B=$abc$2385$new_n449 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[2]
|
||||
.subckt ORNOT A=:1.test_1[3] B=$abc$2385$new_n83 Y=$abc$2385$new_n451
|
||||
.subckt AND A=$abc$2385$new_n435 B=$abc$2385$new_n444 Y=$abc$2385$new_n452
|
||||
.subckt AND A=$abc$2385$new_n304 B=$abc$2385$new_n452 Y=$abc$2385$new_n453
|
||||
.subckt XNOR A=$abc$2385$new_n305 B=$abc$2385$new_n452 Y=$abc$2385$new_n454
|
||||
.subckt MUX A=$abc$2385$new_n451 B=$abc$2385$new_n454 S=$abc$2385$new_n74 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[3]
|
||||
.subckt NAND A=in_b_var[0] B=$abc$2385$new_n59 Y=$abc$2385$new_n60
|
||||
.subckt XNOR A=in_b_var[2] B=$abc$2385$new_n94 Y=$abc$2385$new_n96
|
||||
.subckt ORNOT A=:1.test_1[4] B=$abc$2385$new_n83 Y=$abc$2385$new_n456
|
||||
.subckt ORNOT A=$abc$2385$new_n303 B=$abc$2385$new_n453 Y=$abc$2385$new_n457
|
||||
.subckt XNOR A=$abc$2385$new_n303 B=$abc$2385$new_n453 Y=$abc$2385$new_n458
|
||||
.subckt MUX A=$abc$2385$new_n456 B=$abc$2385$new_n458 S=$abc$2385$new_n74 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[4]
|
||||
.subckt ORNOT A=:1.test_1[5] B=$abc$2385$new_n83 Y=$abc$2385$new_n460
|
||||
.subckt OR A=$abc$2385$new_n302 B=$abc$2385$new_n457 Y=$abc$2385$new_n461
|
||||
.subckt XOR A=$abc$2385$new_n302 B=$abc$2385$new_n457 Y=$abc$2385$new_n462
|
||||
.subckt NAND A=$abc$2385$new_n74 B=$abc$2385$new_n462 Y=$abc$2385$new_n463
|
||||
.subckt NAND A=$abc$2385$new_n460 B=$abc$2385$new_n463 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[5]
|
||||
.subckt NAND A=$abc$2385$new_n299 B=$abc$2385$new_n461 Y=$abc$2385$new_n465
|
||||
.subckt OR A=$abc$2385$new_n90 B=$abc$2385$new_n96 Y=$abc$2385$new_n97
|
||||
.subckt OR A=$abc$2385$new_n299 B=$abc$2385$new_n461 Y=$abc$2385$new_n466
|
||||
.subckt AND A=$abc$2385$new_n74 B=$abc$2385$new_n466 Y=$abc$2385$new_n467
|
||||
.subckt NAND A=$abc$2385$new_n465 B=$abc$2385$new_n467 Y=$abc$2385$new_n468
|
||||
.subckt MUX A=$abc$2385$new_n73 B=$abc$2385$new_n137 S=$abc$2385$new_n76 Y=$abc$2385$new_n469
|
||||
.subckt OR A=$abc$2385$new_n74 B=$abc$2385$new_n469 Y=$abc$2385$new_n470
|
||||
.subckt NAND A=$abc$2385$new_n468 B=$abc$2385$new_n470 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[6]
|
||||
.subckt NAND A=$abc$2385$new_n392 B=$abc$2385$new_n467 Y=$abc$2385$new_n472
|
||||
.subckt ANDNOT A=$abc$2385$new_n137 B=$abc$2385$new_n76 Y=$abc$2385$new_n473
|
||||
.subckt XNOR A=$abc$2385$new_n150 B=$abc$2385$new_n473 Y=$abc$2385$new_n474
|
||||
.subckt AND A=$abc$2385$new_n472 B=$abc$2385$new_n474 Y=$abc$1802$auto$ghdl.cc:825:import_module$22[7]
|
||||
.subckt XOR A=$abc$2385$new_n90 B=$abc$2385$new_n96 Y=$abc$2385$new_n98
|
||||
.subckt AND A=$abc$2385$new_n58 B=$abc$2385$new_n438 Y=:38.Y[0]
|
||||
.subckt NAND A=in_a_var[1] B=$abc$2385$new_n74 Y=$abc$2385$new_n477
|
||||
.subckt NAND A=$abc$2385$new_n84 B=$abc$2385$new_n477 Y=:38.Y[1]
|
||||
.subckt NAND A=in_a_var[2] B=$abc$2385$new_n74 Y=$abc$2385$new_n479
|
||||
.subckt NAND A=$abc$2385$new_n92 B=$abc$2385$new_n479 Y=:38.Y[2]
|
||||
.subckt NAND A=in_a_var[3] B=$abc$2385$new_n74 Y=$abc$2385$new_n481
|
||||
.subckt NAND A=$abc$2385$new_n104 B=$abc$2385$new_n481 Y=:38.Y[3]
|
||||
.subckt NAND A=in_a_var[4] B=$abc$2385$new_n74 Y=$abc$2385$new_n483
|
||||
.subckt NAND A=$abc$2385$new_n116 B=$abc$2385$new_n483 Y=:38.Y[4]
|
||||
.subckt NAND A=in_a_var[5] B=$abc$2385$new_n74 Y=$abc$2385$new_n485
|
||||
.subckt NAND A=$abc$2385$new_n89 B=$abc$2385$new_n98 Y=$abc$2385$new_n99
|
||||
.subckt NAND A=$abc$2385$new_n127 B=$abc$2385$new_n485 Y=:38.Y[5]
|
||||
.subckt NAND A=in_a_var[6] B=$abc$2385$new_n74 Y=$abc$2385$new_n487
|
||||
.subckt NAND A=$abc$2385$new_n137 B=$abc$2385$new_n487 Y=:38.Y[6]
|
||||
.subckt NAND A=in_a_var[7] B=$abc$2385$new_n74 Y=$abc$2385$new_n489
|
||||
.subckt NAND A=$abc$2385$new_n150 B=$abc$2385$new_n489 Y=:38.Y[7]
|
||||
.subckt DFF C=clk D=$abc$2385$auto$maccmap.cc:114:fulladd$252.Y[0] Q=out_var[0]
|
||||
.subckt DFF C=clk D=$abc$2385$auto$maccmap.cc:240:synth$253.P[1] Q=out_var[1]
|
||||
.subckt DFF C=clk D=$abc$2385$auto$maccmap.cc:240:synth$253.Y[2] Q=out_var[2]
|
||||
.subckt DFF C=clk D=$abc$2385$auto$maccmap.cc:240:synth$253.Y[3] Q=out_var[3]
|
||||
.subckt DFF C=clk D=$abc$2385$auto$maccmap.cc:240:synth$253.Y[4] Q=out_var[4]
|
||||
.subckt XOR A=$abc$2385$new_n89 B=$abc$2385$new_n98 Y=$abc$2385$auto$maccmap.cc:240:synth$253.Y[2]
|
||||
.subckt DFF C=clk D=$abc$2385$auto$maccmap.cc:240:synth$253.Y[5] Q=out_var[5]
|
||||
.subckt DFF C=clk D=$abc$2385$auto$maccmap.cc:240:synth$253.Y[6] Q=out_var[6]
|
||||
.subckt DFF C=clk D=$abc$2385$auto$maccmap.cc:240:synth$253.Y[7] Q=out_var[7]
|
||||
.subckt DFF C=clk D=:38.Y[0] Q=:1.test_1[0]
|
||||
.subckt DFF C=clk D=:38.Y[1] Q=:1.test_1[1]
|
||||
.subckt DFF C=clk D=:38.Y[2] Q=:1.test_1[2]
|
||||
.subckt DFF C=clk D=:38.Y[3] Q=:1.test_1[3]
|
||||
.subckt DFF C=clk D=:38.Y[4] Q=:1.test_1[4]
|
||||
.subckt DFF C=clk D=:38.Y[5] Q=:1.test_1[5]
|
||||
.subckt DFF C=clk D=:38.Y[6] Q=:1.test_1[6]
|
||||
.subckt NAND A=$abc$2385$new_n97 B=$abc$2385$new_n99 Y=$abc$2385$new_n101
|
||||
.subckt DFF C=clk D=:38.Y[7] Q=:1.test_1[7]
|
||||
.subckt DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[0] Q=:1.test_2[0]
|
||||
.subckt DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[1] Q=:1.test_2[1]
|
||||
.subckt DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[2] Q=:1.test_2[2]
|
||||
.subckt DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[3] Q=:1.test_2[3]
|
||||
.subckt DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[4] Q=:1.test_2[4]
|
||||
.subckt DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[5] Q=:1.test_2[5]
|
||||
.subckt DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[6] Q=:1.test_2[6]
|
||||
.subckt DFF C=clk D=$abc$1802$auto$ghdl.cc:825:import_module$22[7] Q=:1.test_2[7]
|
||||
.subckt AND A=$abc$2385$new_n93 B=$abc$2385$new_n95 Y=$abc$2385$new_n102
|
||||
.subckt XNOR A=:1.test_1[3] B=$abc$2385$new_n67 Y=$abc$2385$new_n103
|
||||
.subckt AND A=$abc$2385$new_n83 B=$abc$2385$new_n103 Y=$abc$2385$new_n104
|
||||
.subckt ORNOT A=$abc$2385$new_n104 B=in_a_var[3] Y=$abc$2385$new_n105
|
||||
.subckt XOR A=in_b_var[0] B=$abc$2385$new_n59 Y=$abc$2385$auto$maccmap.cc:114:fulladd$252.Y[0]
|
||||
.subckt XNOR A=in_a_var[3] B=$abc$2385$new_n104 Y=$abc$2385$new_n106
|
||||
.subckt NAND A=in_b_var[3] B=$abc$2385$new_n106 Y=$abc$2385$new_n107
|
||||
.subckt XNOR A=in_b_var[3] B=$abc$2385$new_n106 Y=$abc$2385$new_n108
|
||||
.subckt OR A=$abc$2385$new_n102 B=$abc$2385$new_n108 Y=$abc$2385$new_n109
|
||||
.subckt XOR A=$abc$2385$new_n102 B=$abc$2385$new_n108 Y=$abc$2385$new_n110
|
||||
.subckt NAND A=$abc$2385$new_n101 B=$abc$2385$new_n110 Y=$abc$2385$new_n111
|
||||
.subckt XOR A=$abc$2385$new_n101 B=$abc$2385$new_n110 Y=$abc$2385$auto$maccmap.cc:240:synth$253.Y[3]
|
||||
.subckt NAND A=$abc$2385$new_n109 B=$abc$2385$new_n111 Y=$abc$2385$new_n113
|
||||
.subckt AND A=$abc$2385$new_n105 B=$abc$2385$new_n107 Y=$abc$2385$new_n114
|
||||
.subckt XNOR A=:1.test_1[4] B=$abc$2385$new_n68 Y=$abc$2385$new_n115
|
||||
.subckt NAND A=$abc$2385$new_n57 B=$abc$2385$new_n60 Y=$abc$2385$new_n62
|
||||
.subckt AND A=$abc$2385$new_n83 B=$abc$2385$new_n115 Y=$abc$2385$new_n116
|
||||
.subckt ORNOT A=$abc$2385$new_n116 B=in_a_var[4] Y=$abc$2385$new_n117
|
||||
.subckt XNOR A=in_a_var[4] B=$abc$2385$new_n116 Y=$abc$2385$new_n118
|
||||
.subckt NAND A=in_b_var[4] B=$abc$2385$new_n118 Y=$abc$2385$new_n119
|
||||
.subckt XNOR A=in_b_var[4] B=$abc$2385$new_n118 Y=$abc$2385$new_n120
|
||||
.subckt OR A=$abc$2385$new_n114 B=$abc$2385$new_n120 Y=$abc$2385$new_n121
|
||||
.subckt XOR A=$abc$2385$new_n114 B=$abc$2385$new_n120 Y=$abc$2385$new_n122
|
||||
.subckt NAND A=$abc$2385$new_n113 B=$abc$2385$new_n122 Y=$abc$2385$new_n123
|
||||
.subckt XOR A=$abc$2385$new_n113 B=$abc$2385$new_n122 Y=$abc$2385$auto$maccmap.cc:240:synth$253.Y[4]
|
||||
.subckt AND A=$abc$2385$new_n121 B=$abc$2385$new_n123 Y=$abc$2385$new_n125
|
||||
.subckt NOR A=:1.test_1[0] B=:1.test_1[1] Y=$abc$2385$new_n63
|
||||
.subckt AND A=$abc$2385$new_n117 B=$abc$2385$new_n119 Y=$abc$2385$new_n126
|
||||
.subckt AND A=$abc$2385$new_n77 B=$abc$2385$new_n83 Y=$abc$2385$new_n127
|
||||
.subckt ORNOT A=$abc$2385$new_n127 B=in_a_var[5] Y=$abc$2385$new_n128
|
||||
.subckt XNOR A=in_a_var[5] B=$abc$2385$new_n127 Y=$abc$2385$new_n129
|
||||
.subckt NAND A=in_b_var[5] B=$abc$2385$new_n129 Y=$abc$2385$new_n130
|
||||
.subckt XNOR A=in_b_var[5] B=$abc$2385$new_n129 Y=$abc$2385$new_n131
|
||||
.subckt OR A=$abc$2385$new_n126 B=$abc$2385$new_n131 Y=$abc$2385$new_n132
|
||||
.subckt NAND A=$abc$2385$new_n126 B=$abc$2385$new_n131 Y=$abc$2385$new_n133
|
||||
.subckt XOR A=$abc$2385$new_n126 B=$abc$2385$new_n131 Y=$abc$2385$new_n134
|
||||
.subckt XNOR A=$abc$2385$new_n125 B=$abc$2385$new_n134 Y=$abc$2385$auto$maccmap.cc:240:synth$253.Y[5]
|
||||
.subckt AND A=:1.test_1[0] B=:1.test_1[1] Y=$abc$2385$new_n64
|
||||
.subckt AND A=$abc$2385$new_n128 B=$abc$2385$new_n130 Y=$abc$2385$new_n136
|
||||
.subckt AND A=$abc$2385$new_n72 B=$abc$2385$new_n82 Y=$abc$2385$new_n137
|
||||
.subckt ORNOT A=$abc$2385$new_n137 B=in_a_var[6] Y=$abc$2385$new_n138
|
||||
.subckt XNOR A=in_a_var[6] B=$abc$2385$new_n137 Y=$abc$2385$new_n139
|
||||
.subckt NAND A=in_b_var[6] B=$abc$2385$new_n139 Y=$abc$2385$new_n140
|
||||
.subckt XNOR A=in_b_var[6] B=$abc$2385$new_n139 Y=$abc$2385$new_n141
|
||||
.subckt OR A=$abc$2385$new_n136 B=$abc$2385$new_n141 Y=$abc$2385$new_n142
|
||||
.subckt XOR A=$abc$2385$new_n136 B=$abc$2385$new_n141 Y=$abc$2385$new_n143
|
||||
.subckt NAND A=$abc$2385$new_n125 B=$abc$2385$new_n132 Y=$abc$2385$new_n144
|
||||
.subckt AND A=$abc$2385$new_n133 B=$abc$2385$new_n144 Y=$abc$2385$new_n145
|
||||
.subckt XOR A=:1.test_1[0] B=:1.test_1[1] Y=$abc$2385$new_n65
|
||||
.subckt NAND A=$abc$2385$new_n143 B=$abc$2385$new_n145 Y=$abc$2385$new_n146
|
||||
.subckt XOR A=$abc$2385$new_n143 B=$abc$2385$new_n145 Y=$abc$2385$auto$maccmap.cc:240:synth$253.Y[6]
|
||||
.subckt AND A=$abc$2385$new_n142 B=$abc$2385$new_n146 Y=$abc$2385$new_n148
|
||||
.subckt AND A=$abc$2385$new_n138 B=$abc$2385$new_n140 Y=$abc$2385$new_n149
|
||||
.subckt AND A=$abc$2385$new_n75 B=$abc$2385$new_n83 Y=$abc$2385$new_n150
|
||||
.subckt NOR A=in_b_var[7] B=in_a_var[7] Y=$abc$2385$new_n151
|
||||
.subckt XOR A=in_b_var[7] B=in_a_var[7] Y=$abc$2385$new_n152
|
||||
.subckt XNOR A=$abc$2385$new_n150 B=$abc$2385$new_n152 Y=$abc$2385$new_n153
|
||||
.subckt XNOR A=$abc$2385$new_n149 B=$abc$2385$new_n153 Y=$abc$2385$new_n154
|
||||
.subckt XNOR A=$abc$2385$new_n148 B=$abc$2385$new_n154 Y=$abc$2385$auto$maccmap.cc:240:synth$253.Y[7]
|
||||
.gateinit :1.test_2[7]=0
|
||||
.gateinit :1.test_2[6]=0
|
||||
.gateinit :1.test_2[5]=0
|
||||
.gateinit :1.test_2[4]=0
|
||||
.gateinit :1.test_2[3]=0
|
||||
.gateinit :1.test_2[2]=0
|
||||
.gateinit :1.test_2[1]=0
|
||||
.gateinit :1.test_2[0]=0
|
||||
.gateinit :1.test_1[7]=1
|
||||
.gateinit :1.test_1[6]=1
|
||||
.gateinit :1.test_1[5]=1
|
||||
.gateinit :1.test_1[4]=1
|
||||
.gateinit :1.test_1[3]=1
|
||||
.gateinit :1.test_1[2]=1
|
||||
.gateinit :1.test_1[1]=1
|
||||
.gateinit :1.test_1[0]=1
|
||||
.end
|
||||
2
tests/blif/gatesi.ys
Normal file
2
tests/blif/gatesi.ys
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
read_blif gatesi.blif
|
||||
write_blif -gatesi gatesi.blif.out
|
||||
|
|
@ -3,5 +3,9 @@ source ../common-env.sh
|
|||
set -e
|
||||
for x in *.ys; do
|
||||
echo "Running $x.."
|
||||
../../yosys -ql ${x%.ys}.log $x
|
||||
../../yosys --no-version -ql ${x%.ys}.log $x
|
||||
done
|
||||
|
||||
for x in *.blif; do
|
||||
diff $x.out $x.ok
|
||||
done
|
||||
190
tests/functional/test_smtbmc_witness_mismatch.py
Normal file
190
tests/functional/test_smtbmc_witness_mismatch.py
Normal file
|
|
@ -0,0 +1,190 @@
|
|||
import json
|
||||
import shutil
|
||||
import subprocess
|
||||
from pathlib import Path
|
||||
|
||||
import pytest
|
||||
|
||||
base_path = Path(__file__).resolve().parent.parent.parent
|
||||
|
||||
pytestmark = pytest.mark.skipif(shutil.which("z3") is None, reason="z3 not available")
|
||||
|
||||
def run(cmd, **kwargs):
|
||||
"""Run a command and assert it succeeds."""
|
||||
status = subprocess.run(cmd, **kwargs)
|
||||
assert status.returncode == 0, f"{cmd[0]} failed"
|
||||
return status
|
||||
|
||||
|
||||
def write_smt2(tmp_path, verilog_text):
|
||||
"""Write Verilog to temp and emit SMT2 via yosys."""
|
||||
vfile = tmp_path / "design.v"
|
||||
smt2 = tmp_path / "design.smt2"
|
||||
vfile.write_text(verilog_text)
|
||||
run([base_path / "yosys", "-Q", "-p",
|
||||
f"read_verilog {vfile}; prep -top top; write_smt2 {smt2}"])
|
||||
return smt2
|
||||
|
||||
|
||||
def witness_entries(smt2_path):
|
||||
"""Parse yosys-smt2-witness JSON records from an SMT2 file."""
|
||||
entries = []
|
||||
marker = "yosys-smt2-witness"
|
||||
with open(smt2_path, "r") as f:
|
||||
for line in f:
|
||||
if marker not in line:
|
||||
continue
|
||||
payload = line.split(marker, 1)[1].strip()
|
||||
entries.append(json.loads(payload))
|
||||
return entries
|
||||
|
||||
|
||||
def find_entry(entries, entry_type):
|
||||
"""Return the first witness entry of the given type."""
|
||||
for entry in entries:
|
||||
if entry.get("type") == entry_type:
|
||||
return entry
|
||||
return None
|
||||
|
||||
|
||||
def write_yw(yw_path, signals, bits):
|
||||
"""Write a minimal Yosys witness file with one step of bits."""
|
||||
data = {
|
||||
"format": "Yosys Witness Trace",
|
||||
"clocks": [],
|
||||
"signals": signals,
|
||||
"steps": [{"bits": bits}],
|
||||
}
|
||||
yw_path.write_text(json.dumps(data))
|
||||
|
||||
|
||||
def run_smtbmc(smt2_path, yw_path):
|
||||
"""Run yosys-smtbmc on the SMT2 file with a witness trace."""
|
||||
cmd = [
|
||||
base_path / "yosys-smtbmc",
|
||||
"-s", "z3",
|
||||
"-m", "top",
|
||||
"--check-witness",
|
||||
"--yw", yw_path,
|
||||
"-t", "1",
|
||||
smt2_path,
|
||||
]
|
||||
return subprocess.run(cmd, capture_output=True, text=True)
|
||||
|
||||
|
||||
def assert_no_mismatch_message(result):
|
||||
"""Assert the mismatch error prefix is absent from outputs."""
|
||||
combined = (result.stderr or "") + (result.stdout or "")
|
||||
assert "Yosys witness signal mismatch" not in combined
|
||||
|
||||
|
||||
def assert_has_mismatch_message(result, msg):
|
||||
"""Assert the mismatch error prefix and substring are present."""
|
||||
combined = (result.stderr or "") + (result.stdout or "")
|
||||
assert "Yosys witness signal mismatch" in combined
|
||||
assert msg in combined
|
||||
|
||||
|
||||
def test_missing_signal_path(tmp_path):
|
||||
smt2 = write_smt2(tmp_path, "module top(input ok, output out); assign out = ok; endmodule")
|
||||
yw_path = tmp_path / "trace.yw"
|
||||
signals = [{"path": ["\\missing"], "offset": 0, "width": 1, "init_only": False}]
|
||||
write_yw(yw_path, signals, "1")
|
||||
result = run_smtbmc(smt2, yw_path)
|
||||
assert result.returncode != 0
|
||||
assert_has_mismatch_message(result, "signal not found in design")
|
||||
|
||||
|
||||
def test_width_mismatch(tmp_path):
|
||||
smt2 = write_smt2(tmp_path, "module top(input ok, output out); assign out = ok; endmodule")
|
||||
entries = witness_entries(smt2)
|
||||
input_entry = find_entry(entries, "input")
|
||||
assert input_entry is not None
|
||||
yw_path = tmp_path / "trace.yw"
|
||||
signals = [{
|
||||
"path": input_entry["path"],
|
||||
"offset": 0,
|
||||
"width": 2,
|
||||
"init_only": False,
|
||||
}]
|
||||
write_yw(yw_path, signals, "10")
|
||||
result = run_smtbmc(smt2, yw_path)
|
||||
assert result.returncode != 0
|
||||
assert_has_mismatch_message(result, "signal width/offset mismatch")
|
||||
|
||||
|
||||
def test_memory_address_oob(tmp_path):
|
||||
verilog = """
|
||||
module top(input ok, output [7:0] mem_out);
|
||||
reg [7:0] mem [0:1];
|
||||
assign mem_out = mem[0] ^ {8{ok}};
|
||||
endmodule
|
||||
"""
|
||||
smt2 = write_smt2(tmp_path, verilog)
|
||||
entries = witness_entries(smt2)
|
||||
mem_entry = find_entry(entries, "mem")
|
||||
assert mem_entry is not None
|
||||
addr = mem_entry["size"]
|
||||
yw_path = tmp_path / "trace.yw"
|
||||
signals = [{
|
||||
"path": mem_entry["path"] + [f"\\[{addr}]"],
|
||||
"offset": 0,
|
||||
"width": mem_entry["width"],
|
||||
"init_only": False,
|
||||
}]
|
||||
bits = "0" * mem_entry["width"]
|
||||
write_yw(yw_path, signals, bits)
|
||||
result = run_smtbmc(smt2, yw_path)
|
||||
assert result.returncode != 0
|
||||
assert_has_mismatch_message(result, "memory address out of bounds")
|
||||
|
||||
|
||||
def test_allowed_extra_signal_in_design(tmp_path):
|
||||
verilog = """
|
||||
module top(input ok, input extra, output [1:0] out);
|
||||
assign out = {ok, extra};
|
||||
endmodule
|
||||
"""
|
||||
smt2 = write_smt2(tmp_path, verilog)
|
||||
entries = witness_entries(smt2)
|
||||
input_entry = find_entry(entries, "input")
|
||||
assert input_entry is not None
|
||||
yw_path = tmp_path / "trace.yw"
|
||||
signals = [{
|
||||
"path": input_entry["path"],
|
||||
"offset": 0,
|
||||
"width": input_entry["width"],
|
||||
"init_only": False,
|
||||
}]
|
||||
bits = "0" * input_entry["width"]
|
||||
write_yw(yw_path, signals, bits)
|
||||
result = run_smtbmc(smt2, yw_path)
|
||||
# With --check-witness and no assertions, smtbmc can still exit non-zero.
|
||||
# Thus we don't check the result.returncode here and in the other success
|
||||
# cases.
|
||||
assert_no_mismatch_message(result)
|
||||
|
||||
|
||||
def test_allowed_extra_memory_in_design(tmp_path):
|
||||
verilog = """
|
||||
module top(input ok, output [7:0] out);
|
||||
reg [7:0] mem0 [0:1];
|
||||
reg [7:0] mem1 [0:3];
|
||||
assign out = mem0[0] ^ mem1[0];
|
||||
endmodule
|
||||
"""
|
||||
smt2 = write_smt2(tmp_path, verilog)
|
||||
entries = witness_entries(smt2)
|
||||
input_entry = find_entry(entries, "input")
|
||||
assert input_entry is not None
|
||||
yw_path = tmp_path / "trace.yw"
|
||||
signals = [{
|
||||
"path": input_entry["path"],
|
||||
"offset": 0,
|
||||
"width": input_entry["width"],
|
||||
"init_only": False,
|
||||
}]
|
||||
bits = "1" * input_entry["width"]
|
||||
write_yw(yw_path, signals, bits)
|
||||
result = run_smtbmc(smt2, yw_path)
|
||||
assert_no_mismatch_message(result)
|
||||
1246
tests/opt/opt_balance_tree.ys
Normal file
1246
tests/opt/opt_balance_tree.ys
Normal file
File diff suppressed because it is too large
Load diff
10
tests/opt/opt_clean_standalone_wires.ys
Normal file
10
tests/opt/opt_clean_standalone_wires.ys
Normal file
|
|
@ -0,0 +1,10 @@
|
|||
read_rtlil << EOT
|
||||
module \test
|
||||
wire \wire_a
|
||||
wire \wire_f
|
||||
connect \wire_f \wire_a
|
||||
end
|
||||
EOT
|
||||
|
||||
opt_clean
|
||||
select -assert-count 0 */*
|
||||
|
|
@ -319,3 +319,59 @@ check
|
|||
equiv_opt -assert opt_expr -keepdc
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$mul r:A_WIDTH=4 %i r:B_WIDTH=4 %i r:Y_WIDTH=8 %i
|
||||
|
||||
###########
|
||||
|
||||
design -reset
|
||||
read_rtlil <<EOF
|
||||
module \top
|
||||
wire width 3 input 2 \binary
|
||||
|
||||
wire width 32 output 3 \y
|
||||
|
||||
cell $pow $0
|
||||
parameter \A_WIDTH 32
|
||||
parameter \B_WIDTH 3
|
||||
parameter \A_SIGNED 1
|
||||
parameter \B_SIGNED 0
|
||||
parameter \Y_WIDTH 32
|
||||
connect \A 2
|
||||
connect \B \binary
|
||||
connect \Y \y
|
||||
end
|
||||
end
|
||||
EOF
|
||||
|
||||
scratchpad -set opt.did_something false
|
||||
opt_expr
|
||||
scratchpad -assert opt.did_something true
|
||||
sat -verify -set binary 0 -prove y 1
|
||||
sat -verify -set binary 1 -prove y 2
|
||||
sat -verify -set binary 2 -prove y 4
|
||||
sat -verify -set binary 3 -prove y 8
|
||||
|
||||
###########
|
||||
|
||||
design -reset
|
||||
read_rtlil <<EOF
|
||||
module \top
|
||||
wire width 3 input 2 \binary
|
||||
|
||||
wire width 32 output 3 \y
|
||||
|
||||
cell $pow $0
|
||||
parameter \A_WIDTH 2
|
||||
parameter \B_WIDTH 3
|
||||
parameter \A_SIGNED 1
|
||||
parameter \B_SIGNED 0
|
||||
parameter \Y_WIDTH 32
|
||||
connect \A 2'10
|
||||
connect \B \binary
|
||||
connect \Y \y
|
||||
end
|
||||
end
|
||||
EOF
|
||||
|
||||
scratchpad -set opt.did_something false
|
||||
opt_expr
|
||||
scratchpad -assert opt.did_something false
|
||||
|
|
@ -1,11 +1,12 @@
|
|||
read_verilog -sv <<EOT
|
||||
module opt_expr_or_test(input [3:0] i, input [7:0] j, output [8:0] o);
|
||||
wire[8:0] a = 8'b0;
|
||||
wire[8:0] a;
|
||||
initial begin
|
||||
a = 8'b0;
|
||||
a |= i;
|
||||
a |= j;
|
||||
end
|
||||
assign o = a;
|
||||
assign o = a;
|
||||
endmodule
|
||||
EOT
|
||||
proc
|
||||
|
|
@ -17,12 +18,13 @@ select -assert-count 1 t:$or r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=4 %i %i %i
|
|||
design -reset
|
||||
read_verilog -sv <<EOT
|
||||
module opt_expr_add_test(input [3:0] i, input [7:0] j, output [8:0] o);
|
||||
wire[8:0] a = 8'b0;
|
||||
wire[8:0] a;
|
||||
initial begin
|
||||
a += i;
|
||||
a += j;
|
||||
a = 8'b0;
|
||||
a += i;
|
||||
a += j;
|
||||
end
|
||||
assign o = a;
|
||||
assign o = a;
|
||||
endmodule
|
||||
EOT
|
||||
proc
|
||||
|
|
@ -34,12 +36,13 @@ select -assert-count 1 t:$add r:A_WIDTH=9 r:B_WIDTH=8 r:Y_WIDTH=9 %i %i %i
|
|||
design -reset
|
||||
read_verilog -sv <<EOT
|
||||
module opt_expr_xor_test(input [3:0] i, input [7:0] j, output [8:0] o);
|
||||
wire[8:0] a = 8'b0;
|
||||
wire[8:0] a;
|
||||
initial begin
|
||||
a ^= i;
|
||||
a ^= j;
|
||||
a = 8'b0;
|
||||
a ^= i;
|
||||
a ^= j;
|
||||
end
|
||||
assign o = a;
|
||||
assign o = a;
|
||||
endmodule
|
||||
EOT
|
||||
proc
|
||||
|
|
@ -51,12 +54,13 @@ select -assert-count 1 t:$xor r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=4 %i %i %i
|
|||
design -reset
|
||||
read_verilog -sv <<EOT
|
||||
module opt_expr_sub_test(input [3:0] i, input [7:0] j, output [8:0] o);
|
||||
wire[8:0] a = 8'b0;
|
||||
wire[8:0] a;
|
||||
initial begin
|
||||
a -= i;
|
||||
a -= j;
|
||||
a = 8'b0;
|
||||
a -= i;
|
||||
a -= j;
|
||||
end
|
||||
assign o = a;
|
||||
assign o = a;
|
||||
endmodule
|
||||
EOT
|
||||
proc
|
||||
|
|
@ -68,12 +72,13 @@ select -assert-count 1 t:$sub r:A_WIDTH=9 r:B_WIDTH=8 r:Y_WIDTH=9 %i %i %i
|
|||
design -reset
|
||||
read_verilog -sv <<EOT
|
||||
module opt_expr_and_test(input [3:0] i, input [7:0] j, output [8:0] o);
|
||||
wire[8:0] a = 8'b11111111;
|
||||
wire[8:0] a;
|
||||
initial begin
|
||||
a &= i;
|
||||
a &= j;
|
||||
a = 8'b11111111;
|
||||
a &= i;
|
||||
a &= j;
|
||||
end
|
||||
assign o = a;
|
||||
assign o = a;
|
||||
endmodule
|
||||
EOT
|
||||
proc
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@ foreach fn [glob opt_hier_*.v] {
|
|||
design -copy-from gate -as gate A:top
|
||||
yosys rename -hide
|
||||
equiv_make gold gate equiv
|
||||
equiv_induct equiv
|
||||
equiv_induct -ignore-unknown-cells equiv
|
||||
equiv_status -assert equiv
|
||||
|
||||
log -pop
|
||||
|
|
|
|||
106
tests/pass-fuzzing.md
Normal file
106
tests/pass-fuzzing.md
Normal file
|
|
@ -0,0 +1,106 @@
|
|||
Suppose you're making significant changes to a pass that should not change
|
||||
the pass's output in any way. It might be useful to run a large number of
|
||||
automatically generated tests to try to find bugs where the output has
|
||||
changed. This document describes how to do that.
|
||||
|
||||
Basically we're going to use [AFL++](https://github.com/AFLplusplus/AFLplusplus) with the
|
||||
[Grammar-Mutator](https://github.com/AFLplusplus/Grammar-Mutator) plugin to generate
|
||||
RTLIL testcases. For each testcase, we run a Yosys script that applies both the old and new
|
||||
implementation of the pass to the same design and compares the results. Testcase
|
||||
generation is coverage-guided, i.e. the fuzzer will try to find testcases that exercise all
|
||||
code in the old and new implementation of the pass (and in the RTLIL parser).
|
||||
|
||||
## Setup
|
||||
|
||||
These instructions clone tools into subdirectories of your home directory. They assume
|
||||
you have a Yosys checkout under `$HOME/yosys`, and that you're testing the `opt_merge` pass.
|
||||
They have been tested with AFL++ revision 68b492b2c7725816068718ef9437b72b40e67519 and Grammar-Mutator revision 05d8f537f8d656f0754e7ad5dcc653c42cb4f8ff.
|
||||
|
||||
Clone and build AFL++ and Grammar-Mutator:
|
||||
```
|
||||
cd $HOME
|
||||
git clone https://github.com/AFLplusplus/AFLplusplus.git
|
||||
git -C AFLplusplus checkout stable
|
||||
git clone https://github.com/AFLplusplus/Grammar-Mutator.git
|
||||
git -C Grammar-Mutator checkout stable
|
||||
```
|
||||
|
||||
Check that `rtlil-fuzz-grammar.json` generates RTLIL constructs relevant to your pass.
|
||||
Currently it's quite simple and generates a limited set of cells and wires; you may need to
|
||||
extend it to generate different kinds of cells and other RTLIL constructs (e.g. `proc`).
|
||||
|
||||
Build AFL++ and Grammar-Mutator:
|
||||
```
|
||||
make -C $HOME/AFLplusplus -j all
|
||||
make -C $HOME/Grammar-Mutator -j GRAMMAR_FILE=$HOME/yosys/tests/tools/rtlil-fuzz-grammar.json
|
||||
```
|
||||
|
||||
Create a Yosys commit that adds the old version of your pass as a new command, e.g. copy
|
||||
`opt_merge.cc` into `old_opt_merge.cc` and change the name of the command to `old_opt_merge`.
|
||||
[Here's](https://github.com/YosysHQ/yosys/commit/827cd8c998f3e455b14ac990a3159030ddc19b21) an example.
|
||||
|
||||
You may also need to patch in [this commit](https://github.com/YosysHQ/yosys/commit/121c52f514c4ca282b4e6b3b14f71184f3849ddf) to work around a bug involving `std::reverse` on
|
||||
empty vectors in the RTLIL parser when building with fuzzing instrumentation.
|
||||
I think this is a clang++ bug so hopefully it will get fixed eventually and that patch will not be
|
||||
necessary.
|
||||
|
||||
Rebuild Yosys with the AFL++ compiler wrapper. This assumes your config builds Yosys with clang++.
|
||||
```
|
||||
(cd $HOME/yosys; patch -lp1 << EOF)
|
||||
diff --git a/Makefile b/Makefile
|
||||
index 9c361294d..c9a98f74c 100644
|
||||
--- a/Makefile
|
||||
+++ b/Makefile
|
||||
@@ -238,7 +238,7 @@
|
||||
LTOFLAGS := $(GCC_LTO)
|
||||
|
||||
ifeq ($(CONFIG),clang)
|
||||
-CXX = clang++
|
||||
+CXX = $(HOME)/AFLplusplus/afl-c++
|
||||
CXXFLAGS += -std=$(CXXSTD) $(OPT_LEVEL)
|
||||
ifeq ($(ENABLE_LTO),1)
|
||||
LINKFLAGS += -fuse-ld=lld
|
||||
EOF
|
||||
make -C yosys clean && make -C yosys -j
|
||||
```
|
||||
|
||||
You probably need to configure coredumps to work normally instead of going through some OS service:
|
||||
```
|
||||
echo core | sudo tee /proc/sys/kernel/core_pattern
|
||||
```
|
||||
|
||||
## Running the fuzzer
|
||||
|
||||
Generate some initial testcases using Grammar-Mutator:
|
||||
```
|
||||
(cd $HOME/Grammar-Mutator; rm -rf seeds trees; ./grammar_generator-rtlil 100 1000 ./seeds ./trees)
|
||||
```
|
||||
|
||||
Now run AFL++.
|
||||
```
|
||||
(cd $HOME/Grammar-Mutator; \
|
||||
AFL_CUSTOM_MUTATOR_LIBRARY=./libgrammarmutator-rtlil.so \
|
||||
AFL_CUSTOM_MUTATOR_ONLY=1 \
|
||||
AFL_BENCH_UNTIL_CRASH=1 \
|
||||
YOSYS_WORK_UNITS_PER_THREAD=1 \
|
||||
YOSYS_ABORT_ON_LOG_ERROR=1 \
|
||||
$HOME/AFLplusplus/afl-fuzz -t 5000 -m none -i seeds -o out -- \
|
||||
$HOME/yosys/yosys -p 'read_rtlil -legalize @@; design -save init; old_opt_merge; design -save old; design -load init; opt_merge; design_equal old' \
|
||||
)
|
||||
```
|
||||
This will run the fuzzer until the first crash (including any pass output mismatches) and then stop.
|
||||
Or if you're lucky, the fuzzer will run indefinitely. This uses very little parallelism; if it doesn't find any errors right away, you can increase the test throughput by running AFL++ in parallel using the instructions [here](https://aflplus.plus/docs/parallel_fuzzing).
|
||||
|
||||
## Working with fuzz test failures
|
||||
|
||||
Any failing testcases will be dropped in `$HOME/Grammar-Mutator/out/default/crashes`.
|
||||
Run `yosys -p 'read_rtlil -legalize ... ; dump'` to get the testcase as legalized RTLIL.
|
||||
|
||||
## Notes on generating semantically valid RTLIL
|
||||
|
||||
`Grammar-Mutator` generates RTLIL files according to the context-free grammar in `rtlil-fuzz-grammar.json`.
|
||||
However, the testcases must also be semantically valid, e.g. references to wires should only refer to
|
||||
wires that actually exist. These constraints cannot reasonably be expresed in a CFG. Therefore we
|
||||
have added a `-legalize` option to the `read_rtlil` command. When `-legalize` is set, when `read_rtlil`
|
||||
detects a failed semantic check, instead of erroring out it emits a warning and patches the incoming RTLIL
|
||||
to make it valid.
|
||||
19
tests/proc/bug5572.ys
Normal file
19
tests/proc/bug5572.ys
Normal file
|
|
@ -0,0 +1,19 @@
|
|||
read_rtlil << EOT
|
||||
attribute \top 1
|
||||
module \top
|
||||
wire width 1 \sig
|
||||
wire width 1 \val
|
||||
|
||||
process $2
|
||||
switch \sig [0]
|
||||
case 1'0
|
||||
case 1'1
|
||||
case
|
||||
assign \val [0] 1'1
|
||||
end
|
||||
end
|
||||
end
|
||||
EOT
|
||||
proc_rmdead
|
||||
proc_clean
|
||||
select -assert-none p:*
|
||||
20
tests/pyosys/test_design_run_pass.py
Normal file
20
tests/pyosys/test_design_run_pass.py
Normal file
|
|
@ -0,0 +1,20 @@
|
|||
from pathlib import Path
|
||||
from pyosys import libyosys as ys
|
||||
|
||||
__file_dir__ = Path(__file__).absolute().parent
|
||||
add_sub = __file_dir__.parent / "arch" / "common" / "add_sub.v"
|
||||
|
||||
base = ys.Design()
|
||||
base.run_pass(["read_verilog", str(add_sub)])
|
||||
base.run_pass("hierarchy -top top")
|
||||
base.run_pass(["proc"])
|
||||
base.run_pass("equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5")
|
||||
|
||||
postopt = ys.Design()
|
||||
postopt.run_pass("design -load postopt")
|
||||
postopt.run_pass(["cd", "top"])
|
||||
postopt.run_pass("select -assert-min 25 t:LUT4")
|
||||
postopt.run_pass("select -assert-max 26 t:LUT4")
|
||||
postopt.run_pass(["select", "-assert-count", "10", "t:PFUMX"])
|
||||
postopt.run_pass(["select", "-assert-count", "6", "t:L6MUX21"])
|
||||
postopt.run_pass("select -assert-none t:LUT4 t:PFUMX t:L6MUX21 %% t:* %D")
|
||||
|
|
@ -33,12 +33,3 @@ assert repr_test == {'tomato': 'tomato', 'first': 'second', 'key': 'value', 'im
|
|||
before = len(repr_test)
|
||||
print(repr_test.popitem())
|
||||
assert before - 1 == len(repr_test)
|
||||
|
||||
# test noncomparable
|
||||
## if ys.CellType ever gets an == operator just disable this section
|
||||
uncomparable_value = ys.Globals.yosys_celltypes.cell_types[ys.IdString("$not")]
|
||||
|
||||
x = ys.IdstringToCelltypeDict({ ys.IdString("\\a"): uncomparable_value})
|
||||
y = ys.IdstringToCelltypeDict({ ys.IdString("\\a"): uncomparable_value})
|
||||
|
||||
assert x != y # not comparable
|
||||
|
|
|
|||
87
tests/svtypes/array_assign.sv
Normal file
87
tests/svtypes/array_assign.sv
Normal file
|
|
@ -0,0 +1,87 @@
|
|||
// Test for array-to-array assignment and ternary expressions
|
||||
|
||||
`define STRINGIFY(x) `"x`"
|
||||
`define STATIC_ASSERT(x) if(!(x)) $error({"assert failed: ", `STRINGIFY(x)})
|
||||
|
||||
module top;
|
||||
// Test 1: Basic array ternary with continuous assignment
|
||||
reg [7:0] a1[4];
|
||||
reg [7:0] b1[4];
|
||||
wire [7:0] out1[4];
|
||||
wire sel1;
|
||||
assign out1 = sel1 ? a1 : b1;
|
||||
`STATIC_ASSERT($bits(out1) == 32);
|
||||
|
||||
// Test 2: Non-zero base index
|
||||
reg [7:0] a2[3:6];
|
||||
reg [7:0] b2[3:6];
|
||||
wire [7:0] out2[3:6];
|
||||
wire sel2;
|
||||
assign out2 = sel2 ? a2 : b2;
|
||||
`STATIC_ASSERT($bits(out2) == 32);
|
||||
|
||||
// Test 3: Single-bit elements
|
||||
reg a3[8];
|
||||
reg b3[8];
|
||||
wire out3[8];
|
||||
wire sel3;
|
||||
assign out3 = sel3 ? a3 : b3;
|
||||
`STATIC_ASSERT($bits(out3) == 8);
|
||||
|
||||
// Test 4: Multi-dimensional array ternary
|
||||
reg [7:0] a4[2][3];
|
||||
reg [7:0] b4[2][3];
|
||||
wire [7:0] out4[2][3];
|
||||
wire sel4;
|
||||
assign out4 = sel4 ? a4 : b4;
|
||||
`STATIC_ASSERT($bits(out4) == 48);
|
||||
|
||||
// Test 5: Direct array assignment (continuous)
|
||||
reg [7:0] a5[4];
|
||||
wire [7:0] b5[4];
|
||||
assign b5 = a5;
|
||||
`STATIC_ASSERT($bits(b5) == 32);
|
||||
|
||||
// Test 6: Multi-dimensional direct assignment (continuous)
|
||||
reg [7:0] a6[2][3];
|
||||
wire [7:0] b6[2][3];
|
||||
assign b6 = a6;
|
||||
`STATIC_ASSERT($bits(b6) == 48);
|
||||
|
||||
// Test 7: Procedural direct assignment with different unpacked index ranges
|
||||
// Covers the AST_BLOCK expansion path for AST_ASSIGN_EQ.
|
||||
logic pa [1:0][1:0];
|
||||
logic pb [1:0][0:1];
|
||||
always_comb begin
|
||||
pa[0][0] = 1'b0;
|
||||
pa[0][1] = 1'b1;
|
||||
pa[1][0] = 1'b1;
|
||||
pa[1][1] = 1'b1;
|
||||
|
||||
pb = pa;
|
||||
|
||||
assert(pb[0][1] == 1'b0);
|
||||
assert(pb[0][0] == 1'b1);
|
||||
assert(pb[1][1] == 1'b1);
|
||||
assert(pb[1][0] == 1'b1);
|
||||
end
|
||||
|
||||
// Test 8: Procedural ternary assignment on arrays
|
||||
// Covers the AST_BLOCK expansion path for ternary RHS.
|
||||
logic pt_a [1:0];
|
||||
logic pt_b [1:0];
|
||||
logic pt_o [1:0];
|
||||
logic pt_sel;
|
||||
always_comb begin
|
||||
pt_a[0] = 1'b0;
|
||||
pt_a[1] = 1'b1;
|
||||
pt_b[0] = 1'b1;
|
||||
pt_b[1] = 1'b0;
|
||||
pt_sel = 1'b1;
|
||||
|
||||
pt_o = pt_sel ? pt_a : pt_b;
|
||||
|
||||
assert(pt_o[0] == 1'b0);
|
||||
assert(pt_o[1] == 1'b1);
|
||||
end
|
||||
endmodule
|
||||
19
tests/techmap/abc9-nonbox-loop-with-box.ys
Normal file
19
tests/techmap/abc9-nonbox-loop-with-box.ys
Normal file
|
|
@ -0,0 +1,19 @@
|
|||
read_verilog -icells -specify <<EOT
|
||||
(* abc9_box, blackbox *)
|
||||
module box1(input i, output o);
|
||||
specify
|
||||
(i => o) = 1;
|
||||
endspecify
|
||||
endmodule
|
||||
|
||||
module top(input i, output o);
|
||||
wire a, b, c, z;
|
||||
$_AND_ a0(.A(b), .B(i), .Y(a));
|
||||
$_AND_ b0(.A(a), .B(c), .Y(b));
|
||||
$_AND_ c0(.A(b), .B(i), .Y(c));
|
||||
box1 u_box(.i(i), .o(z));
|
||||
assign o = c ^ z;
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
abc9 -lut 4
|
||||
13
tests/techmap/abc_temp_dir_sanitization.ys
Normal file
13
tests/techmap/abc_temp_dir_sanitization.ys
Normal file
|
|
@ -0,0 +1,13 @@
|
|||
read_verilog <<EOT
|
||||
module simple(I1, I2, O);
|
||||
input wire I1;
|
||||
input wire I2;
|
||||
output wire O;
|
||||
|
||||
assign O = I1 | I2;
|
||||
endmodule
|
||||
EOT
|
||||
techmap
|
||||
|
||||
logger -warn " /tmp/" -werror " /tmp/"
|
||||
abc -g all
|
||||
11
tests/techmap/bug5574.ys
Normal file
11
tests/techmap/bug5574.ys
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
# On Linux, with a spawned abc, this message is the error
|
||||
# otherwise the error is the failure to load the output.blif
|
||||
logger -expect log "ABC: Error: This command can only be applied to an AIG" 1
|
||||
logger -expect error "ABC" 1
|
||||
read_verilog << EOT
|
||||
module fuzz_mwoqk (input i0, output o0);
|
||||
assign o0 = i0 ^ 1;
|
||||
endmodule
|
||||
EOT
|
||||
synth
|
||||
abc -script +resub,-K,8;
|
||||
24
tests/techmap/lut2bmux.ys
Normal file
24
tests/techmap/lut2bmux.ys
Normal file
|
|
@ -0,0 +1,24 @@
|
|||
read_rtlil << EOT
|
||||
module \top
|
||||
wire width 4 input 0 \A
|
||||
wire output 1 \Y
|
||||
|
||||
cell $lut $0
|
||||
parameter \WIDTH 4
|
||||
parameter \LUT 16'0110100110010110
|
||||
connect \A \A
|
||||
connect \Y \Y
|
||||
end
|
||||
end
|
||||
EOT
|
||||
|
||||
hierarchy -auto-top
|
||||
|
||||
|
||||
equiv_opt -assert lut2bmux
|
||||
|
||||
|
||||
lut2bmux
|
||||
|
||||
select -assert-count 0 t:$lut
|
||||
select -assert-count 1 t:$bmux r:WIDTH=1 r:S_WIDTH=4 %i
|
||||
42
tests/techmap/lut2mux.ys
Normal file
42
tests/techmap/lut2mux.ys
Normal file
|
|
@ -0,0 +1,42 @@
|
|||
# Test lut2mux pass using a directly constructed $lut (avoids frontend/synth differences in test-verific)
|
||||
|
||||
read_rtlil << EOT
|
||||
module \top
|
||||
wire width 2 input 1 \a
|
||||
wire width 1 output 2 \y
|
||||
cell $lut \u_lut
|
||||
parameter \WIDTH 2
|
||||
parameter \LUT 4'0110
|
||||
connect \A \a
|
||||
connect \Y \y
|
||||
end
|
||||
end
|
||||
EOT
|
||||
|
||||
select -assert-count 1 t:$lut
|
||||
|
||||
# default mode -> gate-level $_MUX_
|
||||
design -save gold
|
||||
lut2mux
|
||||
rename \top \gate
|
||||
select -assert-count 3 gate/t:$_MUX_
|
||||
select -assert-count 0 gate/t:$mux
|
||||
select -assert-count 0 gate/t:$lut
|
||||
|
||||
# -word mode -> word-level $mux
|
||||
design -copy-from gold -as top \top
|
||||
select -none
|
||||
select top
|
||||
lut2mux -word
|
||||
select -clear
|
||||
rename \top \word
|
||||
select -assert-count 3 word/t:$mux
|
||||
select -assert-count 0 word/t:$_MUX_
|
||||
select -assert-count 0 gate/t:$lut
|
||||
|
||||
# equivalence
|
||||
equiv_make \gate \word equiv
|
||||
hierarchy -top equiv
|
||||
equiv_simple
|
||||
equiv_induct
|
||||
equiv_status -assert
|
||||
31
tests/techmap/module_not_derived.ys
Normal file
31
tests/techmap/module_not_derived.ys
Normal file
|
|
@ -0,0 +1,31 @@
|
|||
# Test 1: internal cells from alumacc/techmap must not keep module_not_derived.
|
||||
read_verilog <<EOF_VERILOG
|
||||
module top(a, b, y);
|
||||
input wire [7:0] a;
|
||||
input wire [7:0] b;
|
||||
output wire [7:0] y;
|
||||
assign y = a + b;
|
||||
endmodule
|
||||
EOF_VERILOG
|
||||
|
||||
prep
|
||||
alumacc
|
||||
techmap -max_iter 1
|
||||
|
||||
select -assert-any t:$lcu
|
||||
select -assert-count 0 t:$lcu a:module_not_derived %i
|
||||
|
||||
design -reset
|
||||
# Test 2: public module instances should still keep module_not_derived.
|
||||
read_verilog <<EOF_VERILOG
|
||||
module mycell(input a, output y);
|
||||
assign y = a;
|
||||
endmodule
|
||||
|
||||
module top(input a, output y);
|
||||
mycell u0(.a(a), .y(y));
|
||||
endmodule
|
||||
EOF_VERILOG
|
||||
|
||||
hierarchy -top top
|
||||
select -assert-any t:mycell a:module_not_derived %i
|
||||
104
tests/tools/rtlil-fuzz-grammar.json
Normal file
104
tests/tools/rtlil-fuzz-grammar.json
Normal file
|
|
@ -0,0 +1,104 @@
|
|||
{
|
||||
"<MODULE>": [
|
||||
[
|
||||
"module \\test\n",
|
||||
"<WIRE>", "<WIRES>",
|
||||
"<CELLS>",
|
||||
"<CONNECTS>",
|
||||
"end\n"
|
||||
]
|
||||
],
|
||||
"<WIRE>": [ [ " wire width ", "<WIDTH>", " ", "<WIRE_MODE>", " ", "<WIRE_ID>", "\n" ] ],
|
||||
"<WIDTH>": [ [ "1" ], [ "2" ], [ "3" ], [ "4" ], [ "32" ], [ "128" ] ],
|
||||
"<WIRE_MODE>": [ [ "input ", "<PORT_ID>" ], [ "output ", "<PORT_ID>" ], [ "inout ", "<PORT_ID>" ], [] ],
|
||||
"<CELL>": [
|
||||
[
|
||||
" cell $not ", "<CELL_ID>", "\n",
|
||||
" parameter \\A_SIGNED 0\n",
|
||||
" parameter \\A_WIDTH 0\n",
|
||||
" parameter \\Y_WIDTH 0\n",
|
||||
" connect \\A ", "<SIGSPEC>", "\n",
|
||||
" connect \\Y ", "<SIGSPEC>", "\n",
|
||||
" end\n"
|
||||
],
|
||||
[
|
||||
" cell $and ", "<CELL_ID>", "\n",
|
||||
" parameter \\A_SIGNED 0\n",
|
||||
" parameter \\B_SIGNED 0\n",
|
||||
" parameter \\A_WIDTH 0\n",
|
||||
" parameter \\B_WIDTH 0\n",
|
||||
" parameter \\Y_WIDTH 0\n",
|
||||
" connect \\A ", "<SIGSPEC>", "\n",
|
||||
" connect \\B ", "<SIGSPEC>", "\n",
|
||||
" connect \\Y ", "<SIGSPEC>", "\n",
|
||||
" end\n"
|
||||
],
|
||||
[
|
||||
" cell $or ", "<CELL_ID>", "\n",
|
||||
" parameter \\A_SIGNED 0\n",
|
||||
" parameter \\B_SIGNED 0\n",
|
||||
" parameter \\A_WIDTH 0\n",
|
||||
" parameter \\B_WIDTH 0\n",
|
||||
" parameter \\Y_WIDTH 0\n",
|
||||
" connect \\A ", "<SIGSPEC>", "\n",
|
||||
" connect \\B ", "<SIGSPEC>", "\n",
|
||||
" connect \\Y ", "<SIGSPEC>", "\n",
|
||||
" end\n"
|
||||
],
|
||||
[
|
||||
" cell $xor ", "<CELL_ID>", "\n",
|
||||
" parameter \\A_SIGNED 0\n",
|
||||
" parameter \\B_SIGNED 0\n",
|
||||
" parameter \\A_WIDTH 0\n",
|
||||
" parameter \\B_WIDTH 0\n",
|
||||
" parameter \\Y_WIDTH 0\n",
|
||||
" connect \\A ", "<SIGSPEC>", "\n",
|
||||
" connect \\B ", "<SIGSPEC>", "\n",
|
||||
" connect \\Y ", "<SIGSPEC>", "\n",
|
||||
" end\n"
|
||||
],
|
||||
[
|
||||
" cell ", "<BLACKBOX_CELL>", " ", "<CELL_ID>", "\n",
|
||||
" connect \\A ", "<SIGSPEC>", "\n",
|
||||
" connect \\Y ", "<SIGSPEC>", "\n",
|
||||
" end\n"
|
||||
],
|
||||
[
|
||||
" cell ", "<BLACKBOX_CELL>", " ", "<CELL_ID>", "\n",
|
||||
" connect \\A ", "<SIGSPEC>", "\n",
|
||||
" connect \\B ", "<SIGSPEC>", "\n",
|
||||
" connect \\Y ", "<SIGSPEC>", "\n",
|
||||
" end\n"
|
||||
]
|
||||
],
|
||||
"<WIRE_ID>": [ [ "\\wire_a" ], [ "\\wire_b" ], [ "\\wire_c" ], [ "\\wire_d" ], [ "\\wire_e" ], [ "\\wire_f" ], [ "\\wire_g" ], [ "\\wire_h" ], [ "\\wire_i" ], [ "\\wire_j" ] ],
|
||||
"<CELL_ID>": [ [ "\\cell_a" ], [ "\\cell_b" ], [ "\\cell_c" ], [ "\\cell_d" ], [ "\\cell_e" ], [ "\\cell_f" ], [ "\\cell_g" ], [ "\\cell_h" ], [ "\\cell_i" ], [ "\\cell_j" ] ],
|
||||
"<BLACKBOX_CELL>": [ [ "\\bb1" ], [ "\\bb2" ] ],
|
||||
"<SIGSPEC>": [
|
||||
[ "<WIRE_ID>", " " ],
|
||||
[ "{", "<SIGSPEC>", " ", "<SIGSPECS>", "}" ],
|
||||
[ "<CONST>" ],
|
||||
[ "<SIGSPEC>", "[", "<BIT_OFFSET>", "]" ],
|
||||
[ "<SIGSPEC>", "[", "<BIT_OFFSET>", ":", "<BIT_OFFSET>", "]" ]
|
||||
],
|
||||
"<CONST>": [
|
||||
[ "0'", "<BITS>" ],
|
||||
[ "1'", "<BITS>" ],
|
||||
[ "2'", "<BITS>" ],
|
||||
[ "3'", "<BITS>" ],
|
||||
[ "4'", "<BITS>" ],
|
||||
[ "31'", "<BITS>" ],
|
||||
[ "32'", "<BITS>" ],
|
||||
[ "128'", "<BITS>" ]
|
||||
],
|
||||
"<BIT>": [ [ "0" ], [ "1" ], [ "x" ], [ "z" ], [ "-" ], [ "m" ] ],
|
||||
"<BIT_OFFSET>": [ "0", "1", "2", "3", "31", "32" ],
|
||||
"<PORT_ID>": [ "1", "2", "3", "4", "5", "6", "7", "8", "9", "10" ],
|
||||
"<CONNECT>": [ [ " connect ", "<SIGSPEC>", " ", "<SIGSPEC>", "\n" ] ],
|
||||
|
||||
"<WIRES>": [ [ ], [ "<WIRE>", "<WIRES>" ] ],
|
||||
"<CELLS>": [ [ ], [ "<CELL>", "<CELLS>" ] ],
|
||||
"<BITS>": [ [ ], [ "<BIT>", "<BITS>" ] ],
|
||||
"<CONNECTS>": [ [ ], [ "<CONNECT>", "<CONNECTS>" ] ],
|
||||
"<SIGSPECS>": [ [ ], [ "<SIGSPEC>", " ", "<SIGSPECS>" ] ]
|
||||
}
|
||||
|
|
@ -18,10 +18,11 @@ endif
|
|||
|
||||
EXTRAFLAGS := -lyosys -pthread
|
||||
|
||||
OBJTEST := objtest
|
||||
BINTEST := bintest
|
||||
MAKEFILE_DIR := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
|
||||
OBJTEST := $(MAKEFILE_DIR)objtest
|
||||
BINTEST := $(MAKEFILE_DIR)bintest
|
||||
|
||||
ALLTESTFILE := $(shell find . -name '*Test.cc' | sed 's|^\./||' | tr '\n' ' ')
|
||||
ALLTESTFILE := $(shell cd $(MAKEFILE_DIR) && find . -name '*Test.cc' | sed 's|^\./||' | tr '\n' ' ')
|
||||
TESTDIRS := $(sort $(dir $(ALLTESTFILE)))
|
||||
TESTS := $(addprefix $(BINTEST)/, $(basename $(ALLTESTFILE:%Test.cc=%Test.o)))
|
||||
|
||||
|
|
@ -34,7 +35,7 @@ $(BINTEST)/%: $(OBJTEST)/%.o | prepare
|
|||
$(CXX) -L$(ROOTPATH) $(RPATH) $(LINKFLAGS) -o $@ $^ $(LIBS) \
|
||||
$(GTEST_LDFLAGS) $(EXTRAFLAGS)
|
||||
|
||||
$(OBJTEST)/%.o: $(basename $(subst $(OBJTEST),.,%)).cc | prepare
|
||||
$(OBJTEST)/%.o: $(MAKEFILE_DIR)/%.cc | prepare
|
||||
$(CXX) -o $@ -c -I$(ROOTPATH) $(CPPFLAGS) $(CXXFLAGS) $(GTEST_CXXFLAGS) $^
|
||||
|
||||
.PHONY: prepare run-tests clean
|
||||
|
|
|
|||
87
tests/unit/kernel/cellTypesTest.cc
Normal file
87
tests/unit/kernel/cellTypesTest.cc
Normal file
|
|
@ -0,0 +1,87 @@
|
|||
#include <gtest/gtest.h>
|
||||
#include "kernel/yosys.h"
|
||||
#include "kernel/yosys_common.h"
|
||||
#include "kernel/celltypes.h"
|
||||
#include "kernel/newcelltypes.h"
|
||||
|
||||
#include <unordered_set>
|
||||
|
||||
YOSYS_NAMESPACE_BEGIN
|
||||
|
||||
TEST(CellTypesTest, basic)
|
||||
{
|
||||
yosys_setup();
|
||||
log_files.push_back(stdout);
|
||||
CellTypes older;
|
||||
NewCellTypes newer;
|
||||
older.setup(nullptr);
|
||||
newer.setup(nullptr);
|
||||
older.setup_type(ID(bleh), {ID::G}, {ID::H, ID::I}, false, true);
|
||||
newer.setup_type(ID(bleh), {ID::G}, {ID::H, ID::I}, false, true);
|
||||
EXPECT_EQ(older.cell_known(ID(aaaaa)), newer.cell_known(ID(aaaaa)));
|
||||
EXPECT_EQ(older.cell_known(ID($and)), newer.cell_known(ID($and)));
|
||||
auto check_port = [&](auto type, auto port) {
|
||||
EXPECT_EQ(older.cell_port_dir(type, port), newer.cell_port_dir(type, port));
|
||||
EXPECT_EQ(older.cell_input(type, port), newer.cell_input(type, port));
|
||||
EXPECT_EQ(older.cell_output(type, port), newer.cell_output(type, port));
|
||||
};
|
||||
|
||||
// ground truth
|
||||
const pool<IdString> expected_ff_types = {
|
||||
ID($sr), ID($ff), ID($dff), ID($dffe), ID($dffsr), ID($dffsre),
|
||||
ID($adff), ID($adffe), ID($aldff), ID($aldffe),
|
||||
ID($sdff), ID($sdffe), ID($sdffce),
|
||||
ID($dlatch), ID($adlatch), ID($dlatchsr),
|
||||
ID($_DFFE_NN_), ID($_DFFE_NP_), ID($_DFFE_PN_), ID($_DFFE_PP_),
|
||||
ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_),
|
||||
ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_),
|
||||
ID($_DFFSRE_NNNN_), ID($_DFFSRE_NNNP_), ID($_DFFSRE_NNPN_), ID($_DFFSRE_NNPP_),
|
||||
ID($_DFFSRE_NPNN_), ID($_DFFSRE_NPNP_), ID($_DFFSRE_NPPN_), ID($_DFFSRE_NPPP_),
|
||||
ID($_DFFSRE_PNNN_), ID($_DFFSRE_PNNP_), ID($_DFFSRE_PNPN_), ID($_DFFSRE_PNPP_),
|
||||
ID($_DFFSRE_PPNN_), ID($_DFFSRE_PPNP_), ID($_DFFSRE_PPPN_), ID($_DFFSRE_PPPP_),
|
||||
ID($_DFF_N_), ID($_DFF_P_),
|
||||
ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_),
|
||||
ID($_DFF_PN0_), ID($_DFF_PN1_), ID($_DFF_PP0_), ID($_DFF_PP1_),
|
||||
ID($_DFFE_NN0N_), ID($_DFFE_NN0P_), ID($_DFFE_NN1N_), ID($_DFFE_NN1P_),
|
||||
ID($_DFFE_NP0N_), ID($_DFFE_NP0P_), ID($_DFFE_NP1N_), ID($_DFFE_NP1P_),
|
||||
ID($_DFFE_PN0N_), ID($_DFFE_PN0P_), ID($_DFFE_PN1N_), ID($_DFFE_PN1P_),
|
||||
ID($_DFFE_PP0N_), ID($_DFFE_PP0P_), ID($_DFFE_PP1N_), ID($_DFFE_PP1P_),
|
||||
ID($_ALDFF_NN_), ID($_ALDFF_NP_), ID($_ALDFF_PN_), ID($_ALDFF_PP_),
|
||||
ID($_ALDFFE_NNN_), ID($_ALDFFE_NNP_), ID($_ALDFFE_NPN_), ID($_ALDFFE_NPP_),
|
||||
ID($_ALDFFE_PNN_), ID($_ALDFFE_PNP_), ID($_ALDFFE_PPN_), ID($_ALDFFE_PPP_),
|
||||
ID($_SDFF_NN0_), ID($_SDFF_NN1_), ID($_SDFF_NP0_), ID($_SDFF_NP1_),
|
||||
ID($_SDFF_PN0_), ID($_SDFF_PN1_), ID($_SDFF_PP0_), ID($_SDFF_PP1_),
|
||||
ID($_SDFFE_NN0N_), ID($_SDFFE_NN0P_), ID($_SDFFE_NN1N_), ID($_SDFFE_NN1P_),
|
||||
ID($_SDFFE_NP0N_), ID($_SDFFE_NP0P_), ID($_SDFFE_NP1N_), ID($_SDFFE_NP1P_),
|
||||
ID($_SDFFE_PN0N_), ID($_SDFFE_PN0P_), ID($_SDFFE_PN1N_), ID($_SDFFE_PN1P_),
|
||||
ID($_SDFFE_PP0N_), ID($_SDFFE_PP0P_), ID($_SDFFE_PP1N_), ID($_SDFFE_PP1P_),
|
||||
ID($_SDFFCE_NN0N_), ID($_SDFFCE_NN0P_), ID($_SDFFCE_NN1N_), ID($_SDFFCE_NN1P_),
|
||||
ID($_SDFFCE_NP0N_), ID($_SDFFCE_NP0P_), ID($_SDFFCE_NP1N_), ID($_SDFFCE_NP1P_),
|
||||
ID($_SDFFCE_PN0N_), ID($_SDFFCE_PN0P_), ID($_SDFFCE_PN1N_), ID($_SDFFCE_PN1P_),
|
||||
ID($_SDFFCE_PP0N_), ID($_SDFFCE_PP0P_), ID($_SDFFCE_PP1N_), ID($_SDFFCE_PP1P_),
|
||||
ID($_SR_NN_), ID($_SR_NP_), ID($_SR_PN_), ID($_SR_PP_),
|
||||
ID($_DLATCH_N_), ID($_DLATCH_P_),
|
||||
ID($_DLATCH_NN0_), ID($_DLATCH_NN1_), ID($_DLATCH_NP0_), ID($_DLATCH_NP1_),
|
||||
ID($_DLATCH_PN0_), ID($_DLATCH_PN1_), ID($_DLATCH_PP0_), ID($_DLATCH_PP1_),
|
||||
ID($_DLATCHSR_NNN_), ID($_DLATCHSR_NNP_), ID($_DLATCHSR_NPN_), ID($_DLATCHSR_NPP_),
|
||||
ID($_DLATCHSR_PNN_), ID($_DLATCHSR_PNP_), ID($_DLATCHSR_PPN_), ID($_DLATCHSR_PPP_),
|
||||
ID($_FF_),
|
||||
};
|
||||
|
||||
for (size_t i = 0; i < static_cast<size_t>(RTLIL::StaticId::STATIC_ID_END); i++) {
|
||||
IdString type;
|
||||
type.index_ = i;
|
||||
EXPECT_EQ(older.cell_known(type), newer.cell_known(type));
|
||||
if (older.cell_evaluable(type) != newer.cell_evaluable(type))
|
||||
std::cout << type.str() << "\n";
|
||||
EXPECT_EQ(older.cell_evaluable(type), newer.cell_evaluable(type));
|
||||
for (auto port : StaticCellTypes::builder.cells.data()->inputs.ports)
|
||||
check_port(type, port);
|
||||
for (auto port : StaticCellTypes::builder.cells.data()->outputs.ports)
|
||||
check_port(type, port);
|
||||
EXPECT_EQ(expected_ff_types.count(type) > 0, StaticCellTypes::categories.is_ff(type));
|
||||
}
|
||||
yosys_shutdown();
|
||||
}
|
||||
|
||||
YOSYS_NAMESPACE_END
|
||||
47
tests/unit/kernel/modindexTest.cc
Normal file
47
tests/unit/kernel/modindexTest.cc
Normal file
|
|
@ -0,0 +1,47 @@
|
|||
#include <gtest/gtest.h>
|
||||
|
||||
#include "kernel/modtools.h"
|
||||
#include "kernel/rtlil.h"
|
||||
|
||||
YOSYS_NAMESPACE_BEGIN
|
||||
|
||||
TEST(ModIndexSwapTest, has)
|
||||
{
|
||||
Design* d = new Design;
|
||||
Module* m = d->addModule("$m");
|
||||
Wire* o = m->addWire("$o", 2);
|
||||
o->port_input = true;
|
||||
Wire* i = m->addWire("$i", 2);
|
||||
i->port_input = true;
|
||||
m->fixup_ports();
|
||||
m->addNot("$not", i, o);
|
||||
auto mi = ModIndex(m);
|
||||
mi.reload_module();
|
||||
for (auto [sb, info] : mi.database) {
|
||||
EXPECT_TRUE(mi.database.find(sb) != mi.database.end());
|
||||
}
|
||||
m->swap_names(i, o);
|
||||
for (auto [sb, info] : mi.database) {
|
||||
EXPECT_TRUE(mi.database.find(sb) != mi.database.end());
|
||||
}
|
||||
}
|
||||
|
||||
TEST(ModIndexDeleteTest, has)
|
||||
{
|
||||
if (log_files.empty()) log_files.emplace_back(stdout);
|
||||
Design* d = new Design;
|
||||
Module* m = d->addModule("$m");
|
||||
Wire* w = m->addWire("$w");
|
||||
Wire* o = m->addWire("$o");
|
||||
o->port_output = true;
|
||||
m->fixup_ports();
|
||||
Cell* not_ = m->addNotGate("$not", w, o);
|
||||
auto mi = ModIndex(m);
|
||||
mi.reload_module();
|
||||
mi.dump_db();
|
||||
Wire* a = m->addWire("\\a");
|
||||
not_->setPort(ID::A, a);
|
||||
EXPECT_TRUE(mi.ok());
|
||||
}
|
||||
|
||||
YOSYS_NAMESPACE_END
|
||||
61
tests/unit/kernel/rtlilStringTest.cc
Normal file
61
tests/unit/kernel/rtlilStringTest.cc
Normal file
|
|
@ -0,0 +1,61 @@
|
|||
#include <gtest/gtest.h>
|
||||
|
||||
#include "kernel/rtlil.h"
|
||||
#include "kernel/yosys.h"
|
||||
|
||||
YOSYS_NAMESPACE_BEGIN
|
||||
|
||||
namespace RTLIL {
|
||||
|
||||
TEST(RtlilStrTest, DesignToString) {
|
||||
Design design;
|
||||
Module *mod = design.addModule(ID(my_module));
|
||||
mod->addWire(ID(my_wire), 1);
|
||||
|
||||
std::string design_str = design.to_rtlil_str();
|
||||
|
||||
EXPECT_NE(design_str.find("module \\my_module"), std::string::npos);
|
||||
EXPECT_NE(design_str.find("end"), std::string::npos);
|
||||
}
|
||||
|
||||
TEST(RtlilStrTest, ModuleToString) {
|
||||
Design design;
|
||||
Module *mod = design.addModule(ID(test_mod));
|
||||
Wire *wire = mod->addWire(ID(clk), 1);
|
||||
wire->port_input = true;
|
||||
|
||||
std::string mod_str = mod->to_rtlil_str();
|
||||
|
||||
EXPECT_NE(mod_str.find("module \\test_mod"), std::string::npos);
|
||||
EXPECT_NE(mod_str.find("wire"), std::string::npos);
|
||||
EXPECT_NE(mod_str.find("\\clk"), std::string::npos);
|
||||
EXPECT_NE(mod_str.find("input"), std::string::npos);
|
||||
}
|
||||
|
||||
TEST(RtlilStrTest, WireToString) {
|
||||
Design design;
|
||||
Module *mod = design.addModule(ID(m));
|
||||
Wire *wire = mod->addWire(ID(data), 8);
|
||||
|
||||
std::string wire_str = wire->to_rtlil_str();
|
||||
|
||||
EXPECT_NE(wire_str.find("wire"), std::string::npos);
|
||||
EXPECT_NE(wire_str.find("width 8"), std::string::npos);
|
||||
EXPECT_NE(wire_str.find("\\data"), std::string::npos);
|
||||
}
|
||||
|
||||
TEST(RtlilStrTest, CellToString) {
|
||||
Design design;
|
||||
Module *mod = design.addModule(ID(m));
|
||||
Cell *cell = mod->addCell(ID(u1), ID(my_cell_type));
|
||||
|
||||
std::string cell_str = cell->to_rtlil_str();
|
||||
|
||||
EXPECT_NE(cell_str.find("cell"), std::string::npos);
|
||||
EXPECT_NE(cell_str.find("\\my_cell_type"), std::string::npos);
|
||||
EXPECT_NE(cell_str.find("\\u1"), std::string::npos);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
YOSYS_NAMESPACE_END
|
||||
179
tests/unit/opt/optDffFindComplementaryPatternTest.cc
Normal file
179
tests/unit/opt/optDffFindComplementaryPatternTest.cc
Normal file
|
|
@ -0,0 +1,179 @@
|
|||
#include <gtest/gtest.h>
|
||||
#include "kernel/pattern.h"
|
||||
|
||||
YOSYS_NAMESPACE_BEGIN
|
||||
|
||||
class FindComplementaryPatternVarTest : public ::testing::Test {
|
||||
protected:
|
||||
RTLIL::Design *design;
|
||||
RTLIL::Module *module;
|
||||
RTLIL::Wire *wire_a;
|
||||
RTLIL::Wire *wire_b;
|
||||
RTLIL::Wire *wire_c;
|
||||
RTLIL::Wire *bus;
|
||||
|
||||
void SetUp() override {
|
||||
design = new RTLIL::Design;
|
||||
module = design->addModule(ID(test_module));
|
||||
wire_a = module->addWire(ID(a));
|
||||
wire_b = module->addWire(ID(b));
|
||||
wire_c = module->addWire(ID(c));
|
||||
bus = module->addWire(ID(bus), 4);
|
||||
}
|
||||
|
||||
void TearDown() override {
|
||||
delete design;
|
||||
}
|
||||
|
||||
RTLIL::SigBit bit(RTLIL::Wire *w, int offset = 0) {
|
||||
return RTLIL::SigBit(w, offset);
|
||||
}
|
||||
};
|
||||
|
||||
TEST_F(FindComplementaryPatternVarTest, EmptyPatterns) {
|
||||
pattern_t left, right;
|
||||
|
||||
auto result = find_complementary_pattern_var(left, right);
|
||||
EXPECT_FALSE(result.has_value());
|
||||
}
|
||||
|
||||
TEST_F(FindComplementaryPatternVarTest, IdenticalSingleVar) {
|
||||
pattern_t left, right;
|
||||
left[bit(wire_a)] = true;
|
||||
right[bit(wire_a)] = true;
|
||||
|
||||
auto result = find_complementary_pattern_var(left, right);
|
||||
EXPECT_FALSE(result.has_value());
|
||||
}
|
||||
|
||||
TEST_F(FindComplementaryPatternVarTest, ComplementarySingleVar) {
|
||||
pattern_t left, right;
|
||||
left[bit(wire_a)] = true;
|
||||
right[bit(wire_a)] = false;
|
||||
|
||||
auto result = find_complementary_pattern_var(left, right);
|
||||
ASSERT_TRUE(result.has_value());
|
||||
EXPECT_EQ(result.value(), bit(wire_a));
|
||||
}
|
||||
|
||||
TEST_F(FindComplementaryPatternVarTest, MissingKeyInRight) {
|
||||
pattern_t left, right;
|
||||
left[bit(wire_a)] = true;
|
||||
left[bit(wire_b)] = false;
|
||||
right[bit(wire_a)] = true;
|
||||
|
||||
auto result = find_complementary_pattern_var(left, right);
|
||||
EXPECT_FALSE(result.has_value());
|
||||
}
|
||||
|
||||
TEST_F(FindComplementaryPatternVarTest, TwoVarsOneComplementary) {
|
||||
pattern_t left, right;
|
||||
left[bit(wire_a)] = true;
|
||||
left[bit(wire_b)] = false;
|
||||
right[bit(wire_a)] = true;
|
||||
right[bit(wire_b)] = true;
|
||||
|
||||
auto result = find_complementary_pattern_var(left, right);
|
||||
ASSERT_TRUE(result.has_value());
|
||||
EXPECT_EQ(result.value(), bit(wire_b));
|
||||
}
|
||||
|
||||
TEST_F(FindComplementaryPatternVarTest, TwoVarsBothComplementary) {
|
||||
pattern_t left, right;
|
||||
left[bit(wire_a)] = true;
|
||||
left[bit(wire_b)] = false;
|
||||
right[bit(wire_a)] = false;
|
||||
right[bit(wire_b)] = true;
|
||||
|
||||
auto result = find_complementary_pattern_var(left, right);
|
||||
EXPECT_FALSE(result.has_value());
|
||||
}
|
||||
|
||||
TEST_F(FindComplementaryPatternVarTest, LeftSubsetOfRight) {
|
||||
pattern_t left, right;
|
||||
left[bit(wire_a)] = true;
|
||||
left[bit(wire_b)] = false;
|
||||
right[bit(wire_a)] = true;
|
||||
right[bit(wire_b)] = true;
|
||||
right[bit(wire_c)] = false;
|
||||
|
||||
auto result = find_complementary_pattern_var(left, right);
|
||||
ASSERT_TRUE(result.has_value());
|
||||
EXPECT_EQ(result.value(), bit(wire_b));
|
||||
}
|
||||
|
||||
TEST_F(FindComplementaryPatternVarTest, ThreeVarsAllSame) {
|
||||
pattern_t left, right;
|
||||
left[bit(wire_a)] = true;
|
||||
left[bit(wire_b)] = false;
|
||||
left[bit(wire_c)] = true;
|
||||
right[bit(wire_a)] = true;
|
||||
right[bit(wire_b)] = false;
|
||||
right[bit(wire_c)] = true;
|
||||
|
||||
auto result = find_complementary_pattern_var(left, right);
|
||||
EXPECT_FALSE(result.has_value());
|
||||
}
|
||||
|
||||
TEST_F(FindComplementaryPatternVarTest, PracticalPatternSimplification) {
|
||||
pattern_t pattern1, pattern2;
|
||||
pattern1[bit(bus, 0)] = true;
|
||||
pattern1[bit(bus, 1)] = true;
|
||||
pattern2[bit(bus, 0)] = true;
|
||||
pattern2[bit(bus, 1)] = false;
|
||||
|
||||
auto result = find_complementary_pattern_var(pattern1, pattern2);
|
||||
ASSERT_TRUE(result.has_value());
|
||||
EXPECT_EQ(result.value(), bit(bus, 1));
|
||||
|
||||
// Swapped args
|
||||
auto result2 = find_complementary_pattern_var(pattern2, pattern1);
|
||||
ASSERT_TRUE(result2.has_value());
|
||||
EXPECT_EQ(result2.value(), bit(bus, 1));
|
||||
}
|
||||
|
||||
TEST_F(FindComplementaryPatternVarTest, MuxTreeClockEnableDetection) {
|
||||
pattern_t feedback_path1, feedback_path2;
|
||||
feedback_path1[bit(wire_a)] = true;
|
||||
feedback_path1[bit(wire_b)] = true;
|
||||
feedback_path2[bit(wire_a)] = true;
|
||||
feedback_path2[bit(wire_b)] = false;
|
||||
|
||||
auto comp = find_complementary_pattern_var(feedback_path1, feedback_path2);
|
||||
ASSERT_TRUE(comp.has_value());
|
||||
EXPECT_EQ(comp.value(), bit(wire_b));
|
||||
|
||||
pattern_t simplified = feedback_path1;
|
||||
simplified.erase(comp.value());
|
||||
|
||||
EXPECT_EQ(simplified.size(), 1);
|
||||
EXPECT_TRUE(simplified.count(bit(wire_a)));
|
||||
EXPECT_TRUE(simplified[bit(wire_a)]);
|
||||
}
|
||||
|
||||
TEST_F(FindComplementaryPatternVarTest, AsymmetricPatterns) {
|
||||
pattern_t left, right;
|
||||
left[bit(wire_a)] = true;
|
||||
right[bit(wire_a)] = false;
|
||||
right[bit(wire_b)] = true;
|
||||
right[bit(wire_c)] = false;
|
||||
|
||||
auto result = find_complementary_pattern_var(left, right);
|
||||
ASSERT_TRUE(result.has_value());
|
||||
EXPECT_EQ(result.value(), bit(wire_a));
|
||||
}
|
||||
|
||||
TEST_F(FindComplementaryPatternVarTest, WireOffsetDistinction) {
|
||||
pattern_t left, right;
|
||||
left[bit(bus, 0)] = true;
|
||||
left[bit(bus, 1)] = false;
|
||||
right[bit(bus, 0)] = true;
|
||||
right[bit(bus, 1)] = true;
|
||||
right[bit(bus, 2)] = false;
|
||||
|
||||
auto result = find_complementary_pattern_var(left, right);
|
||||
ASSERT_TRUE(result.has_value());
|
||||
EXPECT_EQ(result.value(), bit(bus, 1));
|
||||
}
|
||||
|
||||
YOSYS_NAMESPACE_END
|
||||
2
tests/various/.gitignore
vendored
2
tests/various/.gitignore
vendored
|
|
@ -4,6 +4,8 @@
|
|||
/plugin.so
|
||||
/plugin_search
|
||||
/plugin.so.dSYM
|
||||
/ezcmdline_plugin.so
|
||||
/ezcmdline_plugin.so.dSYM
|
||||
/temp
|
||||
/smtlib2_module.smt2
|
||||
/smtlib2_module-filtered.smt2
|
||||
|
|
|
|||
49
tests/various/const_shift_empty_arg.ys
Normal file
49
tests/various/const_shift_empty_arg.ys
Normal file
|
|
@ -0,0 +1,49 @@
|
|||
# Regression test for #5684: const_shift_worker must not crash when arg1 is
|
||||
# empty.
|
||||
|
||||
read_json << EOF
|
||||
{
|
||||
"modules": {
|
||||
"sshl": {
|
||||
"cells": {
|
||||
"sshlCell": {
|
||||
"connections": {
|
||||
"A": [],
|
||||
"B": [3],
|
||||
"Y": [1]
|
||||
},
|
||||
"parameters": {
|
||||
"A_SIGNED": "1",
|
||||
"A_WIDTH": "0",
|
||||
"B_SIGNED": "0",
|
||||
"B_WIDTH": "1",
|
||||
"Y_WIDTH": "1"
|
||||
},
|
||||
"port_directions": {
|
||||
"A": "input",
|
||||
"B": "input",
|
||||
"Y": "output"
|
||||
},
|
||||
"type": "$sshl"
|
||||
}
|
||||
},
|
||||
"ports": {
|
||||
"A": {
|
||||
"bits": [],
|
||||
"direction": "input"
|
||||
},
|
||||
"B": {
|
||||
"bits": [3],
|
||||
"direction": "input"
|
||||
},
|
||||
"Y": {
|
||||
"bits": [1],
|
||||
"direction": "output"
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
EOF
|
||||
|
||||
eval -set B 0 -show Y sshl
|
||||
14
tests/various/debugon.ys
Normal file
14
tests/various/debugon.ys
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
# Test debug -on/-off modes
|
||||
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module top(input a, input b, output y);
|
||||
assign y = a & b;
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
debug -on
|
||||
hierarchy
|
||||
select -assert-count 1 t:$and
|
||||
debug -off
|
||||
22
tests/various/design_equal_fail.ys
Normal file
22
tests/various/design_equal_fail.ys
Normal file
|
|
@ -0,0 +1,22 @@
|
|||
logger -expect error "Second design missing module top_renamed" 1
|
||||
|
||||
read_rtlil <<EOT
|
||||
module \top
|
||||
wire width 1 input 1 \a
|
||||
wire width 1 output 2 \y
|
||||
connect \y \a
|
||||
end
|
||||
EOT
|
||||
|
||||
design -save golden
|
||||
|
||||
design -reset
|
||||
read_rtlil <<EOT
|
||||
module \top_renamed
|
||||
wire width 1 input 1 \a
|
||||
wire width 1 output 2 \y
|
||||
connect \y \a
|
||||
end
|
||||
EOT
|
||||
|
||||
design_equal golden
|
||||
17
tests/various/design_equal_pass.ys
Normal file
17
tests/various/design_equal_pass.ys
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
read_rtlil <<EOT
|
||||
module \top
|
||||
wire width 1 input 1 \a
|
||||
wire width 1 output 2 \y
|
||||
connect \y \a
|
||||
end
|
||||
EOT
|
||||
|
||||
design -save golden
|
||||
design_equal golden
|
||||
|
||||
design -save copy
|
||||
design_equal copy
|
||||
|
||||
design -load golden
|
||||
design_equal golden
|
||||
design_equal copy
|
||||
61
tests/various/ezcmdline_dummy_solver
Executable file
61
tests/various/ezcmdline_dummy_solver
Executable file
|
|
@ -0,0 +1,61 @@
|
|||
#!/bin/sh
|
||||
# Dummy SAT solver for ezCmdlineSAT tests.
|
||||
# Accepts exactly two CNF shapes:
|
||||
# - SAT: p cnf 1 1; clause: "1 0" -> exits 10 with v 1
|
||||
# - UNSAT: p cnf 1 2; clauses: "1 0" and "-1 0" -> exits 20
|
||||
set -e
|
||||
|
||||
if [ "$#" -ne 1 ]; then
|
||||
echo "usage: $0 <cnf>" >&2
|
||||
exit 1
|
||||
fi
|
||||
|
||||
awk '
|
||||
BEGIN {
|
||||
vars = 0;
|
||||
clauses = 0;
|
||||
clause_count = 0;
|
||||
clause_data = "";
|
||||
current = "";
|
||||
}
|
||||
$1 == "c" {
|
||||
next;
|
||||
}
|
||||
$1 == "p" && $2 == "cnf" {
|
||||
vars = $3;
|
||||
clauses = $4;
|
||||
next;
|
||||
}
|
||||
{
|
||||
for (i = 1; i <= NF; i++) {
|
||||
lit = $i;
|
||||
if (lit == 0) {
|
||||
clause_count++;
|
||||
if (clause_data != "")
|
||||
clause_data = clause_data ";" current;
|
||||
else
|
||||
clause_data = current;
|
||||
current = "";
|
||||
} else {
|
||||
if (current == "")
|
||||
current = lit;
|
||||
else
|
||||
current = current "," lit;
|
||||
}
|
||||
}
|
||||
}
|
||||
END {
|
||||
if (vars == 1 && clause_count == 1 && clause_data == "1") {
|
||||
print "s SATISFIABLE";
|
||||
print "v 1 0";
|
||||
exit 10;
|
||||
}
|
||||
if (vars == 1 && clause_count == 2 && clause_data == "1;-1") {
|
||||
print "s UNSATISFIABLE";
|
||||
exit 20;
|
||||
}
|
||||
print "c unexpected CNF for dummy solver";
|
||||
print "c vars=" vars " header_clauses=" clauses " parsed_clauses=" clause_count " data=" clause_data;
|
||||
exit 1;
|
||||
}
|
||||
' "$1"
|
||||
53
tests/various/ezcmdline_plugin.cc
Normal file
53
tests/various/ezcmdline_plugin.cc
Normal file
|
|
@ -0,0 +1,53 @@
|
|||
#include "kernel/yosys.h"
|
||||
#include "libs/ezsat/ezcmdline.h"
|
||||
|
||||
USING_YOSYS_NAMESPACE
|
||||
PRIVATE_NAMESPACE_BEGIN
|
||||
|
||||
struct EzCmdlineTestPass : public Pass {
|
||||
EzCmdlineTestPass() : Pass("ezcmdline_test", "smoke-test ezCmdlineSAT") { }
|
||||
void execute(std::vector<std::string> args, RTLIL::Design *design) override
|
||||
{
|
||||
std::string cmd;
|
||||
size_t argidx = 1;
|
||||
|
||||
while (argidx < args.size()) {
|
||||
if (args[argidx] == "-cmd" && argidx + 1 < args.size()) {
|
||||
cmd = args[argidx + 1];
|
||||
argidx += 2;
|
||||
continue;
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
||||
extra_args(args, argidx, design);
|
||||
|
||||
if (cmd.empty())
|
||||
log_error("Missing -cmd <solver> argument.\n");
|
||||
|
||||
ezCmdlineSAT sat(cmd);
|
||||
sat.non_incremental();
|
||||
|
||||
// assume("A") adds a permanent CNF clause "A".
|
||||
sat.assume(sat.VAR("A"));
|
||||
|
||||
std::vector<int> model_expressions;
|
||||
std::vector<bool> model_values;
|
||||
model_expressions.push_back(sat.VAR("A"));
|
||||
|
||||
// Expect SAT with A=true.
|
||||
if (!sat.solve(model_expressions, model_values))
|
||||
log_error("ezCmdlineSAT SAT case failed.\n");
|
||||
if (model_values.size() != 1 || !model_values[0])
|
||||
log_error("ezCmdlineSAT SAT model mismatch.\n");
|
||||
|
||||
// Passing NOT("A") here adds a temporary unit clause for this solve call,
|
||||
// so the solver sees A && !A and must return UNSAT.
|
||||
if (sat.solve(model_expressions, model_values, sat.NOT("A")))
|
||||
log_error("ezCmdlineSAT UNSAT case failed.\n");
|
||||
|
||||
log("ezcmdline_test passed!\n");
|
||||
}
|
||||
} EzCmdlineTestPass;
|
||||
|
||||
PRIVATE_NAMESPACE_END
|
||||
12
tests/various/ezcmdline_plugin.sh
Normal file
12
tests/various/ezcmdline_plugin.sh
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
set -e
|
||||
|
||||
DIR=$(cd "$(dirname "$0")" && pwd)
|
||||
BASEDIR=$(cd "$DIR/../.." && pwd)
|
||||
rm -f "$DIR/ezcmdline_plugin.so"
|
||||
chmod +x "$DIR/ezcmdline_dummy_solver"
|
||||
CXXFLAGS=$("$BASEDIR/yosys-config" --cxxflags)
|
||||
DATDIR=$("$BASEDIR/yosys-config" --datdir)
|
||||
DATDIR=${DATDIR//\//\\\/}
|
||||
CXXFLAGS=${CXXFLAGS//$DATDIR/..\/..\/share}
|
||||
"$BASEDIR/yosys-config" --exec --cxx ${CXXFLAGS} -I"$BASEDIR" --ldflags -shared -o "$DIR/ezcmdline_plugin.so" "$DIR/ezcmdline_plugin.cc"
|
||||
"$BASEDIR/yosys" -m "$DIR/ezcmdline_plugin.so" -p "ezcmdline_test -cmd $DIR/ezcmdline_dummy_solver" | grep -q "ezcmdline_test passed!"
|
||||
10
tests/various/json_param_defaults.v
Normal file
10
tests/various/json_param_defaults.v
Normal file
|
|
@ -0,0 +1,10 @@
|
|||
module json_param_defaults #(
|
||||
parameter WIDTH = 8,
|
||||
parameter SIGNED = 1
|
||||
) (
|
||||
input [WIDTH-1:0] a,
|
||||
output [WIDTH-1:0] y
|
||||
);
|
||||
wire [WIDTH-1:0] y_int = a << SIGNED;
|
||||
assign y = y_int;
|
||||
endmodule
|
||||
8
tests/various/json_param_defaults.ys
Normal file
8
tests/various/json_param_defaults.ys
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
! mkdir -p temp
|
||||
read_verilog -sv json_param_defaults.v
|
||||
write_json temp/json_param_defaults.json
|
||||
design -reset
|
||||
read_json temp/json_param_defaults.json
|
||||
write_verilog -noattr -defaultparams temp/json_param_defaults.v
|
||||
! grep -qF "parameter WIDTH = 32'd8" temp/json_param_defaults.v
|
||||
! grep -qF "parameter SIGNED = 32'd1" temp/json_param_defaults.v
|
||||
|
|
@ -43,7 +43,7 @@ select n:C_* -assert-count 2
|
|||
equiv_make gold gate equiv
|
||||
hierarchy -top equiv
|
||||
equiv_struct
|
||||
equiv_induct -seq 5
|
||||
equiv_induct -ignore-unknown-cells -seq 5
|
||||
equiv_status -assert
|
||||
design -reset
|
||||
|
||||
|
|
@ -57,7 +57,7 @@ select n:B_* -assert-count 2
|
|||
equiv_make gold gate equiv
|
||||
hierarchy -top equiv
|
||||
equiv_struct
|
||||
equiv_induct -seq 5
|
||||
equiv_induct -ignore-unknown-cells -seq 5
|
||||
equiv_status -assert
|
||||
design -reset
|
||||
|
||||
|
|
|
|||
2
tests/verific/mixed_flist.flist
Normal file
2
tests/verific/mixed_flist.flist
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
mixed_flist.sv
|
||||
mixed_flist.vhd
|
||||
4
tests/verific/mixed_flist.sv
Normal file
4
tests/verific/mixed_flist.sv
Normal file
|
|
@ -0,0 +1,4 @@
|
|||
module sv_top(input logic a, output logic y);
|
||||
// Instantiates VHDL entity to ensure mixed -f list is required
|
||||
vhdl_mod u_vhdl(.a(a), .y(y));
|
||||
endmodule
|
||||
14
tests/verific/mixed_flist.vhd
Normal file
14
tests/verific/mixed_flist.vhd
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
library ieee;
|
||||
use ieee.std_logic_1164.all;
|
||||
|
||||
entity vhdl_mod is
|
||||
port (
|
||||
a : in std_logic;
|
||||
y : out std_logic
|
||||
);
|
||||
end entity vhdl_mod;
|
||||
|
||||
architecture rtl of vhdl_mod is
|
||||
begin
|
||||
y <= a;
|
||||
end architecture rtl;
|
||||
3
tests/verific/mixed_flist.ys
Normal file
3
tests/verific/mixed_flist.ys
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
verific -f -sv mixed_flist.flist
|
||||
verific -import sv_top
|
||||
select -assert-mod-count 1 sv_top
|
||||
1
tests/verilog/.gitignore
vendored
1
tests/verilog/.gitignore
vendored
|
|
@ -1,3 +1,4 @@
|
|||
/bug5572.v
|
||||
/const_arst.v
|
||||
/const_sr.v
|
||||
/doubleslash.v
|
||||
|
|
|
|||
104
tests/verilog/automatic_lifetime.ys
Normal file
104
tests/verilog/automatic_lifetime.ys
Normal file
|
|
@ -0,0 +1,104 @@
|
|||
# Automatic reg as intermediate value in always @(*)
|
||||
# The result must be provably equivalent to the direct expression.
|
||||
# No latch or DFF must be created for tmp.
|
||||
design -reset
|
||||
read_verilog -sv <<EOF
|
||||
module t1(input a, b, c, output reg y);
|
||||
always @(*) begin : blk
|
||||
automatic reg tmp;
|
||||
tmp = a ^ b;
|
||||
if (c) tmp = tmp & a;
|
||||
y = tmp;
|
||||
end
|
||||
// equivalent to: y = c ? ((a^b)&a) : (a^b)
|
||||
assert property (y === (c ? ((a ^ b) & a) : (a ^ b)));
|
||||
endmodule
|
||||
EOF
|
||||
proc
|
||||
async2sync
|
||||
# no state elements for tmp
|
||||
select -assert-none t:$dff t:$dlatch %%
|
||||
sat -verify -prove-asserts -show-all
|
||||
|
||||
# automatic logic in always_comb with chained computation
|
||||
# Two automatic intermediates used in sequence; result must match
|
||||
# the direct expression. No latch/DFF.
|
||||
design -reset
|
||||
read_verilog -sv <<EOF
|
||||
module t2(input [3:0] a, b, input sel, output reg [3:0] y, output reg co);
|
||||
always_comb begin : blk
|
||||
automatic reg [4:0] sum;
|
||||
automatic reg [3:0] pick;
|
||||
sum = {1'b0, a} + {1'b0, b};
|
||||
pick = sel ? sum[3:0] : (a & b);
|
||||
y = pick;
|
||||
co = sum[4];
|
||||
end
|
||||
assert property (y === (sel ? ((a + b) & 4'hf) : (a & b)));
|
||||
assert property (co === (((5'(a) + 5'(b)) >> 4) & 1'b1));
|
||||
endmodule
|
||||
EOF
|
||||
proc
|
||||
async2sync
|
||||
select -assert-none t:$dff t:$dlatch %%
|
||||
sat -verify -prove-asserts -show-all
|
||||
|
||||
# automatic in a clocked block — only the explicitly registered
|
||||
# output (result) must get a DFF; the automatic temp must not.
|
||||
design -reset
|
||||
read_verilog -sv <<EOF
|
||||
module t3(input clk, rst, input [7:0] data, output reg [7:0] result);
|
||||
always @(posedge clk) begin : compute
|
||||
automatic reg [7:0] tmp;
|
||||
tmp = data ^ 8'hA5;
|
||||
if (rst)
|
||||
result <= 8'h00;
|
||||
else
|
||||
result <= tmp;
|
||||
end
|
||||
endmodule
|
||||
EOF
|
||||
proc
|
||||
# Exactly one DFF (for result), zero latches, no DFF for tmp
|
||||
select -assert-count 1 t:$dff %%
|
||||
select -assert-none t:$dlatch %%
|
||||
|
||||
# automatic integer in named block — ensure integer-width
|
||||
# automatic variables work and produce no state elements.
|
||||
design -reset
|
||||
read_verilog -sv <<EOF
|
||||
module t4(input [7:0] a, b, input sub, output reg [7:0] y);
|
||||
always @(*) begin : arith
|
||||
automatic integer acc;
|
||||
if (sub)
|
||||
acc = $signed(a) - $signed(b);
|
||||
else
|
||||
acc = $signed(a) + $signed(b);
|
||||
y = acc[7:0];
|
||||
end
|
||||
assert property (y === (sub ? (a - b) : (a + b)));
|
||||
endmodule
|
||||
EOF
|
||||
proc
|
||||
async2sync
|
||||
select -assert-none t:$dff t:$dlatch %%
|
||||
sat -verify -prove-asserts -show-all
|
||||
|
||||
# automatic variable not assigned on all paths (X semantics)
|
||||
# With 'automatic', tmp holds no previous state; the undriven path
|
||||
# produces X, not the old register value. After proc, no latch may be
|
||||
# inferred for tmp.
|
||||
design -reset
|
||||
read_verilog -sv <<EOF
|
||||
module t5(input en, d, output reg q);
|
||||
always @(*) begin : blk
|
||||
automatic reg tmp;
|
||||
if (en) tmp = d;
|
||||
// tmp is X when en==0: automatic means no state retention
|
||||
q = tmp;
|
||||
end
|
||||
endmodule
|
||||
EOF
|
||||
proc
|
||||
# No latch for tmp — X propagates instead of old value
|
||||
select -assert-none t:$dff t:$dlatch %%
|
||||
15
tests/verilog/bug5572.ys
Normal file
15
tests/verilog/bug5572.ys
Normal file
|
|
@ -0,0 +1,15 @@
|
|||
read_rtlil << EOT
|
||||
module \top
|
||||
wire \sig
|
||||
wire \val
|
||||
process $2
|
||||
attribute \full_case 1
|
||||
switch \sig
|
||||
end
|
||||
end
|
||||
end
|
||||
EOT
|
||||
|
||||
write_verilog bug5572.v
|
||||
design -reset
|
||||
read_verilog bug5572.v
|
||||
20
tests/verilog/genblk_wire.sv
Normal file
20
tests/verilog/genblk_wire.sv
Normal file
|
|
@ -0,0 +1,20 @@
|
|||
module gold(a, b);
|
||||
output wire [1:0] a;
|
||||
input wire [1:0] b;
|
||||
genvar i;
|
||||
for (i = 0; i < 2; i++) begin
|
||||
wire x;
|
||||
assign x = b[i];
|
||||
assign a[i] = x;
|
||||
end
|
||||
endmodule
|
||||
|
||||
module gate(a, b);
|
||||
output wire [1:0] a;
|
||||
input wire [1:0] b;
|
||||
genvar i;
|
||||
for (i = 0; i < 2; i++) begin
|
||||
assign x = b[i];
|
||||
assign a[i] = x;
|
||||
end
|
||||
endmodule
|
||||
17
tests/verilog/genblk_wire.ys
Normal file
17
tests/verilog/genblk_wire.ys
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
logger -expect warning "Identifier `\\genblk1[[]0[]]\.x' is implicitly declared." 1
|
||||
logger -expect warning "Identifier `\\genblk1[[]1[]]\.x' is implicitly declared." 1
|
||||
read_verilog -sv genblk_wire.sv
|
||||
logger -check-expected
|
||||
|
||||
select -assert-count 1 gate/genblk1[0].x
|
||||
select -assert-count 1 gate/genblk1[1].x
|
||||
select -assert-count 0 gate/genblk1[2].x
|
||||
|
||||
select -assert-count 1 gold/genblk1[0].x
|
||||
select -assert-count 1 gold/genblk1[1].x
|
||||
select -assert-count 0 gold/genblk1[2].x
|
||||
|
||||
proc
|
||||
equiv_make gold gate equiv
|
||||
equiv_simple
|
||||
equiv_status -assert
|
||||
Loading…
Add table
Add a link
Reference in a new issue