mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-23 00:55:32 +00:00
Merge branch 'master' into eddie/submod_po
This commit is contained in:
Eddie Hung
commit
136842b1ef
219 changed files with 12089 additions and 6025 deletions
|
|
@ -33,7 +33,7 @@ design -import gold -as gold
|
|||
design -import gate -as gate
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -show-ports -seq 16 miter
|
||||
"
|
||||
" -l ${aag}.log
|
||||
done
|
||||
|
||||
for aig in *.aig; do
|
||||
|
|
@ -50,5 +50,5 @@ design -import gold -as gold
|
|||
design -import gate -as gate
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -show-ports -seq 16 miter
|
||||
"
|
||||
" -l ${aig}.log
|
||||
done
|
||||
|
|
|
|||
9
tests/aiger/symbols.aag
Normal file
9
tests/aiger/symbols.aag
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
aag 2 1 1 1 0
|
||||
2
|
||||
4 2 1
|
||||
4
|
||||
i0 d
|
||||
l0 q
|
||||
o0 q
|
||||
c
|
||||
Generated by Yosys 0.9+932 (git sha1 baba33fb, clang 9.0.0-2 -fPIC -Os)
|
||||
8
tests/aiger/symbols.aig
Normal file
8
tests/aiger/symbols.aig
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
aig 2 1 1 1 0
|
||||
2 1
|
||||
4
|
||||
i0 d
|
||||
l0 q
|
||||
o0 q
|
||||
c
|
||||
Generated by Yosys 0.9+932 (git sha1 baba33fb, clang 9.0.0-2 -fPIC -Os)
|
||||
|
|
@ -2,7 +2,7 @@ read_verilog ../common/counter.v
|
|||
hierarchy -top top
|
||||
proc
|
||||
flatten
|
||||
equiv_opt -map +/anlogic/cells_sim.v synth_anlogic # equivalency check
|
||||
equiv_opt -assert -multiclock -map +/anlogic/cells_sim.v synth_anlogic # 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
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
read_verilog ../common/memory.v
|
||||
hierarchy -top top
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic
|
||||
|
|
@ -11,7 +11,7 @@ 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 top
|
||||
cd lutram_1w1r
|
||||
|
||||
select -assert-count 8 t:AL_MAP_LUT2
|
||||
select -assert-count 8 t:AL_MAP_LUT4
|
||||
45
tests/arch/common/blockram.v
Normal file
45
tests/arch/common/blockram.v
Normal file
|
|
@ -0,0 +1,45 @@
|
|||
`default_nettype none
|
||||
module sync_ram_sp #(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;
|
||||
data_out_r <= memory[address_in];
|
||||
end
|
||||
|
||||
assign data_out = data_out_r;
|
||||
endmodule // sync_ram_sp
|
||||
|
||||
|
||||
`default_nettype none
|
||||
module sync_ram_sdp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10)
|
||||
(input wire clk, write_enable,
|
||||
input wire [DATA_WIDTH-1:0] data_in,
|
||||
input wire [ADDRESS_WIDTH-1:0] address_in_r, address_in_w,
|
||||
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_w] <= data_in;
|
||||
data_out_r <= memory[address_in_r];
|
||||
end
|
||||
|
||||
assign data_out = data_out_r;
|
||||
endmodule // sync_ram_sdp
|
||||
|
||||
42
tests/arch/common/lutram.v
Normal file
42
tests/arch/common/lutram.v
Normal file
|
|
@ -0,0 +1,42 @@
|
|||
module lutram_1w1r
|
||||
#(parameter D_WIDTH=8, A_WIDTH=6)
|
||||
(
|
||||
input [D_WIDTH-1:0] data_a,
|
||||
input [A_WIDTH:1] addr_a,
|
||||
input we_a, clk,
|
||||
output reg [D_WIDTH-1:0] q_a
|
||||
);
|
||||
// Declare the RAM variable
|
||||
reg [D_WIDTH-1:0] ram[(2**A_WIDTH)-1:0];
|
||||
|
||||
// Port A
|
||||
always @ (posedge clk)
|
||||
begin
|
||||
if (we_a)
|
||||
ram[addr_a] <= data_a;
|
||||
q_a <= ram[addr_a];
|
||||
end
|
||||
endmodule
|
||||
|
||||
|
||||
module lutram_1w3r
|
||||
#(parameter D_WIDTH=8, A_WIDTH=5)
|
||||
(
|
||||
input [D_WIDTH-1:0] data_a, data_b, data_c,
|
||||
input [A_WIDTH:1] addr_a, addr_b, addr_c,
|
||||
input we_a, clk,
|
||||
output reg [D_WIDTH-1:0] q_a, q_b, q_c
|
||||
);
|
||||
// Declare the RAM variable
|
||||
reg [D_WIDTH-1:0] ram[(2**A_WIDTH)-1:0];
|
||||
|
||||
// Port A
|
||||
always @ (posedge clk)
|
||||
begin
|
||||
if (we_a)
|
||||
ram[addr_a] <= data_a;
|
||||
q_a <= ram[addr_a];
|
||||
q_b <= ram[addr_b];
|
||||
q_c <= ram[addr_c];
|
||||
end
|
||||
endmodule
|
||||
|
|
@ -1,21 +0,0 @@
|
|||
module top
|
||||
(
|
||||
input [7:0] data_a,
|
||||
input [6:1] addr_a,
|
||||
input we_a, clk,
|
||||
output reg [7:0] q_a
|
||||
);
|
||||
// Declare the RAM variable
|
||||
reg [7:0] ram[63:0];
|
||||
|
||||
// Port A
|
||||
always @ (posedge clk)
|
||||
begin
|
||||
if (we_a)
|
||||
begin
|
||||
ram[addr_a] <= data_a;
|
||||
q_a <= data_a;
|
||||
end
|
||||
q_a <= ram[addr_a];
|
||||
end
|
||||
endmodule
|
||||
88
tests/arch/common/memory_attributes/attributes_test.v
Normal file
88
tests/arch/common/memory_attributes/attributes_test.v
Normal file
|
|
@ -0,0 +1,88 @@
|
|||
`default_nettype none
|
||||
module block_ram #(parameter DATA_WIDTH=4, 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;
|
||||
data_out_r <= memory[address_in];
|
||||
end
|
||||
|
||||
assign data_out = data_out_r;
|
||||
endmodule // block_ram
|
||||
|
||||
`default_nettype none
|
||||
module distributed_ram #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=4)
|
||||
(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;
|
||||
data_out_r <= memory[address_in];
|
||||
end
|
||||
|
||||
assign data_out = data_out_r;
|
||||
endmodule // distributed_ram
|
||||
|
||||
`default_nettype none
|
||||
module distributed_ram_manual #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=4)
|
||||
(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;
|
||||
(* ram_style = "block" *) reg [WORD:0] memory [0:DEPTH];
|
||||
|
||||
always @(posedge clk) begin
|
||||
if (write_enable)
|
||||
memory[address_in] <= data_in;
|
||||
data_out_r <= memory[address_in];
|
||||
end
|
||||
|
||||
assign data_out = data_out_r;
|
||||
endmodule // distributed_ram
|
||||
|
||||
`default_nettype none
|
||||
module distributed_ram_manual_syn #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=4)
|
||||
(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;
|
||||
(* synthesis, ram_block *) reg [WORD:0] memory [0:DEPTH];
|
||||
|
||||
always @(posedge clk) begin
|
||||
if (write_enable)
|
||||
memory[address_in] <= data_in;
|
||||
data_out_r <= memory[address_in];
|
||||
end
|
||||
|
||||
assign data_out = data_out_r;
|
||||
endmodule // distributed_ram
|
||||
|
||||
25
tests/arch/ecp5/bug1459.ys
Normal file
25
tests/arch/ecp5/bug1459.ys
Normal file
|
|
@ -0,0 +1,25 @@
|
|||
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,
|
||||
output reg [63:0] read1_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];
|
||||
end
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
synth_ecp5 -abc9
|
||||
16
tests/arch/ecp5/bug1598.ys
Normal file
16
tests/arch/ecp5/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 +/ecp5/cells_sim.v synth_ecp5 -abc9
|
||||
BIN
tests/arch/ecp5/bug1630.il.gz
Normal file
BIN
tests/arch/ecp5/bug1630.il.gz
Normal file
Binary file not shown.
2
tests/arch/ecp5/bug1630.ys
Normal file
2
tests/arch/ecp5/bug1630.ys
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
read_ilang bug1630.il.gz
|
||||
abc9 -lut +/ecp5/abc9_5g.lut
|
||||
|
|
@ -2,7 +2,7 @@ read_verilog ../common/counter.v
|
|||
hierarchy -top top
|
||||
proc
|
||||
flatten
|
||||
equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
|
||||
equiv_opt -assert -multiclock -map +/ecp5/cells_sim.v synth_ecp5 # 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 4 t:CCU2C
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
read_verilog ../common/memory.v
|
||||
hierarchy -top top
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
|
||||
|
|
@ -10,7 +10,7 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
|||
sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd top
|
||||
cd lutram_1w1r
|
||||
select -assert-count 24 t:L6MUX21
|
||||
select -assert-count 71 t:LUT4
|
||||
select -assert-count 32 t:PFUMX
|
||||
|
|
@ -3,8 +3,8 @@ hierarchy -top top
|
|||
proc
|
||||
# Blocked by issue #1358 (Missing ECP5 simulation models)
|
||||
#equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
|
||||
equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
synth_ecp5
|
||||
#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:MULT18X18D
|
||||
select -assert-count 4 t:CCU2C
|
||||
|
|
|
|||
|
|
@ -3,9 +3,9 @@ hierarchy -top top
|
|||
proc
|
||||
# Blocked by issue #1358 (Missing ECP5 simulation models)
|
||||
#equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
|
||||
equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
|
||||
synth_ecp5
|
||||
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
#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:MULT18X18D
|
||||
select -assert-none t:MULT18X18D %% t:* %D
|
||||
|
|
|
|||
|
|
@ -39,8 +39,8 @@ proc
|
|||
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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-count 8 t:L6MUX21
|
||||
select -assert-count 26 t:LUT4
|
||||
select -assert-count 12 t:PFUMX
|
||||
select -assert-count 12 t:L6MUX21
|
||||
select -assert-count 34 t:LUT4
|
||||
select -assert-count 17 t:PFUMX
|
||||
|
||||
select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@ read_verilog ../common/counter.v
|
|||
hierarchy -top top
|
||||
proc
|
||||
flatten
|
||||
equiv_opt -map +/efinix/cells_sim.v synth_efinix # equivalency check
|
||||
equiv_opt -assert -multiclock -map +/efinix/cells_sim.v synth_efinix # 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
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
read_verilog ../common/memory.v
|
||||
hierarchy -top top
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/efinix/cells_sim.v synth_efinix
|
||||
|
|
@ -12,7 +12,7 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
|||
sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd top
|
||||
cd lutram_1w1r
|
||||
select -assert-count 1 t:EFX_GBUFCE
|
||||
select -assert-count 1 t:EFX_RAM_5K
|
||||
select -assert-none t:EFX_GBUFCE t:EFX_RAM_5K %% t:* %D
|
||||
|
|
@ -36,6 +36,6 @@ proc
|
|||
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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-count 12 t:EFX_LUT4
|
||||
select -assert-max 12 t:EFX_LUT4
|
||||
|
||||
select -assert-none t:EFX_LUT4 %% t:* %D
|
||||
|
|
|
|||
|
|
@ -34,11 +34,12 @@ proc
|
|||
equiv_opt -async2sync -assert -map +/gowin/cells_sim.v synth_gowin # 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:DFFS
|
||||
select -assert-count 1 t:DFF
|
||||
select -assert-count 1 t:LUT2
|
||||
select -assert-count 4 t:IBUF
|
||||
select -assert-count 1 t:OBUF
|
||||
|
||||
select -assert-none t:DFFS t:IBUF t:OBUF %% t:* %D
|
||||
select -assert-none t:DFF t:LUT2 t:IBUF t:OBUF %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@ read_verilog ../common/counter.v
|
|||
hierarchy -top top
|
||||
proc
|
||||
flatten
|
||||
equiv_opt -map +/gowin/cells_sim.v synth_gowin # equivalency check
|
||||
equiv_opt -assert -multiclock -map +/gowin/cells_sim.v synth_gowin # 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
|
||||
|
||||
|
|
|
|||
224
tests/arch/gowin/init.v
Normal file
224
tests/arch/gowin/init.v
Normal file
|
|
@ -0,0 +1,224 @@
|
|||
module myDFF (output reg Q, input CLK, D);
|
||||
parameter [0:0] INIT = 1'b0;
|
||||
initial Q = INIT;
|
||||
always @(posedge CLK)
|
||||
Q <= D;
|
||||
endmodule
|
||||
|
||||
module myDFFE (output reg Q, input D, CLK, CE);
|
||||
parameter [0:0] INIT = 1'b0;
|
||||
initial Q = INIT;
|
||||
always @(posedge CLK) begin
|
||||
if (CE)
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFE (positive clock edge; clock enable)
|
||||
|
||||
|
||||
module myDFFS (output reg Q, input D, CLK, SET);
|
||||
parameter [0:0] INIT = 1'b1;
|
||||
initial Q = INIT;
|
||||
always @(posedge CLK) begin
|
||||
if (SET)
|
||||
Q <= 1'b1;
|
||||
else
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFS (positive clock edge; synchronous set)
|
||||
|
||||
|
||||
module myDFFSE (output reg Q, input D, CLK, CE, SET);
|
||||
parameter [0:0] INIT = 1'b1;
|
||||
initial Q = INIT;
|
||||
always @(posedge CLK) begin
|
||||
if (SET)
|
||||
Q <= 1'b1;
|
||||
else if (CE)
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFSE (positive clock edge; synchronous set takes precedence over clock enable)
|
||||
|
||||
|
||||
module myDFFR (output reg Q, input D, CLK, RESET);
|
||||
parameter [0:0] INIT = 1'b0;
|
||||
initial Q = INIT;
|
||||
always @(posedge CLK) begin
|
||||
if (RESET)
|
||||
Q <= 1'b0;
|
||||
else
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFR (positive clock edge; synchronous reset)
|
||||
|
||||
|
||||
module myDFFRE (output reg Q, input D, CLK, CE, RESET);
|
||||
parameter [0:0] INIT = 1'b0;
|
||||
initial Q = INIT;
|
||||
always @(posedge CLK) begin
|
||||
if (RESET)
|
||||
Q <= 1'b0;
|
||||
else if (CE)
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFRE (positive clock edge; synchronous reset takes precedence over clock enable)
|
||||
|
||||
|
||||
module myDFFP (output reg Q, input D, CLK, PRESET);
|
||||
parameter [0:0] INIT = 1'b1;
|
||||
initial Q = INIT;
|
||||
always @(posedge CLK or posedge PRESET) begin
|
||||
if(PRESET)
|
||||
Q <= 1'b1;
|
||||
else
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFP (positive clock edge; asynchronous preset)
|
||||
|
||||
|
||||
module myDFFPE (output reg Q, input D, CLK, CE, PRESET);
|
||||
parameter [0:0] INIT = 1'b1;
|
||||
initial Q = INIT;
|
||||
always @(posedge CLK or posedge PRESET) begin
|
||||
if(PRESET)
|
||||
Q <= 1'b1;
|
||||
else if (CE)
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFPE (positive clock edge; asynchronous preset; clock enable)
|
||||
|
||||
|
||||
module myDFFC (output reg Q, input D, CLK, CLEAR);
|
||||
parameter [0:0] INIT = 1'b0;
|
||||
initial Q = INIT;
|
||||
always @(posedge CLK or posedge CLEAR) begin
|
||||
if(CLEAR)
|
||||
Q <= 1'b0;
|
||||
else
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFC (positive clock edge; asynchronous clear)
|
||||
|
||||
|
||||
module myDFFCE (output reg Q, input D, CLK, CE, CLEAR);
|
||||
parameter [0:0] INIT = 1'b0;
|
||||
initial Q = INIT;
|
||||
always @(posedge CLK or posedge CLEAR) begin
|
||||
if(CLEAR)
|
||||
Q <= 1'b0;
|
||||
else if (CE)
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFCE (positive clock edge; asynchronous clear; clock enable)
|
||||
|
||||
|
||||
module myDFFN (output reg Q, input CLK, D);
|
||||
parameter [0:0] INIT = 1'b0;
|
||||
initial Q = INIT;
|
||||
always @(negedge CLK)
|
||||
Q <= D;
|
||||
endmodule
|
||||
|
||||
module myDFFNE (output reg Q, input D, CLK, CE);
|
||||
parameter [0:0] INIT = 1'b0;
|
||||
initial Q = INIT;
|
||||
always @(negedge CLK) begin
|
||||
if (CE)
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFNE (negative clock edge; clock enable)
|
||||
|
||||
|
||||
module myDFFNS (output reg Q, input D, CLK, SET);
|
||||
parameter [0:0] INIT = 1'b1;
|
||||
initial Q = INIT;
|
||||
always @(negedge CLK) begin
|
||||
if (SET)
|
||||
Q <= 1'b1;
|
||||
else
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFNS (negative clock edge; synchronous set)
|
||||
|
||||
|
||||
module myDFFNSE (output reg Q, input D, CLK, CE, SET);
|
||||
parameter [0:0] INIT = 1'b1;
|
||||
initial Q = INIT;
|
||||
always @(negedge CLK) begin
|
||||
if (SET)
|
||||
Q <= 1'b1;
|
||||
else if (CE)
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFNSE (negative clock edge; synchronous set takes precedence over clock enable)
|
||||
|
||||
|
||||
module myDFFNR (output reg Q, input D, CLK, RESET);
|
||||
parameter [0:0] INIT = 1'b0;
|
||||
initial Q = INIT;
|
||||
always @(negedge CLK) begin
|
||||
if (RESET)
|
||||
Q <= 1'b0;
|
||||
else
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFNR (negative clock edge; synchronous reset)
|
||||
|
||||
|
||||
module myDFFNRE (output reg Q, input D, CLK, CE, RESET);
|
||||
parameter [0:0] INIT = 1'b0;
|
||||
initial Q = INIT;
|
||||
always @(negedge CLK) begin
|
||||
if (RESET)
|
||||
Q <= 1'b0;
|
||||
else if (CE)
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFNRE (negative clock edge; synchronous reset takes precedence over clock enable)
|
||||
|
||||
|
||||
module myDFFNP (output reg Q, input D, CLK, PRESET);
|
||||
parameter [0:0] INIT = 1'b1;
|
||||
initial Q = INIT;
|
||||
always @(negedge CLK or posedge PRESET) begin
|
||||
if(PRESET)
|
||||
Q <= 1'b1;
|
||||
else
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFNP (negative clock edge; asynchronous preset)
|
||||
|
||||
|
||||
module myDFFNPE (output reg Q, input D, CLK, CE, PRESET);
|
||||
parameter [0:0] INIT = 1'b1;
|
||||
initial Q = INIT;
|
||||
always @(negedge CLK or posedge PRESET) begin
|
||||
if(PRESET)
|
||||
Q <= 1'b1;
|
||||
else if (CE)
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFNPE (negative clock edge; asynchronous preset; clock enable)
|
||||
|
||||
|
||||
module myDFFNC (output reg Q, input D, CLK, CLEAR);
|
||||
parameter [0:0] INIT = 1'b0;
|
||||
initial Q = INIT;
|
||||
always @(negedge CLK or posedge CLEAR) begin
|
||||
if(CLEAR)
|
||||
Q <= 1'b0;
|
||||
else
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFNC (negative clock edge; asynchronous clear)
|
||||
|
||||
|
||||
module myDFFNCE (output reg Q, input D, CLK, CE, CLEAR);
|
||||
parameter [0:0] INIT = 1'b0;
|
||||
initial Q = INIT;
|
||||
always @(negedge CLK or posedge CLEAR) begin
|
||||
if(CLEAR)
|
||||
Q <= 1'b0;
|
||||
else if (CE)
|
||||
Q <= D;
|
||||
end
|
||||
endmodule // DFFNCE (negative clock edge; asynchronous clear; clock enable)
|
||||
74
tests/arch/gowin/init.ys
Normal file
74
tests/arch/gowin/init.ys
Normal file
|
|
@ -0,0 +1,74 @@
|
|||
read_verilog init.v
|
||||
read_verilog -lib +/gowin/cells_sim.v
|
||||
design -save read
|
||||
|
||||
proc
|
||||
flatten
|
||||
synth_gowin -run coarse:
|
||||
|
||||
# check if all init values are handled
|
||||
check -assert -noinit
|
||||
# check if every flop mapped correctly
|
||||
select -assert-count 1 t:DFF
|
||||
select -assert-count 1 t:DFFC
|
||||
select -assert-count 1 t:DFFCE
|
||||
select -assert-count 1 t:DFFE
|
||||
select -assert-count 1 t:DFFN
|
||||
select -assert-count 1 t:DFFNC
|
||||
select -assert-count 1 t:DFFNCE
|
||||
select -assert-count 1 t:DFFNE
|
||||
select -assert-count 1 t:DFFNP
|
||||
select -assert-count 1 t:DFFNPE
|
||||
select -assert-count 1 t:DFFNR
|
||||
select -assert-count 1 t:DFFNRE
|
||||
select -assert-count 1 t:DFFNS
|
||||
select -assert-count 1 t:DFFNSE
|
||||
select -assert-count 1 t:DFFP
|
||||
select -assert-count 1 t:DFFPE
|
||||
select -assert-count 1 t:DFFR
|
||||
select -assert-count 1 t:DFFRE
|
||||
select -assert-count 1 t:DFFS
|
||||
select -assert-count 1 t:DFFSE
|
||||
|
||||
delete
|
||||
design -load read
|
||||
|
||||
# these should synth to a flop with reset
|
||||
chparam -set INIT 1 myDFF myDFFN myDFFE myDFFNE
|
||||
|
||||
# async should give a warning
|
||||
# sync should synth to a mux
|
||||
chparam -set INIT 0 myDFF*S* myDFF*P*
|
||||
chparam -set INIT 1 myDFF*R* myDFF*C*
|
||||
|
||||
proc
|
||||
flatten
|
||||
synth_gowin -run coarse:
|
||||
|
||||
# check the flops mapped as expected
|
||||
select -assert-count 1 t:DFF
|
||||
select -assert-count 1 t:DFFC
|
||||
select -assert-count 1 t:DFFCE
|
||||
select -assert-count 1 t:DFFE
|
||||
select -assert-count 1 t:DFFN
|
||||
select -assert-count 1 t:DFFNC
|
||||
select -assert-count 1 t:DFFNCE
|
||||
select -assert-count 1 t:DFFNE
|
||||
select -assert-count 1 t:DFFNP
|
||||
select -assert-count 1 t:DFFNPE
|
||||
select -assert-count 0 t:DFFNR
|
||||
select -assert-count 0 t:DFFNRE
|
||||
select -assert-count 2 t:DFFNS
|
||||
select -assert-count 2 t:DFFNSE
|
||||
select -assert-count 1 t:DFFP
|
||||
select -assert-count 1 t:DFFPE
|
||||
select -assert-count 0 t:DFFR
|
||||
select -assert-count 0 t:DFFRE
|
||||
select -assert-count 2 t:DFFS
|
||||
select -assert-count 2 t:DFFSE
|
||||
select -assert-count 12 t:LUT2
|
||||
|
||||
# check the expected leftover init values
|
||||
# this would happen if your reset value is not the initial value
|
||||
# which would be weird
|
||||
select -assert-count 8 a:init
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
read_verilog ../common/memory.v
|
||||
hierarchy -top top
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/gowin/cells_sim.v synth_gowin
|
||||
|
|
@ -12,7 +12,7 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
|||
sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd top
|
||||
cd lutram_1w1r
|
||||
select -assert-count 8 t:RAM16S4
|
||||
# other logic present that is not simple
|
||||
#select -assert-none t:RAM16S4 %% t:* %D
|
||||
72
tests/arch/ice40/bug1597.ys
Normal file
72
tests/arch/ice40/bug1597.ys
Normal file
|
|
@ -0,0 +1,72 @@
|
|||
read_verilog <<EOT
|
||||
module top (
|
||||
input CLK, PIN_1, PIN_2, PIN_3, PIN_4, PIN_5,
|
||||
PIN_6, PIN_7, PIN_8, PIN_9, PIN_10, PIN_11, PIN_12, PIN_13, PIN_25,
|
||||
output USBPU, PIN_14, PIN_15, PIN_16, PIN_17, PIN_18,
|
||||
PIN_19, PIN_20, PIN_21, PIN_22, PIN_23, PIN_24,
|
||||
);
|
||||
assign USBPU = 0;
|
||||
|
||||
wire[5:0] parOut;
|
||||
wire[5:0] chrg;
|
||||
|
||||
assign PIN_14 = parOut[0];
|
||||
assign PIN_15 = parOut[1];
|
||||
assign PIN_16 = parOut[2];
|
||||
assign PIN_17 = parOut[3];
|
||||
assign PIN_18 = parOut[4];
|
||||
assign PIN_19 = parOut[5];
|
||||
assign chrg[0] = PIN_3;
|
||||
assign chrg[1] = PIN_4;
|
||||
assign chrg[2] = PIN_5;
|
||||
assign chrg[3] = PIN_6;
|
||||
assign chrg[4] = PIN_7;
|
||||
assign chrg[5] = PIN_8;
|
||||
|
||||
SSCounter6o sc6(PIN_1, CLK, PIN_2, PIN_9, chrg, parOut);
|
||||
|
||||
endmodule
|
||||
|
||||
module SSCounter6 (input wire rst, clk, adv, jmp, input wire [5:0] in, output reg[5:0] out);
|
||||
always @(posedge clk, posedge rst)
|
||||
if (rst) out <= 0;
|
||||
else if (adv || jmp) out <= jmp ? in : out + 1;
|
||||
endmodule
|
||||
|
||||
// Optimized 6 bit counter, it should takes 7 cells.
|
||||
/* b[5:1] /* b[0]
|
||||
1010101010101010 in 1010101010101010 in
|
||||
1100110011001100 jmp 1100110011001100 jmp
|
||||
1111000011110000 loop 1111000011110000 loop
|
||||
1111111100000000 carry 1111111100000000 -
|
||||
---------------------- ----------------------
|
||||
1000101110111000 out 1000101110001011 out
|
||||
8 B B 8 8 B 8 B
|
||||
*/
|
||||
module SSCounter6o (input wire rst, clk, adv, jmp, input wire [5:0] in, output wire[5:0] out);
|
||||
wire[4:0] co;
|
||||
wire[5:0] lo;
|
||||
wire ien;
|
||||
SB_LUT4 #(.LUT_INIT(16'hFFF0)) lien (ien, 0, 0, adv, jmp);
|
||||
SB_CARRY c0 (co[0], jmp, out[0], 1),
|
||||
c1 (co[1], jmp, out[1], co[0]),
|
||||
c2 (co[2], jmp, out[2], co[1]),
|
||||
c3 (co[3], jmp, out[3], co[2]),
|
||||
c4 (co[4], jmp, out[4], co[3]);
|
||||
SB_DFFER d0 (out[0], clk, ien, rst, lo[0]),
|
||||
d1 (out[1], clk, ien, rst, lo[1]),
|
||||
d2 (out[2], clk, ien, rst, lo[2]),
|
||||
d3 (out[3], clk, ien, rst, lo[3]),
|
||||
d4 (out[4], clk, ien, rst, lo[4]),
|
||||
d5 (out[5], clk, ien, rst, lo[5]);
|
||||
SB_LUT4 #(.LUT_INIT(16'h8B8B)) l0 (lo[0], in[0], jmp, out[0], 0);
|
||||
SB_LUT4 #(.LUT_INIT(16'h8BB8)) l1 (lo[1], in[1], jmp, out[1], co[0]);
|
||||
SB_LUT4 #(.LUT_INIT(16'h8BB8)) l2 (lo[2], in[2], jmp, out[2], co[1]);
|
||||
SB_LUT4 #(.LUT_INIT(16'h8BB8)) l3 (lo[3], in[3], jmp, out[3], co[2]);
|
||||
SB_LUT4 #(.LUT_INIT(16'h8BB8)) l4 (lo[4], in[4], jmp, out[4], co[3]);
|
||||
SB_LUT4 #(.LUT_INIT(16'h8BB8)) l5 (lo[5], in[5], jmp, out[5], co[4]);
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -top top
|
||||
flatten
|
||||
equiv_opt -multiclock -map +/ice40/cells_sim.v synth_ice40
|
||||
16
tests/arch/ice40/bug1598.ys
Normal file
16
tests/arch/ice40/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 +/ice40/cells_sim.v synth_ice40 -abc9
|
||||
217
tests/arch/ice40/bug1626.ys
Normal file
217
tests/arch/ice40/bug1626.ys
Normal file
|
|
@ -0,0 +1,217 @@
|
|||
read_ilang <<EOT
|
||||
# Generated by Yosys 0.9+1706 (git sha1 58ab9f60, clang 6.0.0-1ubuntu2 -fPIC -Os)
|
||||
autoidx 2815
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:9"
|
||||
attribute \cells_not_processed 1
|
||||
attribute \dynports 1
|
||||
module \ahb_async_sram_halfwidth
|
||||
parameter \DEPTH
|
||||
parameter \W_ADDR
|
||||
parameter \W_BYTEADDR
|
||||
parameter \W_DATA
|
||||
parameter \W_SRAM_ADDR
|
||||
parameter \W_SRAM_DATA
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:71"
|
||||
wire $0\addr_lsb[0:0]
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:71"
|
||||
wire $0\hready_r[0:0]
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:71"
|
||||
wire $0\long_dphase[0:0]
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:71"
|
||||
wire width 16 $0\rdata_buf[15:0]
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:71"
|
||||
wire $0\read_dph[0:0]
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:71"
|
||||
wire $0\write_dph[0:0]
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:63"
|
||||
wire width 32 $add$../hdl/mem/ahb_async_sram_halfwidth.v:63$2433_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:62"
|
||||
wire width 16 $and$../hdl/mem/ahb_async_sram_halfwidth.v:62$2431_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:56"
|
||||
wire $eq$../hdl/mem/ahb_async_sram_halfwidth.v:56$2424_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2450_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2451_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2452_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2453_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2454_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2455_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2456_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2457_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2458_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:112"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:112$2459_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:118"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:118$2444_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:133"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:133$2449_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:140"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:140$2461_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:140"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:140$2463_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:58"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:58$2425_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:59"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:59$2426_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:59"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:59$2427_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:59"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:59$2429_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:91"
|
||||
wire $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:91$2441_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:104"
|
||||
wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:104$2442_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:118"
|
||||
wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:118$2443_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:125"
|
||||
wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:125$2446_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:132"
|
||||
wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:132$2447_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:59"
|
||||
wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:59$2428_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:72"
|
||||
wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:72$2437_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:81"
|
||||
wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:81$2438_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:83"
|
||||
wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:83$2439_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:91"
|
||||
wire $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:91$2440_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:118"
|
||||
wire $logic_or$../hdl/mem/ahb_async_sram_halfwidth.v:118$2445_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:132"
|
||||
wire $logic_or$../hdl/mem/ahb_async_sram_halfwidth.v:132$2448_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:59"
|
||||
wire $logic_or$../hdl/mem/ahb_async_sram_halfwidth.v:59$2430_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:139"
|
||||
wire width 2 $not$../hdl/mem/ahb_async_sram_halfwidth.v:139$2460_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:139"
|
||||
wire width 2 $not$../hdl/mem/ahb_async_sram_halfwidth.v:139$2462_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:54"
|
||||
wire width 2 $not$../hdl/mem/ahb_async_sram_halfwidth.v:54$2421_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:63"
|
||||
wire width 16 $shiftx$../hdl/mem/ahb_async_sram_halfwidth.v:63$2434_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:54"
|
||||
wire width 8 $shl$../hdl/mem/ahb_async_sram_halfwidth.v:54$2419_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:54"
|
||||
wire width 2 $shl$../hdl/mem/ahb_async_sram_halfwidth.v:54$2420_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:55"
|
||||
wire width 2 $shl$../hdl/mem/ahb_async_sram_halfwidth.v:55$2422_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:56"
|
||||
wire width 32 $shl$../hdl/mem/ahb_async_sram_halfwidth.v:56$2423_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:63"
|
||||
wire width 32 $ternary$../hdl/mem/ahb_async_sram_halfwidth.v:63$2432_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:65"
|
||||
wire width 16 $ternary$../hdl/mem/ahb_async_sram_halfwidth.v:65$2435_Y
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:50"
|
||||
wire \addr_lsb
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:24"
|
||||
wire width 32 \ahbls_haddr
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:28"
|
||||
wire width 3 \ahbls_hburst
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:30"
|
||||
wire \ahbls_hmastlock
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:29"
|
||||
wire width 4 \ahbls_hprot
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:32"
|
||||
wire width 32 \ahbls_hrdata
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:22"
|
||||
wire \ahbls_hready
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:21"
|
||||
wire \ahbls_hready_resp
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:23"
|
||||
wire \ahbls_hresp
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:27"
|
||||
wire width 3 \ahbls_hsize
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:26"
|
||||
wire width 2 \ahbls_htrans
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:31"
|
||||
wire width 32 \ahbls_hwdata
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:25"
|
||||
wire \ahbls_hwrite
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:56"
|
||||
wire \aphase_full_width
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:55"
|
||||
wire width 2 \bytemask
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:54"
|
||||
wire width 2 \bytemask_noshift
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:17"
|
||||
wire \clk
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:46"
|
||||
wire \hready_r
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:47"
|
||||
wire \long_dphase
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:64"
|
||||
wire width 16 \rdata_buf
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:49"
|
||||
wire \read_dph
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:18"
|
||||
wire \rst_n
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:34"
|
||||
wire width 11 \sram_addr
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:39"
|
||||
wire width 2 \sram_byte_n
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:36"
|
||||
wire \sram_ce_n
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:35"
|
||||
wire width 16 \sram_dq
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:38"
|
||||
wire \sram_oe_n
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:61"
|
||||
wire width 16 \sram_q
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:62"
|
||||
wire width 16 \sram_rdata
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:63"
|
||||
wire width 16 \sram_wdata
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:37"
|
||||
wire \sram_we_n
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:58"
|
||||
wire \we_next
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:48"
|
||||
wire \write_dph
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:71"
|
||||
process $proc$../hdl/mem/ahb_async_sram_halfwidth.v:71$2436
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:72"
|
||||
switch $logic_not$../hdl/mem/ahb_async_sram_halfwidth.v:72$2437_Y
|
||||
case 1'1
|
||||
case
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:78"
|
||||
switch \ahbls_hready
|
||||
case 1'1
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:79"
|
||||
switch \ahbls_htrans [1]
|
||||
case 1'1
|
||||
case
|
||||
end
|
||||
case
|
||||
attribute \src "../hdl/mem/ahb_async_sram_halfwidth.v:91"
|
||||
switch $logic_and$../hdl/mem/ahb_async_sram_halfwidth.v:91$2441_Y
|
||||
case 1'1
|
||||
case
|
||||
end
|
||||
end
|
||||
end
|
||||
sync posedge \clk
|
||||
sync negedge \rst_n
|
||||
end
|
||||
connect \ahbls_hresp 1'0
|
||||
connect \bytemask_noshift $not$../hdl/mem/ahb_async_sram_halfwidth.v:54$2421_Y
|
||||
connect \bytemask $shl$../hdl/mem/ahb_async_sram_halfwidth.v:55$2422_Y
|
||||
connect \aphase_full_width $eq$../hdl/mem/ahb_async_sram_halfwidth.v:56$2424_Y
|
||||
connect \we_next $logic_or$../hdl/mem/ahb_async_sram_halfwidth.v:59$2430_Y
|
||||
connect \sram_rdata $and$../hdl/mem/ahb_async_sram_halfwidth.v:62$2431_Y
|
||||
connect \sram_wdata $shiftx$../hdl/mem/ahb_async_sram_halfwidth.v:63$2434_Y
|
||||
connect \ahbls_hrdata { \sram_rdata $ternary$../hdl/mem/ahb_async_sram_halfwidth.v:65$2435_Y }
|
||||
connect \ahbls_hready_resp \hready_r
|
||||
end
|
||||
EOT
|
||||
|
||||
synth_ice40 -abc2 -abc9
|
||||
BIN
tests/arch/ice40/bug1644.il.gz
Normal file
BIN
tests/arch/ice40/bug1644.il.gz
Normal file
Binary file not shown.
2
tests/arch/ice40/bug1644.ys
Normal file
2
tests/arch/ice40/bug1644.ys
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
read_ilang bug1644.il.gz
|
||||
synth_ice40 -top top -dsp -json adc_dac_pass_through.json -run :map_bram
|
||||
|
|
@ -2,7 +2,7 @@ read_verilog ../common/counter.v
|
|||
hierarchy -top top
|
||||
proc
|
||||
flatten
|
||||
equiv_opt -map +/ice40/cells_sim.v synth_ice40 # equivalency check
|
||||
equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 # 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 6 t:SB_CARRY
|
||||
|
|
|
|||
11
tests/arch/ice40/ice40_dsp.ys
Normal file
11
tests/arch/ice40/ice40_dsp.ys
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
read_verilog <<EOT
|
||||
module top(input [15:0] a, b, output [31:0] o1, o2, o5);
|
||||
SB_MAC16 m1 (.A(a), .B(16'd1234), .O(o1));
|
||||
assign o2 = a * 16'd0;
|
||||
wire [31:0] o3, o4;
|
||||
SB_MAC16 m2 (.A(a), .B(b), .O(o3));
|
||||
assign o4 = a * b;
|
||||
SB_MAC16 m3 (.A(a), .B(b), .O(o5));
|
||||
endmodule
|
||||
EOT
|
||||
ice40_dsp
|
||||
|
|
@ -6,13 +6,14 @@ module top(input CI, I0, output [1:0] CO, output O);
|
|||
// A[1]: 1100 1100 1100 1100
|
||||
// A[2]: 1111 0000 1111 0000
|
||||
// A[3]: 1111 1111 0000 0000
|
||||
.LUT(~16'b 0110_1001_1001_0110)
|
||||
.LUT(~16'b 0110_1001_1001_0110),
|
||||
.I3_IS_CI(1'b1)
|
||||
) u0 (
|
||||
.A(A),
|
||||
.B(B),
|
||||
.CI(CI),
|
||||
.I0(I0),
|
||||
.I3(CI),
|
||||
.I3(1'bx),
|
||||
.CO(CO[0]),
|
||||
.O(O)
|
||||
);
|
||||
|
|
@ -20,7 +21,98 @@ module top(input CI, I0, output [1:0] CO, output O);
|
|||
endmodule
|
||||
EOT
|
||||
|
||||
equiv_opt -assert -map +/ice40/cells_map.v -map +/ice40/cells_sim.v ice40_opt
|
||||
equiv_opt -assert -map +/ice40/abc9_model.v -map +/ice40/cells_sim.v ice40_opt
|
||||
design -load postopt
|
||||
select -assert-count 1 t:*
|
||||
select -assert-count 1 t:$lut
|
||||
|
||||
# https://github.com/YosysHQ/yosys/issues/1543
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module delay_element (input wire clk, input wire reset, input wire enable,
|
||||
input wire chainin, output wire chainout, output reg latch);
|
||||
|
||||
|
||||
reg const_zero = 0;
|
||||
reg const_one = 1;
|
||||
|
||||
wire delay_tap;
|
||||
|
||||
|
||||
//carry logic
|
||||
(* keep *) SB_CARRY carry ( .CO(chainout), .I0(const_zero),
|
||||
.I1(const_one), .CI(chainin));
|
||||
|
||||
|
||||
//flip flop latch
|
||||
(* keep *) SB_DFFER flipflop( .Q(latch), .C(clk), .E(enable),
|
||||
.D(delay_tap), .R(reset));
|
||||
|
||||
|
||||
//LUT table
|
||||
// the LUT should just echo the carry in (I3)
|
||||
// carry I0 = LUT I1
|
||||
// carry I1 = LUT I2
|
||||
// carry in = LUT I3
|
||||
// LUT_INIT[0] = 0
|
||||
// LUT_INIT[1] = 0
|
||||
// LUT_INIT[2] = 0
|
||||
// LUT_INIT[3] = 0
|
||||
// LUT_INIT[4] = 0
|
||||
// LUT_INIT[5] = 0
|
||||
// LUT_INIT[6] = 0
|
||||
// LUT_INIT[7] = 0
|
||||
// LUT_INIT[8] = 1
|
||||
// LUT_INIT[9] = 1
|
||||
// LUT_INIT[10] = 1
|
||||
// LUT_INIT[11] = 1
|
||||
// LUT_INIT[12] = 1
|
||||
// LUT_INIT[13] = 1
|
||||
// LUT_INIT[14] = 1
|
||||
// LUT_INIT[15] = 1
|
||||
|
||||
(* keep *) SB_LUT4 lut( .O(delay_tap), .I0(const_zero), .I1(const_zero),
|
||||
.I2(const_one), .I3(chainin));
|
||||
|
||||
//TODO: is this the right way round??
|
||||
defparam lut.LUT_INIT=16'hFF00;
|
||||
|
||||
|
||||
endmodule // delay_element
|
||||
EOT
|
||||
|
||||
synth_ice40
|
||||
select -assert-count 1 t:SB_LUT4
|
||||
select -assert-count 1 t:SB_CARRY
|
||||
select -assert-count 1 t:SB_CARRY a:keep %i
|
||||
select -assert-count 1 t:SB_CARRY c:carry %i
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog -icells <<EOT
|
||||
module top(input I3, I2, I1, I0, output O, O2);
|
||||
SB_LUT4 #(
|
||||
.LUT_INIT(8'b 1001_0110)
|
||||
) u0 (
|
||||
.I0(I0),
|
||||
.I1(I1),
|
||||
.I2(I2),
|
||||
.I3(),
|
||||
.O(O)
|
||||
);
|
||||
wire CO;
|
||||
\$__ICE40_CARRY_WRAPPER #(
|
||||
.LUT(~8'b 1001_0110),
|
||||
.I3_IS_CI(1'b0)
|
||||
) u1 (
|
||||
.A(1'b0),
|
||||
.B(1'b0),
|
||||
.CI(1'b0),
|
||||
.I0(),
|
||||
.I3(),
|
||||
.CO(CO),
|
||||
.O(O2)
|
||||
);
|
||||
endmodule
|
||||
EOT
|
||||
ice40_opt
|
||||
|
|
|
|||
54
tests/arch/ice40/ice40_wrapcarry.ys
Normal file
54
tests/arch/ice40/ice40_wrapcarry.ys
Normal file
|
|
@ -0,0 +1,54 @@
|
|||
read_verilog <<EOT
|
||||
module top(input A, B, CI, output O, CO);
|
||||
SB_CARRY carry (
|
||||
.I0(A),
|
||||
.I1(B),
|
||||
.CI(CI),
|
||||
.CO(CO)
|
||||
);
|
||||
SB_LUT4 #(
|
||||
.LUT_INIT(16'b 0110_1001_1001_0110)
|
||||
) adder (
|
||||
.I0(1'b0),
|
||||
.I1(A),
|
||||
.I2(B),
|
||||
.I3(1'b0),
|
||||
.O(O)
|
||||
);
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
ice40_wrapcarry
|
||||
select -assert-count 1 t:$__ICE40_CARRY_WRAPPER
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input A, B, CI, output O, CO);
|
||||
(* foo = "bar", answer = 42, keep=0 *)
|
||||
SB_CARRY carry (
|
||||
.I0(A),
|
||||
.I1(B),
|
||||
.CI(CI),
|
||||
.CO(CO)
|
||||
);
|
||||
(* keep, blah="blah", answer = 43 *)
|
||||
SB_LUT4 #(
|
||||
.LUT_INIT(16'b 0110_1001_1001_0110)
|
||||
) adder (
|
||||
.I0(1'b0),
|
||||
.I1(A),
|
||||
.I2(B),
|
||||
.I3(1'b0),
|
||||
.O(O)
|
||||
);
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
ice40_wrapcarry
|
||||
select -assert-count 1 t:$__ICE40_CARRY_WRAPPER
|
||||
select -assert-count 0 t:* t:$__ICE40_CARRY_WRAPPER %d
|
||||
select -assert-count 1 a:keep=1 a:SB_CARRY.\foo=bar %i a:SB_CARRY.\answer=42 %i a:SB_LUT4.\blah=blah %i a:SB_LUT4.\answer=43 %i
|
||||
|
||||
ice40_wrapcarry -unwrap
|
||||
select -assert-count 1 c:carry a:src=<<EOT:3 %i a:keep=0 %i a:foo=bar %i a:answer=42 %i
|
||||
select -assert-count 1 c:adder a:src=<<EOT:10 %i a:keep=1 %i a:blah=blah %i a:answer=43 %i
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
read_verilog ../common/memory.v
|
||||
hierarchy -top top
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
|
||||
|
|
@ -10,6 +10,6 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
|||
sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd top
|
||||
cd lutram_1w1r
|
||||
select -assert-count 1 t:SB_RAM40_4K
|
||||
select -assert-none t:SB_RAM40_4K %% t:* %D
|
||||
|
|
@ -1,6 +1,6 @@
|
|||
read_verilog ../common/mul.v
|
||||
hierarchy -top top
|
||||
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
|
||||
equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 -dsp # 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:SB_MAC16
|
||||
|
|
|
|||
|
|
@ -2,7 +2,8 @@
|
|||
Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 74].
|
||||
*/
|
||||
module top(data, addr);
|
||||
output [3:0] data;
|
||||
output [3:0] data; // Note: this prompts a Yosys warning, but
|
||||
// vendor doc does not contain 'reg'
|
||||
input [4:0] addr;
|
||||
always @(addr) begin
|
||||
case (addr)
|
||||
|
|
|
|||
|
|
@ -1,22 +0,0 @@
|
|||
read_verilog <<EOT
|
||||
module top(input A, B, CI, output O, CO);
|
||||
SB_CARRY carry (
|
||||
.I0(A),
|
||||
.I1(B),
|
||||
.CI(CI),
|
||||
.CO(CO)
|
||||
);
|
||||
SB_LUT4 #(
|
||||
.LUT_INIT(16'b 0110_1001_1001_0110)
|
||||
) adder (
|
||||
.I0(1'b0),
|
||||
.I1(A),
|
||||
.I2(B),
|
||||
.I3(1'b0),
|
||||
.O(O)
|
||||
);
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
ice40_wrapcarry
|
||||
select -assert-count 1 t:$__ICE40_CARRY_WRAPPER
|
||||
32
tests/arch/xilinx/abc9_dff.ys
Normal file
32
tests/arch/xilinx/abc9_dff.ys
Normal file
|
|
@ -0,0 +1,32 @@
|
|||
read_verilog <<EOT
|
||||
module top(input C, D, output [7:0] Q);
|
||||
FDRE fd1(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[0]));
|
||||
FDSE fd2(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[1]));
|
||||
FDCE fd3(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[2]));
|
||||
FDPE fd4(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[3]));
|
||||
FDRE_1 fd5(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[4]));
|
||||
FDSE_1 fd6(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[5]));
|
||||
FDCE_1 fd7(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[6]));
|
||||
FDPE_1 fd8(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[7]));
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
|
||||
design -load postopt
|
||||
select -assert-none t:FD*
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input C, D, output [7:0] Q);
|
||||
FDRE fd1(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[0]));
|
||||
FDSE fd2(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[1]));
|
||||
FDCE fd3(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[2]));
|
||||
FDPE fd4(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[3]));
|
||||
FDRE_1 fd5(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[4]));
|
||||
FDSE_1 fd6(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[5]));
|
||||
FDCE_1 fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6]));
|
||||
FDPE_1 fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7]));
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
|
||||
design -load postopt
|
||||
select -assert-none t:FD*
|
||||
91
tests/arch/xilinx/abc9_map.ys
Normal file
91
tests/arch/xilinx/abc9_map.ys
Normal file
|
|
@ -0,0 +1,91 @@
|
|||
read_verilog <<EOT
|
||||
module top(input C, CE, D, R, output [1:0] Q);
|
||||
FDRE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .R(R), .Q(Q[0]));
|
||||
FDRE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .R(R), .Q(Q[1]));
|
||||
endmodule
|
||||
EOT
|
||||
design -save gold
|
||||
|
||||
techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
|
||||
techmap -map +/xilinx/abc9_unmap.v
|
||||
select -assert-count 1 t:FDSE
|
||||
select -assert-count 1 t:FDSE_1
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
design -stash gate
|
||||
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -seq 2 -verify -prove-asserts -show-ports miter
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input C, CE, D, S, output [1:0] Q);
|
||||
FDSE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .S(S), .Q(Q[0]));
|
||||
FDSE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .S(S), .Q(Q[1]));
|
||||
endmodule
|
||||
EOT
|
||||
design -save gold
|
||||
|
||||
techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
|
||||
techmap -map +/xilinx/abc9_unmap.v
|
||||
select -assert-count 1 t:FDRE
|
||||
select -assert-count 1 t:FDRE_1
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
design -stash gate
|
||||
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input C, CE, D, PRE, output [1:0] Q);
|
||||
FDPE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .PRE(PRE), .Q(Q[0]));
|
||||
FDPE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .PRE(PRE), .Q(Q[1]));
|
||||
endmodule
|
||||
EOT
|
||||
design -save gold
|
||||
|
||||
techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
|
||||
techmap -map +/xilinx/abc9_unmap.v
|
||||
select -assert-count 1 t:FDCE
|
||||
select -assert-count 1 t:FDCE_1
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
design -stash gate
|
||||
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
clk2fflogic
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input C, CE, D, CLR, output [1:0] Q);
|
||||
FDCE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .CLR(CLR), .Q(Q[0]));
|
||||
FDCE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .CLR(CLR), .Q(Q[1]));
|
||||
endmodule
|
||||
EOT
|
||||
design -save gold
|
||||
|
||||
techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
|
||||
techmap -map +/xilinx/abc9_unmap.v
|
||||
select -assert-count 1 t:FDPE
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
design -stash gate
|
||||
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
clk2fflogic
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
|
||||
|
|
@ -1,11 +1,11 @@
|
|||
read_verilog ../common/add_sub.v
|
||||
hierarchy -top top
|
||||
proc
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -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 14 t:LUT2
|
||||
select -assert-count 6 t:MUXCY
|
||||
select -assert-count 8 t:XORCY
|
||||
select -assert-none t:LUT2 t:MUXCY t:XORCY %% t:* %D
|
||||
stat
|
||||
select -assert-count 16 t:LUT2
|
||||
select -assert-count 2 t:CARRY4
|
||||
select -assert-none t:LUT2 t:CARRY4 %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ design -save read
|
|||
|
||||
hierarchy -top adff
|
||||
proc
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -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:BUFG
|
||||
|
|
@ -15,37 +15,36 @@ select -assert-none t:BUFG t:FDCE %% t:* %D
|
|||
design -load read
|
||||
hierarchy -top adffn
|
||||
proc
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -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:BUFG
|
||||
select -assert-count 1 t:FDCE
|
||||
select -assert-count 1 t:LUT1
|
||||
select -assert-count 1 t:INV
|
||||
|
||||
select -assert-none t:BUFG t:FDCE t:LUT1 %% t:* %D
|
||||
select -assert-none t:BUFG t:FDCE t:INV %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top dffs
|
||||
proc
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -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:BUFG
|
||||
select -assert-count 1 t:FDRE
|
||||
select -assert-count 1 t:LUT2
|
||||
select -assert-count 1 t:FDSE
|
||||
|
||||
select -assert-none t:BUFG t:FDRE t:LUT2 %% t:* %D
|
||||
select -assert-none t:BUFG t:FDSE %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top ndffnr
|
||||
proc
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -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:BUFG
|
||||
select -assert-count 1 t:FDRE_1
|
||||
select -assert-count 1 t:LUT2
|
||||
select -assert-count 1 t:INV
|
||||
|
||||
select -assert-none t:BUFG t:FDRE_1 t:LUT2 %% t:* %D
|
||||
select -assert-none t:BUFG t:FDRE_1 t:INV %% t:* %D
|
||||
|
|
|
|||
47
tests/arch/xilinx/attributes_test.ys
Normal file
47
tests/arch/xilinx/attributes_test.ys
Normal file
|
|
@ -0,0 +1,47 @@
|
|||
# Check that blockram memory without parameters is not modified
|
||||
read_verilog ../common/memory_attributes/attributes_test.v
|
||||
hierarchy -top block_ram
|
||||
synth_xilinx -top block_ram -noiopad
|
||||
cd block_ram # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:RAMB18E1
|
||||
|
||||
# Check that distributed memory without parameters is not modified
|
||||
design -reset
|
||||
read_verilog ../common/memory_attributes/attributes_test.v
|
||||
hierarchy -top distributed_ram
|
||||
synth_xilinx -top distributed_ram -noiopad
|
||||
cd distributed_ram # Constrain all select calls below inside the top module
|
||||
select -assert-count 8 t:RAM32X1D
|
||||
|
||||
# Set ram_style distributed to blockram memory; will be implemented as distributed
|
||||
design -reset
|
||||
read_verilog ../common/memory_attributes/attributes_test.v
|
||||
prep
|
||||
setattr -mod -set ram_style "distributed" block_ram
|
||||
synth_xilinx -top block_ram -noiopad
|
||||
cd block_ram # Constrain all select calls below inside the top module
|
||||
select -assert-count 32 t:RAM128X1D
|
||||
|
||||
# Set synthesis, logic_block to blockram memory; will be implemented as distributed
|
||||
design -reset
|
||||
read_verilog ../common/memory_attributes/attributes_test.v
|
||||
prep
|
||||
setattr -mod -set logic_block 1 block_ram
|
||||
synth_xilinx -top block_ram -noiopad
|
||||
cd block_ram # Constrain all select calls below inside the top module
|
||||
select -assert-count 0 t:RAMB18E1
|
||||
select -assert-count 32 t:RAM128X1D
|
||||
|
||||
# Set ram_style block to a distributed memory; will be implemented as blockram
|
||||
design -reset
|
||||
read_verilog ../common/memory_attributes/attributes_test.v
|
||||
synth_xilinx -top distributed_ram_manual -noiopad
|
||||
cd distributed_ram_manual # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:RAMB18E1
|
||||
|
||||
# Set synthesis, ram_block block to a distributed memory; will be implemented as blockram
|
||||
design -reset
|
||||
read_verilog ../common/memory_attributes/attributes_test.v
|
||||
synth_xilinx -top distributed_ram_manual_syn -noiopad
|
||||
cd distributed_ram_manual_syn # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:RAMB18E1
|
||||
97
tests/arch/xilinx/blockram.ys
Normal file
97
tests/arch/xilinx/blockram.ys
Normal file
|
|
@ -0,0 +1,97 @@
|
|||
### 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: -> RAMB18E1
|
||||
read_verilog ../common/blockram.v
|
||||
chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 1 sync_ram_sdp
|
||||
synth_xilinx -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RAMB18E1
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 18 sync_ram_sdp
|
||||
synth_xilinx -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RAMB18E1
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
chparam -set ADDRESS_WIDTH 14 -set DATA_WIDTH 1 sync_ram_sdp
|
||||
synth_xilinx -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RAMB18E1
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 sync_ram_sdp
|
||||
synth_xilinx -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RAMB18E1
|
||||
|
||||
# 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_xilinx -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 0 t:RAMB18E1
|
||||
select -assert-count 4 t:RAM128X1D
|
||||
|
||||
# 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_xilinx -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RAMB36E1
|
||||
|
||||
|
||||
### With parameters
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1
|
||||
setattr -set ram_style "block" m:memory
|
||||
synth_xilinx -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RAMB18E1
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1
|
||||
setattr -set ram_block 1 m:memory
|
||||
synth_xilinx -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RAMB18E1
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1
|
||||
setattr -set ram_style "dont_infer_a_ram_pretty_please" m:memory
|
||||
synth_xilinx -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 0 t:RAMB18E1
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1
|
||||
setattr -set logic_block 1 m:memory
|
||||
synth_xilinx -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 0 t:RAMB18E1
|
||||
|
||||
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_xilinx -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RAMB18E1
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/blockram.v
|
||||
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1
|
||||
setattr -set ram_block 1 m:memory
|
||||
synth_xilinx -top sync_ram_sdp -noiopad
|
||||
cd sync_ram_sdp
|
||||
select -assert-count 1 t:RAMB18E1
|
||||
34
tests/arch/xilinx/bug1460.ys
Normal file
34
tests/arch/xilinx/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_xilinx -noiopad
|
||||
cd register_file
|
||||
select -assert-count 32 t:RAM32M
|
||||
select -assert-none t:* t:BUFG %d t:RAM32M %d
|
||||
16
tests/arch/xilinx/bug1598.ys
Normal file
16
tests/arch/xilinx/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 +/xilinx/cells_sim.v synth_xilinx -abc9
|
||||
19
tests/arch/xilinx/bug1605.ys
Normal file
19
tests/arch/xilinx/bug1605.ys
Normal file
|
|
@ -0,0 +1,19 @@
|
|||
read_verilog <<EOT
|
||||
module top(inout io);
|
||||
wire in;
|
||||
wire t;
|
||||
wire o;
|
||||
|
||||
IOBUF IOBUF(
|
||||
.I(in),
|
||||
.T(t),
|
||||
.IO(io),
|
||||
.O(o)
|
||||
);
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
synth_xilinx
|
||||
cd top
|
||||
select -assert-count 1 t:IOBUF
|
||||
select -assert-none t:* t:IOBUF %d
|
||||
|
|
@ -2,13 +2,12 @@ read_verilog ../common/counter.v
|
|||
hierarchy -top top
|
||||
proc
|
||||
flatten
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -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 1 t:BUFG
|
||||
select -assert-count 8 t:FDCE
|
||||
select -assert-count 1 t:LUT1
|
||||
select -assert-count 7 t:MUXCY
|
||||
select -assert-count 8 t:XORCY
|
||||
select -assert-none t:BUFG t:FDCE t:LUT1 t:MUXCY t:XORCY %% t:* %D
|
||||
select -assert-count 1 t:INV
|
||||
select -assert-count 2 t:CARRY4
|
||||
select -assert-none t:BUFG t:FDCE t:INV t:CARRY4 %% t:* %D
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ design -save read
|
|||
|
||||
hierarchy -top dff
|
||||
proc
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -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:BUFG
|
||||
|
|
@ -15,7 +15,7 @@ select -assert-none t:BUFG t:FDRE %% t:* %D
|
|||
design -load read
|
||||
hierarchy -top dffe
|
||||
proc
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -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:BUFG
|
||||
|
|
|
|||
89
tests/arch/xilinx/dsp_cascade.ys
Normal file
89
tests/arch/xilinx/dsp_cascade.ys
Normal file
|
|
@ -0,0 +1,89 @@
|
|||
design -reset
|
||||
read_verilog <<EOT
|
||||
module cascade(input clk, input [4:0] a, input [4:0] b, output reg [9:0] o);
|
||||
reg [4:0] ar1, ar2, ar3, br1, br2, br3;
|
||||
reg [9:0] m, n;
|
||||
always @(posedge clk) begin
|
||||
ar1 <= a;
|
||||
ar2 <= ar1;
|
||||
ar3 <= ar2;
|
||||
br1 <= b;
|
||||
br2 <= br1;
|
||||
br3 <= br2;
|
||||
m <= ar1 * br1;
|
||||
n <= ar2 * br2 + m;
|
||||
o <= ar3 * br3 + n;
|
||||
end
|
||||
endmodule
|
||||
EOT
|
||||
proc
|
||||
design -save read
|
||||
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad
|
||||
design -load postopt
|
||||
cd cascade
|
||||
select -assert-count 3 t:DSP48E1
|
||||
select -assert-none t:DSP48E1 t:BUFG %% t:* %D
|
||||
# Very crude method of checking that DSP48E1.PCOUT -> DSP48E1.PCIN
|
||||
# (i.e. Take all DSP48E1s, expand to find all wires connected
|
||||
# to its PCOUT port, then remove all DSP48E1s from this
|
||||
# selection, then expand again to find all cells where
|
||||
# those wires are connected to the PCIN port, then remove
|
||||
# all wires from this selection, and lastly intersect
|
||||
# this selection with all DSP48E1 cells (to check that
|
||||
# the connected cells are indeed DSPs)
|
||||
select -assert-count 2 t:DSP48E1 %co:+[PCOUT] t:DSP48E1 %d %co:+[PCIN] w:* %d t:DSP48E1 %i
|
||||
|
||||
design -load read
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad
|
||||
design -load postopt
|
||||
cd cascade
|
||||
select -assert-count 3 t:DSP48A1
|
||||
select -assert-count 5 t:FDRE # No cascade for A input
|
||||
select -assert-none t:DSP48A1 t:BUFG t:FDRE %% t:* %D
|
||||
# Very crude method of checking that DSP48E1.PCOUT -> DSP48E1.PCIN
|
||||
# (see above for explanation)
|
||||
select -assert-count 2 t:DSP48A1 %co:+[PCOUT] t:DSP48A1 %d %co:+[PCIN] w:* %d t:DSP48A1 %i
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module cascade(input clk, input [4:0] a, input [4:0] b, output reg [9:0] o);
|
||||
reg [4:0] ar1, ar2, ar3, br1, br2, br3;
|
||||
reg [9:0] m;
|
||||
always @(posedge clk) begin
|
||||
ar1 <= a;
|
||||
ar2 <= ar1;
|
||||
ar3 <= ar2;
|
||||
br1 <= b;
|
||||
br2 <= br1;
|
||||
br3 <= br2;
|
||||
m <= ar2 * br2;
|
||||
o <= ar3 * br3 + m;
|
||||
end
|
||||
endmodule
|
||||
EOT
|
||||
proc
|
||||
design -save read
|
||||
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad
|
||||
design -load postopt
|
||||
cd cascade
|
||||
select -assert-count 2 t:DSP48E1
|
||||
select -assert-none t:DSP48E1 t:BUFG %% t:* %D
|
||||
# Very crude method of checking that DSP48E1.PCOUT -> DSP48E1.PCIN
|
||||
# (see above for explanation)
|
||||
select -assert-count 1 t:DSP48E1 %co:+[PCOUT] t:DSP48E1 %d %co:+[PCIN] w:* %d t:DSP48E1 %i
|
||||
|
||||
design -load read
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad
|
||||
design -load postopt
|
||||
cd cascade
|
||||
select -assert-count 2 t:DSP48A1
|
||||
select -assert-count 10 t:FDRE # Cannot cascade because first 'm' DSP
|
||||
# uses both B0REG and B1REG, whereas 'o'
|
||||
# only requires 1
|
||||
select -assert-none t:DSP48A1 t:BUFG t:FDRE %% t:* %D
|
||||
# Very crude method of checking that DSP48E1.PCOUT -> DSP48E1.PCIN
|
||||
# (see above for explanation)
|
||||
select -assert-count 1 t:DSP48A1 %co:+[PCOUT] t:DSP48A1 %d %co:+[PCIN] w:* %d t:DSP48A1 %i
|
||||
|
||||
69
tests/arch/xilinx/dsp_fastfir.ys
Normal file
69
tests/arch/xilinx/dsp_fastfir.ys
Normal file
|
|
@ -0,0 +1,69 @@
|
|||
read_verilog <<EOT
|
||||
// Citation https://github.com/ZipCPU/dspfilters/blob/master/rtl/fastfir.v
|
||||
module fastfir_dynamictaps(i_clk, i_reset, i_tap_wr, i_tap, i_ce, i_sample, o_result);
|
||||
wire [30:0] _00_;
|
||||
wire [23:0] _01_;
|
||||
wire [11:0] _02_;
|
||||
wire [30:0] _03_;
|
||||
wire [23:0] _04_;
|
||||
wire [30:0] _05_;
|
||||
wire [23:0] _06_;
|
||||
wire [30:0] _07_;
|
||||
wire [23:0] _08_;
|
||||
wire [11:0] _09_;
|
||||
wire [30:0] _10_;
|
||||
wire [23:0] _11_;
|
||||
wire [30:0] _12_;
|
||||
wire [23:0] _13_;
|
||||
wire [11:0] \fir.FILTER[0].tapk.delayed_sample ;
|
||||
reg [30:0] \fir.FILTER[0].tapk.o_acc = 31'h00000000;
|
||||
wire [11:0] \fir.FILTER[0].tapk.o_sample ;
|
||||
reg [23:0] \fir.FILTER[0].tapk.product ;
|
||||
reg [11:0] \fir.FILTER[0].tapk.tap = 12'h000;
|
||||
wire [11:0] \fir.FILTER[1].tapk.delayed_sample ;
|
||||
wire [30:0] \fir.FILTER[1].tapk.o_acc ;
|
||||
wire [11:0] \fir.FILTER[1].tapk.o_sample ;
|
||||
reg [23:0] \fir.FILTER[1].tapk.product ;
|
||||
reg [11:0] \fir.FILTER[1].tapk.tap = 12'h000;
|
||||
input i_ce;
|
||||
input i_clk;
|
||||
input i_reset;
|
||||
input [11:0] i_sample;
|
||||
input [11:0] i_tap;
|
||||
input i_tap_wr;
|
||||
output [30:0] o_result;
|
||||
reg [30:0] o_result;
|
||||
assign _03_ = 31'h00000000 + { \fir.FILTER[0].tapk.product [23], \fir.FILTER[0].tapk.product [23], \fir.FILTER[0].tapk.product [23], \fir.FILTER[0].tapk.product [23], \fir.FILTER[0].tapk.product [23], \fir.FILTER[0].tapk.product [23], \fir.FILTER[0].tapk.product [23], \fir.FILTER[0].tapk.product };
|
||||
assign _04_ = $signed(\fir.FILTER[0].tapk.tap ) * $signed(i_sample);
|
||||
always @(posedge i_clk)
|
||||
\fir.FILTER[0].tapk.tap <= _02_;
|
||||
always @(posedge i_clk)
|
||||
\fir.FILTER[0].tapk.o_acc <= _00_;
|
||||
always @(posedge i_clk)
|
||||
\fir.FILTER[0].tapk.product <= _01_;
|
||||
assign _02_ = i_tap_wr ? i_tap : \fir.FILTER[0].tapk.tap ;
|
||||
assign _05_ = i_ce ? _03_ : \fir.FILTER[0].tapk.o_acc ;
|
||||
assign _00_ = i_reset ? 31'h00000000 : _05_;
|
||||
assign _06_ = i_ce ? _04_ : \fir.FILTER[0].tapk.product ;
|
||||
assign _01_ = i_reset ? 24'h000000 : _06_;
|
||||
assign _10_ = \fir.FILTER[0].tapk.o_acc + { \fir.FILTER[1].tapk.product [23], \fir.FILTER[1].tapk.product [23], \fir.FILTER[1].tapk.product [23], \fir.FILTER[1].tapk.product [23], \fir.FILTER[1].tapk.product [23], \fir.FILTER[1].tapk.product [23], \fir.FILTER[1].tapk.product [23], \fir.FILTER[1].tapk.product };
|
||||
assign _11_ = $signed(\fir.FILTER[1].tapk.tap ) * $signed(i_sample);
|
||||
always @(posedge i_clk)
|
||||
\fir.FILTER[1].tapk.tap <= _09_;
|
||||
always @(posedge i_clk)
|
||||
o_result <= _07_;
|
||||
always @(posedge i_clk)
|
||||
\fir.FILTER[1].tapk.product <= _08_;
|
||||
assign _09_ = i_tap_wr ? \fir.FILTER[0].tapk.tap : \fir.FILTER[1].tapk.tap ;
|
||||
assign _12_ = i_ce ? _10_ : o_result;
|
||||
assign _07_ = i_reset ? 31'h00000000 : _12_;
|
||||
assign _13_ = i_ce ? _11_ : \fir.FILTER[1].tapk.product ;
|
||||
assign _08_ = i_reset ? 24'h000000 : _13_;
|
||||
assign \fir.FILTER[1].tapk.o_acc = o_result;
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
synth_xilinx -noiopad
|
||||
cd fastfir_dynamictaps
|
||||
select -assert-count 2 t:DSP48E1
|
||||
select -assert-none t:* t:DSP48E1 %d t:BUFG %d
|
||||
|
|
@ -3,16 +3,17 @@ hierarchy -top fsm
|
|||
proc
|
||||
flatten
|
||||
|
||||
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
|
||||
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -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 1 t:BUFG
|
||||
select -assert-count 5 t:FDRE
|
||||
select -assert-count 1 t:LUT3
|
||||
select -assert-count 2 t:LUT4
|
||||
select -assert-count 4 t:LUT6
|
||||
select -assert-none t:BUFG t:FDRE t:LUT3 t:LUT4 t:LUT6 %% t:* %D
|
||||
select -assert-count 4 t:FDRE
|
||||
select -assert-count 1 t:FDSE
|
||||
select -assert-count 1 t:LUT2
|
||||
select -assert-count 3 t:LUT5
|
||||
select -assert-count 1 t:LUT6
|
||||
select -assert-none t:BUFG t:FDRE t:FDSE t:LUT2 t:LUT5 t:LUT6 %% t:* %D
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ design -save read
|
|||
|
||||
hierarchy -top latchp
|
||||
proc
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd latchp # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:LDCE
|
||||
|
|
@ -14,19 +14,19 @@ select -assert-none t:LDCE %% t:* %D
|
|||
design -load read
|
||||
hierarchy -top latchn
|
||||
proc
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd latchn # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:LDCE
|
||||
select -assert-count 1 t:LUT1
|
||||
select -assert-count 1 t:INV
|
||||
|
||||
select -assert-none t:LDCE t:LUT1 %% t:* %D
|
||||
select -assert-none t:LDCE t:INV %% t:* %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top latchsr
|
||||
proc
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd latchsr # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:LDCE
|
||||
|
|
|
|||
|
|
@ -1,11 +1,11 @@
|
|||
read_verilog ../common/logic.v
|
||||
hierarchy -top top
|
||||
proc
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -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 1 t:INV
|
||||
select -assert-count 6 t:LUT2
|
||||
select -assert-count 2 t:LUT4
|
||||
select -assert-none t:LUT1 t:LUT2 t:LUT4 %% t:* %D
|
||||
select -assert-none t:INV t:LUT2 t:LUT4 %% t:* %D
|
||||
|
|
|
|||
137
tests/arch/xilinx/lutram.ys
Normal file
137
tests/arch/xilinx/lutram.ys
Normal file
|
|
@ -0,0 +1,137 @@
|
|||
#read_verilog ../common/lutram.v
|
||||
#hierarchy -top lutram_1w1r -chparam A_WIDTH 4
|
||||
#proc
|
||||
#memory -nomap
|
||||
#equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -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 1 t:BUFG
|
||||
#select -assert-count 8 t:FDRE
|
||||
#select -assert-count 8 t:RAM16X1D
|
||||
#select -assert-none t:BUFG t:FDRE t:RAM16X1D %% t:* %D
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r -chparam A_WIDTH 5
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -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 1 t:BUFG
|
||||
select -assert-count 8 t:FDRE
|
||||
select -assert-count 8 t:RAM32X1D
|
||||
select -assert-none t:BUFG t:FDRE t:RAM32X1D %% t:* %D
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w1r
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -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 1 t:BUFG
|
||||
select -assert-count 8 t:FDRE
|
||||
select -assert-count 8 t:RAM64X1D
|
||||
select -assert-none t:BUFG t:FDRE t:RAM64X1D %% t:* %D
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog ../common/lutram.v
|
||||
hierarchy -top lutram_1w3r
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -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 1 t:BUFG
|
||||
select -assert-count 24 t:FDRE
|
||||
select -assert-count 4 t:RAM32M
|
||||
select -assert-none t:BUFG t:FDRE t:RAM32M %% 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 +/xilinx/cells_sim.v synth_xilinx -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 1 t:BUFG
|
||||
select -assert-count 24 t:FDRE
|
||||
select -assert-count 8 t:RAM64M
|
||||
select -assert-none t:BUFG t:FDRE t:RAM64M %% 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 +/xilinx/cells_sim.v synth_xilinx -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 1 t:BUFG
|
||||
select -assert-count 6 t:FDRE
|
||||
select -assert-count 1 t:RAM32M
|
||||
select -assert-none t:BUFG t:FDRE t:RAM32M %% 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 +/xilinx/cells_sim.v synth_xilinx -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 1 t:BUFG
|
||||
select -assert-count 6 t:FDRE
|
||||
select -assert-count 2 t:RAM64M
|
||||
select -assert-none t:BUFG t:FDRE t:RAM64M %% t:* %D
|
||||
|
|
@ -1,3 +1,6 @@
|
|||
../../../yosys -qp "synth_xilinx -top macc2; rename -top macc2_uut" macc.v -o macc_uut.v
|
||||
../../../yosys -qp "synth_xilinx -top macc2; rename -top macc2_uut" -o macc_uut.v macc.v
|
||||
iverilog -o test_macc macc_tb.v macc_uut.v macc.v ../../../techlibs/xilinx/cells_sim.v
|
||||
vvp -N ./test_macc
|
||||
../../../yosys -qp "synth_xilinx -family xc6s -top macc2; rename -top macc2_uut" -o macc_uut.v macc.v
|
||||
iverilog -o test_macc macc_tb.v macc_uut.v macc.v ../../../techlibs/xilinx/cells_sim.v
|
||||
vvp -N ./test_macc
|
||||
|
|
|
|||
|
|
@ -3,8 +3,8 @@ design -save read
|
|||
|
||||
hierarchy -top macc
|
||||
proc
|
||||
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO
|
||||
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
|
||||
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
|
||||
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
|
|
@ -17,15 +17,16 @@ select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D
|
|||
design -load read
|
||||
hierarchy -top macc2
|
||||
proc
|
||||
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO
|
||||
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
|
||||
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
|
||||
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd macc2 # Constrain all select calls below inside the top module
|
||||
|
||||
select -assert-count 1 t:BUFG
|
||||
select -assert-count 1 t:DSP48E1
|
||||
select -assert-count 1 t:FDRE
|
||||
select -assert-count 1 t:LUT2
|
||||
select -assert-count 41 t:LUT3
|
||||
select -assert-count 40 t:LUT3
|
||||
select -assert-none t:BUFG t:DSP48E1 t:FDRE t:LUT2 t:LUT3 %% t:* %D
|
||||
|
|
|
|||
|
|
@ -1,17 +0,0 @@
|
|||
read_verilog ../common/memory.v
|
||||
hierarchy -top top
|
||||
proc
|
||||
memory -nomap
|
||||
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
|
||||
memory
|
||||
opt -full
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
|
||||
|
||||
design -load postopt
|
||||
cd top
|
||||
select -assert-count 1 t:BUFG
|
||||
select -assert-count 8 t:FDRE
|
||||
select -assert-count 8 t:RAM64X1D
|
||||
select -assert-none t:BUFG t:FDRE t:RAM64X1D %% t:* %D
|
||||
|
|
@ -1,9 +1,21 @@
|
|||
read_verilog ../common/mul.v
|
||||
hierarchy -top top
|
||||
proc
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -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:DSP48E1
|
||||
select -assert-none t:DSP48E1 %% t:* %D
|
||||
|
||||
design -reset
|
||||
|
||||
read_verilog ../common/mul.v
|
||||
hierarchy -top top
|
||||
proc
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -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:DSP48A1
|
||||
select -assert-none t:DSP48A1 %% t:* %D
|
||||
|
|
|
|||
|
|
@ -2,10 +2,24 @@ read_verilog mul_unsigned.v
|
|||
hierarchy -top mul_unsigned
|
||||
proc
|
||||
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -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:BUFG
|
||||
select -assert-count 1 t:DSP48E1
|
||||
select -assert-count 30 t:FDRE
|
||||
select -assert-none t:DSP48E1 t:FDRE t:BUFG %% t:* %D
|
||||
|
||||
design -reset
|
||||
|
||||
read_verilog mul_unsigned.v
|
||||
hierarchy -top mul_unsigned
|
||||
proc
|
||||
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -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:BUFG
|
||||
select -assert-count 1 t:DSP48A1
|
||||
select -assert-count 30 t:FDRE
|
||||
select -assert-none t:DSP48A1 t:FDRE t:BUFG %% t:* %D
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ design -save read
|
|||
|
||||
hierarchy -top mux2
|
||||
proc
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -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
|
||||
|
|
@ -14,7 +14,7 @@ select -assert-none t:LUT3 %% t:* %D
|
|||
design -load read
|
||||
hierarchy -top mux4
|
||||
proc
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -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
|
||||
|
|
@ -25,7 +25,7 @@ select -assert-none t:LUT6 %% t:* %D
|
|||
design -load read
|
||||
hierarchy -top mux8
|
||||
proc
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -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
|
||||
|
|
@ -37,9 +37,11 @@ select -assert-none t:LUT3 t:LUT6 %% t:* %D
|
|||
design -load read
|
||||
hierarchy -top mux16
|
||||
proc
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -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-count 5 t:LUT6
|
||||
select -assert-min 5 t:LUT6
|
||||
select -assert-max 7 t:LUT6
|
||||
select -assert-max 2 t:MUXF7
|
||||
|
||||
select -assert-none t:LUT6 %% t:* %D
|
||||
select -assert-none t:LUT6 t:MUXF7 %% t:* %D
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@ read_verilog ../common/shifter.v
|
|||
hierarchy -top top
|
||||
proc
|
||||
flatten
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
|
||||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -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
|
||||
|
||||
|
|
|
|||
5
tests/arch/xilinx/tribuf.sh
Normal file
5
tests/arch/xilinx/tribuf.sh
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
! ../../../yosys ../common/tribuf.v -qp "synth_xilinx"
|
||||
../../../yosys ../common/tribuf.v -qp "synth_xilinx -iopad; \
|
||||
select -assert-count 2 t:IBUF; \
|
||||
select -assert-count 1 t:INV; \
|
||||
select -assert-count 1 t:OBUFT"
|
||||
|
|
@ -7,6 +7,7 @@ synth
|
|||
equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd tristate # Constrain all select calls below inside the top module
|
||||
# TODO :: Tristate logic not yet supported; see https://github.com/YosysHQ/yosys/issues/1225
|
||||
select -assert-count 1 t:$_TBUF_
|
||||
select -assert-none t:$_TBUF_ %% t:* %D
|
||||
select -assert-count 2 t:IBUF
|
||||
select -assert-count 1 t:INV
|
||||
select -assert-count 1 t:OBUFT
|
||||
select -assert-none t:IBUF t:INV t:OBUFT %% t:* %D
|
||||
|
|
|
|||
216
tests/arch/xilinx/xilinx_dffopt.ys
Normal file
216
tests/arch/xilinx/xilinx_dffopt.ys
Normal file
|
|
@ -0,0 +1,216 @@
|
|||
read_verilog << EOT
|
||||
|
||||
// FDRE, mergeable CE and R.
|
||||
|
||||
module t0 (...);
|
||||
input wire clk;
|
||||
input wire [7:0] i;
|
||||
output wire [7:0] o;
|
||||
|
||||
wire [7:0] tmp ;
|
||||
|
||||
LUT2 #(.INIT(4'h6)) lut0 (.I0(i[0]), .I1(i[1]), .O(tmp[0]));
|
||||
LUT2 #(.INIT(4'h6)) lut1 (.I0(i[1]), .I1(i[2]), .O(tmp[1]));
|
||||
LUT2 #(.INIT(4'h6)) lut2 (.I0(i[3]), .I1(i[4]), .O(tmp[2]));
|
||||
|
||||
FDRE ff (.D(tmp[0]), .CE(tmp[1]), .R(tmp[2]), .Q(o[0]));
|
||||
|
||||
endmodule
|
||||
|
||||
EOT
|
||||
|
||||
design -save t0
|
||||
|
||||
equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt
|
||||
design -load postopt
|
||||
clean
|
||||
|
||||
select -assert-count 1 t:FDRE
|
||||
select -assert-count 1 t:LUT6
|
||||
select -assert-count 3 t:LUT2
|
||||
select -assert-none t:FDRE t:LUT6 t:LUT2 %% t:* %D
|
||||
|
||||
design -load t0
|
||||
|
||||
equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt -lut4
|
||||
design -load postopt
|
||||
clean
|
||||
|
||||
select -assert-count 1 t:FDRE
|
||||
select -assert-count 1 t:LUT4
|
||||
select -assert-count 3 t:LUT2
|
||||
select -assert-none t:FDRE t:LUT4 t:LUT2 %% t:* %D
|
||||
|
||||
design -reset
|
||||
|
||||
|
||||
read_verilog << EOT
|
||||
|
||||
// FDSE, mergeable CE and S, inversions.
|
||||
|
||||
module t0 (...);
|
||||
input wire clk;
|
||||
input wire [7:0] i;
|
||||
output wire [7:0] o;
|
||||
|
||||
wire [7:0] tmp ;
|
||||
|
||||
LUT2 #(.INIT(4'h6)) lut0 (.I0(i[0]), .I1(i[1]), .O(tmp[0]));
|
||||
LUT2 #(.INIT(4'h6)) lut1 (.I0(i[1]), .I1(i[2]), .O(tmp[1]));
|
||||
LUT2 #(.INIT(4'h6)) lut2 (.I0(i[3]), .I1(i[4]), .O(tmp[2]));
|
||||
|
||||
FDSE #(.IS_D_INVERTED(1'b1), .IS_S_INVERTED(1'b1)) ff (.D(tmp[0]), .CE(tmp[1]), .S(tmp[2]), .Q(o[0]));
|
||||
|
||||
endmodule
|
||||
|
||||
EOT
|
||||
|
||||
design -save t0
|
||||
|
||||
equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt
|
||||
design -load postopt
|
||||
clean
|
||||
|
||||
select -assert-count 1 t:FDSE
|
||||
select -assert-count 1 t:LUT6
|
||||
select -assert-count 3 t:LUT2
|
||||
select -assert-none t:FDSE t:LUT6 t:LUT2 %% t:* %D
|
||||
|
||||
design -load t0
|
||||
|
||||
equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt -lut4
|
||||
design -load postopt
|
||||
clean
|
||||
|
||||
select -assert-count 1 t:FDSE
|
||||
select -assert-count 1 t:LUT4
|
||||
select -assert-count 3 t:LUT2
|
||||
select -assert-none t:FDSE t:LUT4 t:LUT2 %% t:* %D
|
||||
|
||||
design -reset
|
||||
|
||||
|
||||
read_verilog << EOT
|
||||
|
||||
// FDCE, mergeable CE.
|
||||
|
||||
module t0 (...);
|
||||
input wire clk;
|
||||
input wire [7:0] i;
|
||||
output wire [7:0] o;
|
||||
|
||||
wire [7:0] tmp ;
|
||||
|
||||
LUT2 #(.INIT(4'h6)) lut0 (.I0(i[0]), .I1(i[1]), .O(tmp[0]));
|
||||
LUT2 #(.INIT(4'h6)) lut1 (.I0(i[1]), .I1(i[2]), .O(tmp[1]));
|
||||
LUT2 #(.INIT(4'h6)) lut2 (.I0(i[3]), .I1(i[4]), .O(tmp[2]));
|
||||
|
||||
FDCE ff (.D(tmp[0]), .CE(tmp[1]), .CLR(tmp[2]), .Q(o[0]));
|
||||
|
||||
endmodule
|
||||
|
||||
EOT
|
||||
|
||||
design -save t0
|
||||
|
||||
equiv_opt -async2sync -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt
|
||||
design -load postopt
|
||||
clean
|
||||
|
||||
select -assert-count 1 t:FDCE
|
||||
select -assert-count 1 t:LUT4
|
||||
select -assert-count 3 t:LUT2
|
||||
select -assert-none t:FDCE t:LUT4 t:LUT2 %% t:* %D
|
||||
|
||||
design -reset
|
||||
|
||||
|
||||
read_verilog << EOT
|
||||
|
||||
// FDSE, mergeable CE and S, but CE only not worth it.
|
||||
|
||||
module t0 (...);
|
||||
input wire clk;
|
||||
input wire [7:0] i;
|
||||
output wire [7:0] o;
|
||||
|
||||
wire [7:0] tmp ;
|
||||
|
||||
LUT2 #(.INIT(4'h6)) lut0 (.I0(i[0]), .I1(i[1]), .O(tmp[0]));
|
||||
LUT2 #(.INIT(4'h6)) lut1 (.I0(i[1]), .I1(i[2]), .O(tmp[1]));
|
||||
|
||||
FDSE ff (.D(tmp[0]), .CE(i[7]), .S(tmp[1]), .Q(o[0]));
|
||||
|
||||
endmodule
|
||||
|
||||
EOT
|
||||
|
||||
design -save t0
|
||||
|
||||
equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt
|
||||
design -load postopt
|
||||
clean
|
||||
|
||||
select -assert-count 1 t:FDSE
|
||||
select -assert-count 1 t:LUT5
|
||||
select -assert-count 2 t:LUT2
|
||||
select -assert-none t:FDSE t:LUT5 t:LUT2 %% t:* %D
|
||||
|
||||
design -load t0
|
||||
|
||||
equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt -lut4
|
||||
design -load postopt
|
||||
clean
|
||||
|
||||
select -assert-count 1 t:FDSE
|
||||
select -assert-count 2 t:LUT2
|
||||
select -assert-none t:FDSE t:LUT2 %% t:* %D
|
||||
|
||||
design -reset
|
||||
|
||||
|
||||
read_verilog << EOT
|
||||
|
||||
// FDRSE, mergeable CE, S, R.
|
||||
|
||||
module t0 (...);
|
||||
input wire clk;
|
||||
input wire [7:0] i;
|
||||
output wire [7:0] o;
|
||||
|
||||
wire [7:0] tmp ;
|
||||
|
||||
LUT2 #(.INIT(4'h6)) lut0 (.I0(i[0]), .I1(i[1]), .O(tmp[0]));
|
||||
LUT2 #(.INIT(4'h6)) lut1 (.I0(i[1]), .I1(i[2]), .O(tmp[1]));
|
||||
LUT2 #(.INIT(4'h8)) lut2 (.I0(i[2]), .I1(i[0]), .O(tmp[2]));
|
||||
LUT2 #(.INIT(4'h6)) lut3 (.I0(i[3]), .I1(i[4]), .O(tmp[3]));
|
||||
|
||||
FDRSE ff (.D(tmp[0]), .CE(tmp[1]), .S(tmp[2]), .R(tmp[3]), .Q(o[0]));
|
||||
|
||||
endmodule
|
||||
|
||||
EOT
|
||||
|
||||
design -save t0
|
||||
|
||||
equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt
|
||||
design -load postopt
|
||||
clean
|
||||
|
||||
select -assert-count 1 t:FDRSE
|
||||
select -assert-count 1 t:LUT6
|
||||
select -assert-count 4 t:LUT2
|
||||
select -assert-none t:FDRSE t:LUT6 t:LUT2 %% t:* %D
|
||||
|
||||
design -load t0
|
||||
|
||||
equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt -lut4
|
||||
design -load postopt
|
||||
clean
|
||||
|
||||
select -assert-count 1 t:FDRSE
|
||||
select -assert-count 1 t:LUT4
|
||||
select -assert-count 4 t:LUT2
|
||||
select -assert-none t:FDRSE t:LUT4 t:LUT2 %% t:* %D
|
||||
|
||||
design -reset
|
||||
13
tests/arch/xilinx/xilinx_dffopt_blacklist.txt
Normal file
13
tests/arch/xilinx/xilinx_dffopt_blacklist.txt
Normal file
|
|
@ -0,0 +1,13 @@
|
|||
lut0
|
||||
lut1
|
||||
lut2
|
||||
lut3
|
||||
ff
|
||||
ff.D
|
||||
ff.R
|
||||
ff.S
|
||||
ff.CE
|
||||
ff.d
|
||||
ff.r
|
||||
ff.s
|
||||
ff.ce
|
||||
11
tests/arch/xilinx/xilinx_dsp.ys
Normal file
11
tests/arch/xilinx/xilinx_dsp.ys
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
read_verilog <<EOT
|
||||
module top(input [24:0] a, input [17:0] b, output [42:0] o1, o2, o5);
|
||||
DSP48E1 m1 (.A(a), .B(16'd1234), .P(o1));
|
||||
assign o2 = a * 16'd0;
|
||||
wire [42:0] o3, o4;
|
||||
DSP48E1 m2 (.A(a), .B(b), .P(o3));
|
||||
assign o4 = a * b;
|
||||
DSP48E1 m3 (.A(a), .B(b), .P(o5));
|
||||
endmodule
|
||||
EOT
|
||||
xilinx_dsp
|
||||
13
tests/opt/bug1525.ys
Normal file
13
tests/opt/bug1525.ys
Normal file
|
|
@ -0,0 +1,13 @@
|
|||
read_verilog << EOF
|
||||
module top(...);
|
||||
input A1, A2, B, S;
|
||||
output O;
|
||||
|
||||
assign O = S ? (A1 & B) : (A2 & B);
|
||||
|
||||
endmodule
|
||||
EOF
|
||||
|
||||
simplemap
|
||||
opt_share
|
||||
dump
|
||||
|
|
@ -2,3 +2,14 @@ read_verilog -sv initval.v
|
|||
proc;;
|
||||
|
||||
sat -seq 10 -prove-asserts
|
||||
|
||||
design -reset
|
||||
read_verilog -icells <<EOT
|
||||
module top(input clk, i, output [1:0] o);
|
||||
(* init = 2'bx0 *)
|
||||
wire [1:0] o;
|
||||
assign o[1] = o[0];
|
||||
$_DFF_P_ dff (.C(clk), .D(i), .Q(o[0]));
|
||||
endmodule
|
||||
EOT
|
||||
sat -seq 1
|
||||
|
|
|
|||
|
|
@ -7,11 +7,9 @@ module MyMem #(
|
|||
input Clk_i,
|
||||
input [AddrWidth-1:0] Addr_i,
|
||||
input [DataWidth-1:0] Data_i,
|
||||
output [DataWidth-1:0] Data_o,
|
||||
output reg [DataWidth-1:0] Data_o,
|
||||
input WR_i);
|
||||
|
||||
reg [DataWidth-1:0] Data_o;
|
||||
|
||||
localparam Size = 2**AddrWidth;
|
||||
|
||||
(* mem2reg *)
|
||||
|
|
|
|||
|
|
@ -213,17 +213,11 @@ module arbiter (clk, rst, request, acknowledge, grant, grant_valid, grant_encode
|
|||
input rst;
|
||||
endmodule
|
||||
|
||||
(* abc_box_id=1 *)
|
||||
(* abc9_box_id=1, whitebox *)
|
||||
module MUXF8(input I0, I1, S, output O);
|
||||
endmodule
|
||||
|
||||
// Citation: https://github.com/alexforencich/verilog-ethernet
|
||||
// TODO: yosys -p "synth_xilinx -abc9 -top abc9_test022" abc9.v -q
|
||||
// returns before b4321a31
|
||||
// Warning: Wire abc9_test022.\m_eth_payload_axis_tkeep [7] is used but has no
|
||||
// driver.
|
||||
// Warning: Wire abc9_test022.\m_eth_payload_axis_tkeep [3] is used but has no
|
||||
// driver.
|
||||
module abc9_test022
|
||||
(
|
||||
input wire clk,
|
||||
|
|
@ -237,9 +231,6 @@ module abc9_test022
|
|||
endmodule
|
||||
|
||||
// Citation: https://github.com/riscv/riscv-bitmanip
|
||||
// TODO: yosys -p "synth_xilinx -abc9 -top abc9_test023" abc9.v -q
|
||||
// returns before 14233843
|
||||
// Warning: Wire abc9_test023.\dout [1] is used but has no driver.
|
||||
module abc9_test023 #(
|
||||
parameter integer N = 2,
|
||||
parameter integer M = 2
|
||||
|
|
@ -267,3 +258,52 @@ module abc9_test026(output [3:0] o, p);
|
|||
assign o = { 1'b1, 1'bx };
|
||||
assign p = { 1'b1, 1'bx, 1'b0 };
|
||||
endmodule
|
||||
|
||||
module abc9_test030(input [3:0] d, input en, output reg [3:0] q);
|
||||
always @*
|
||||
if (en)
|
||||
q <= d;
|
||||
endmodule
|
||||
|
||||
module abc9_test031(input clk1, clk2, d, output reg q1, q2);
|
||||
always @(posedge clk1) q1 <= d;
|
||||
always @(negedge clk2) q2 <= q1;
|
||||
endmodule
|
||||
|
||||
module abc9_test032(input clk, d, r, output reg q);
|
||||
always @(posedge clk or posedge r)
|
||||
if (r) q <= 1'b0;
|
||||
else q <= d;
|
||||
endmodule
|
||||
|
||||
module abc9_test033(input clk, d, r, output reg q);
|
||||
always @(negedge clk or posedge r)
|
||||
if (r) q <= 1'b1;
|
||||
else q <= d;
|
||||
endmodule
|
||||
|
||||
module abc9_test034(input clk, d, output reg q1, q2);
|
||||
always @(posedge clk) q1 <= d;
|
||||
always @(posedge clk) q2 <= q1;
|
||||
endmodule
|
||||
|
||||
module abc9_test035(input clk, d, output reg [1:0] q);
|
||||
always @(posedge clk) q[0] <= d;
|
||||
always @(negedge clk) q[1] <= q[0];
|
||||
endmodule
|
||||
|
||||
module abc9_test036(input A, B, S, output [1:0] O);
|
||||
(* keep *)
|
||||
MUXF8 m (
|
||||
.I0(I0),
|
||||
.I1(I1),
|
||||
.O(O[0]),
|
||||
.S(S)
|
||||
);
|
||||
MUXF8 m2 (
|
||||
.I0(I0),
|
||||
.I1(I1),
|
||||
.O(O[1]),
|
||||
.S(S)
|
||||
);
|
||||
endmodule
|
||||
|
|
|
|||
|
|
@ -20,10 +20,13 @@ fi
|
|||
cp ../simple/*.v .
|
||||
cp ../simple/*.sv .
|
||||
DOLLAR='?'
|
||||
exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v EXTRA_FLAGS="-n 300 -p '\
|
||||
exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v *.sv EXTRA_FLAGS="-n 300 -p '\
|
||||
hierarchy; \
|
||||
synth -run coarse; \
|
||||
opt -full; \
|
||||
techmap; abc9 -lut 4 -box ../abc.box; \
|
||||
techmap; \
|
||||
abc9 -lut 4 -box ../abc.box; \
|
||||
clean; \
|
||||
check -assert; \
|
||||
select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%'"
|
||||
select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%; \
|
||||
setattr -mod -unset whitebox'"
|
||||
|
|
|
|||
81
tests/techmap/abc9.ys
Normal file
81
tests/techmap/abc9.ys
Normal file
|
|
@ -0,0 +1,81 @@
|
|||
read_verilog <<EOT
|
||||
`define N 256
|
||||
module top(input [`N-1:0] a, output o);
|
||||
wire [`N-2:0] w;
|
||||
assign w[0] = a[0] & a[1];
|
||||
genvar i;
|
||||
generate for (i = 1; i < `N-1; i++)
|
||||
assign w[i] = w[i-1] & a[i+1];
|
||||
endgenerate
|
||||
assign o = w[`N-2];
|
||||
endmodule
|
||||
EOT
|
||||
simplemap
|
||||
dump
|
||||
design -save gold
|
||||
|
||||
abc9 -lut 4
|
||||
|
||||
design -load gold
|
||||
abc9 -lut 4 -fast
|
||||
|
||||
design -load gold
|
||||
scratchpad -copy abc9.script.default.area abc9.script
|
||||
abc9 -lut 4
|
||||
|
||||
design -load gold
|
||||
scratchpad -copy abc9.script.default.fast abc9.script
|
||||
abc9 -lut 4
|
||||
|
||||
design -load gold
|
||||
scratchpad -copy abc9.script.flow abc9.script
|
||||
abc9 -lut 4
|
||||
|
||||
design -load gold
|
||||
scratchpad -copy abc9.script.flow2 abc9.script
|
||||
abc9 -lut 4
|
||||
|
||||
design -load gold
|
||||
scratchpad -copy abc9.script.flow3 abc9.script
|
||||
abc9 -lut 4
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input a, b, output o);
|
||||
(* keep *) wire w = a & b;
|
||||
assign o = ~w;
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
simplemap
|
||||
equiv_opt -assert abc9 -lut 4
|
||||
design -load postopt
|
||||
select -assert-count 2 t:$lut
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog -icells <<EOT
|
||||
module top(input a, b, output o);
|
||||
wire w;
|
||||
(* keep *) $_AND_ gate (.Y(w), .A(a), .B(b));
|
||||
assign o = ~w;
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
simplemap
|
||||
equiv_opt -assert abc9 -lut 4
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$lut
|
||||
select -assert-count 1 t:$_AND_
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog -icells <<EOT
|
||||
module top(input a, b, output o);
|
||||
assign o = ~(a & b);
|
||||
endmodule
|
||||
EOT
|
||||
abc9 -lut 4
|
||||
clean
|
||||
select -assert-count 1 t:$lut
|
||||
select -assert-none t:$lut t:* %D
|
||||
|
|
@ -4,6 +4,7 @@ module dff ((* clkbuf_sink *) input clk, input d, output q); endmodule
|
|||
module dffe ((* clkbuf_sink *) input c, input d, e, output q); endmodule
|
||||
module latch (input e, d, output q); endmodule
|
||||
module clkgen (output o); endmodule
|
||||
module inv ((* clkbuf_inv = "i" *) output o, input i); endmodule
|
||||
|
||||
module top(input clk1, clk2, clk3, d, e, output [4:0] q);
|
||||
wire clk4, clk5, clk6;
|
||||
|
|
@ -17,12 +18,18 @@ dff s6 (.clk(clk6), .d(d), .q(q[4]));
|
|||
endmodule
|
||||
|
||||
module sub(output sclk4, output sclk5, output sclk6, input sd, output sq);
|
||||
wire sclk7, sclk8, sclk9;
|
||||
wire siq;
|
||||
wire tmp;
|
||||
clkgen s7(.o(sclk4));
|
||||
clkgen s8(.o(sclk5));
|
||||
clkgen s9(.o(tmp));
|
||||
clkbuf s10(.i(tmp), .o(sclk6));
|
||||
dff s11(.clk(sclk4), .d(sd), .q(sq));
|
||||
clkbuf s10(.i(tmp), .o(sclk7));
|
||||
dff s11(.clk(sclk4), .d(sd), .q(siq));
|
||||
inv s15(.i(sclk7), .o(sclk6));
|
||||
clkgen s12(.o(sclk8));
|
||||
inv s13(.o(sclk9), .i(sclk8));
|
||||
dff s14(.clk(sclk9), .d(siq), .q(sq));
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
|
|
@ -34,7 +41,7 @@ design -save ref
|
|||
design -load ref
|
||||
clkbufmap -buf clkbuf o:i
|
||||
select -assert-count 3 top/t:clkbuf
|
||||
select -assert-count 2 sub/t:clkbuf
|
||||
select -assert-count 3 sub/t:clkbuf
|
||||
select -set clk1 w:clk1 %a %co t:clkbuf %i # Find 'clk1' fanouts that are 'clkbuf'
|
||||
select -assert-count 1 @clk1 # Check there is one such fanout
|
||||
select -assert-count 1 @clk1 %x:+[o] %co c:s* %i # Check that the 'o' of that clkbuf drives one fanout
|
||||
|
|
@ -51,6 +58,10 @@ select -set sclk4 w:sclk4 %a %ci t:clkbuf %i
|
|||
select -assert-count 1 @sclk4
|
||||
select -assert-count 1 @sclk4 %x:+[o] %co c:s11 %i
|
||||
select -assert-count 1 @sclk4 %x:+[i] %ci c:s7 %i
|
||||
select -set sclk8 w:sclk8 %a %ci t:clkbuf %i
|
||||
select -assert-count 1 @sclk8
|
||||
select -assert-count 1 @sclk8 %x:+[o] %co c:s13 %i
|
||||
select -assert-count 1 @sclk8 %x:+[i] %ci c:s12 %i
|
||||
|
||||
# ----------------------
|
||||
|
||||
|
|
@ -72,7 +83,7 @@ setattr -set clkbuf_inhibit 1 w:clk1
|
|||
setattr -set buffer_type "bufg" w:clk2
|
||||
clkbufmap -buf clkbuf o:i w:* a:buffer_type=none a:buffer_type=bufr %u %d
|
||||
select -assert-count 3 top/t:clkbuf
|
||||
select -assert-count 2 sub/t:clkbuf
|
||||
select -assert-count 3 sub/t:clkbuf
|
||||
select -set clk1 w:clk1 %a %co t:clkbuf %i # Find 'clk1' fanouts that are 'clkbuf'
|
||||
select -assert-count 1 @clk1 # Check there is one such fanout
|
||||
select -assert-count 1 @clk1 %x:+[o] %co c:s* %i # Check that the 'o' of that clkbuf drives one fanout
|
||||
|
|
@ -93,4 +104,4 @@ clkbufmap -buf clkbuf o:i w:* a:buffer_type=none a:buffer_type=bufr %u %d
|
|||
select -assert-count 0 w:clk1 %a %co t:clkbuf %i
|
||||
select -assert-count 0 w:clk2 %a %co t:clkbuf %i
|
||||
select -assert-count 0 top/t:clkbuf
|
||||
select -assert-count 1 sub/t:clkbuf
|
||||
select -assert-count 2 sub/t:clkbuf
|
||||
|
|
|
|||
122
tests/techmap/iopadmap.ys
Normal file
122
tests/techmap/iopadmap.ys
Normal file
|
|
@ -0,0 +1,122 @@
|
|||
read_verilog << EOT
|
||||
module ibuf ((* iopad_external_pin *) input i, output o); endmodule
|
||||
module obuf (input i, (* iopad_external_pin *) output o); endmodule
|
||||
module obuft (input i, input oe, (* iopad_external_pin *) output o); endmodule
|
||||
module iobuf (input i, input oe, output o, (* iopad_external_pin *) inout io); endmodule
|
||||
|
||||
module a(input i, output o);
|
||||
assign o = i;
|
||||
endmodule
|
||||
|
||||
module b(input i, output o);
|
||||
assign o = i;
|
||||
ibuf b (.i(i), .o(o));
|
||||
endmodule
|
||||
|
||||
module c(input i, output o);
|
||||
obuf b (.i(i), .o(o));
|
||||
endmodule
|
||||
|
||||
module d(input i, oe, output o, o2, o3);
|
||||
assign o = oe ? i : 1'bz;
|
||||
assign o2 = o;
|
||||
assign o3 = ~o;
|
||||
endmodule
|
||||
|
||||
module e(input i, oe, inout io, output o2, o3);
|
||||
assign io = oe ? i : 1'bz;
|
||||
assign o2 = io;
|
||||
assign o3 = ~io;
|
||||
endmodule
|
||||
|
||||
module f(output o, o2);
|
||||
assign o = 1'bz;
|
||||
endmodule
|
||||
|
||||
module g(inout io, output o);
|
||||
assign o = io;
|
||||
endmodule
|
||||
|
||||
module h(inout io, output o, input i);
|
||||
assign io = i;
|
||||
assign o = io;
|
||||
endmodule
|
||||
|
||||
EOT
|
||||
|
||||
opt_clean
|
||||
tribuf
|
||||
simplemap
|
||||
iopadmap -bits -inpad ibuf o:i -outpad obuf i:o -toutpad obuft oe:i:o -tinoutpad iobuf oe:o:i:io
|
||||
opt_clean
|
||||
|
||||
select -assert-count 1 a/t:ibuf
|
||||
select -assert-count 1 a/t:obuf
|
||||
select -set ib w:i %a %co a/t:ibuf %i
|
||||
select -set ob w:o %a %ci a/t:obuf %i
|
||||
select -assert-count 1 @ib
|
||||
select -assert-count 1 @ob
|
||||
select -assert-count 1 @ib %co %co @ob %i
|
||||
|
||||
select -assert-count 1 b/t:ibuf
|
||||
select -assert-count 1 b/t:obuf
|
||||
select -set ib w:i %a %co b/t:ibuf %i
|
||||
select -set ob w:o %a %ci b/t:obuf %i
|
||||
select -assert-count 1 @ib
|
||||
select -assert-count 1 @ob
|
||||
select -assert-count 1 @ib %co %co @ob %i
|
||||
|
||||
select -assert-count 1 c/t:ibuf
|
||||
select -assert-count 1 c/t:obuf
|
||||
select -set ib w:i %a %co c/t:ibuf %i
|
||||
select -set ob w:o %a %ci c/t:obuf %i
|
||||
select -assert-count 1 @ib
|
||||
select -assert-count 1 @ob
|
||||
select -assert-count 1 @ib %co %co @ob %i
|
||||
|
||||
select -assert-count 2 d/t:ibuf
|
||||
select -assert-count 2 d/t:obuf
|
||||
select -assert-count 1 d/t:obuft
|
||||
select -set ib w:i %a %co d/t:ibuf %i
|
||||
select -set oeb w:oe %a %co d/t:ibuf %i
|
||||
select -set ob w:o %a %ci d/t:obuft %i
|
||||
select -set o2b w:o2 %a %ci d/t:obuf %i
|
||||
select -set o3b w:o3 %a %ci d/t:obuf %i
|
||||
select -assert-count 1 @ib
|
||||
select -assert-count 1 @oeb
|
||||
select -assert-count 1 @ob
|
||||
select -assert-count 1 @o2b
|
||||
select -assert-count 1 @o3b
|
||||
select -assert-count 1 @ib %co %co @ob %i
|
||||
select -assert-count 1 @oeb %co %co @ob %i
|
||||
select -assert-count 1 @ib %co %co @o2b %i
|
||||
select -assert-count 1 @ib %co %co t:$_NOT_ %i
|
||||
select -assert-count 1 @o3b %ci %ci t:$_NOT_ %i
|
||||
|
||||
select -assert-count 2 e/t:ibuf
|
||||
select -assert-count 2 e/t:obuf
|
||||
select -assert-count 1 e/t:iobuf
|
||||
select -set ib w:i %a %co e/t:ibuf %i
|
||||
select -set oeb w:oe %a %co e/t:ibuf %i
|
||||
select -set iob w:io %a %ci e/t:iobuf %i
|
||||
select -set o2b w:o2 %a %ci e/t:obuf %i
|
||||
select -set o3b w:o3 %a %ci e/t:obuf %i
|
||||
select -assert-count 1 @ib
|
||||
select -assert-count 1 @oeb
|
||||
select -assert-count 1 @iob
|
||||
select -assert-count 1 @o2b
|
||||
select -assert-count 1 @o3b
|
||||
select -assert-count 1 @ib %co %co @iob %i
|
||||
select -assert-count 1 @oeb %co %co @iob %i
|
||||
select -assert-count 1 @iob %co %co @o2b %i
|
||||
select -assert-count 1 @iob %co %co t:$_NOT_ %i
|
||||
select -assert-count 1 @o3b %ci %ci t:$_NOT_ %i
|
||||
|
||||
select -assert-count 2 f/t:obuft
|
||||
|
||||
select -assert-count 1 g/t:obuf
|
||||
select -assert-count 1 g/t:iobuf
|
||||
|
||||
select -assert-count 1 h/t:ibuf
|
||||
select -assert-count 1 h/t:iobuf
|
||||
select -assert-count 1 h/t:obuf
|
||||
|
|
@ -9,3 +9,10 @@ wire w;
|
|||
unknown u(~i, w);
|
||||
unknown2 u2(w, o);
|
||||
endmodule
|
||||
|
||||
module abc9_test032(input clk, d, r, output reg q);
|
||||
initial q = 1'b0;
|
||||
always @(negedge clk or negedge r)
|
||||
if (!r) q <= 1'b0;
|
||||
else q <= d;
|
||||
endmodule
|
||||
|
|
|
|||
|
|
@ -14,6 +14,7 @@ design -import gate -as gate
|
|||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -show-ports miter
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top abc9_test028
|
||||
proc
|
||||
|
|
@ -22,3 +23,33 @@ abc9 -lut 4
|
|||
select -assert-count 1 t:$lut r:LUT=2'b01 r:WIDTH=1 %i %i
|
||||
select -assert-count 1 t:unknown
|
||||
select -assert-none t:$lut t:unknown %% t: %D
|
||||
|
||||
|
||||
design -load read
|
||||
hierarchy -top abc9_test032
|
||||
proc
|
||||
clk2fflogic
|
||||
design -save gold
|
||||
|
||||
abc9 -lut 4
|
||||
check
|
||||
design -stash gate
|
||||
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -seq 10 -verify -prove-asserts -show-ports miter
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog -icells <<EOT
|
||||
module abc9_test036(input clk, d, output q);
|
||||
(* keep *) reg w;
|
||||
$__ABC9_FF_ ff(.D(d), .Q(w));
|
||||
wire \ff.clock = clk;
|
||||
wire \ff.init = 1'b0;
|
||||
assign q = w;
|
||||
endmodule
|
||||
EOT
|
||||
abc9 -lut 4 -dff
|
||||
|
|
|
|||
19
tests/various/autoname.ys
Normal file
19
tests/various/autoname.ys
Normal file
|
|
@ -0,0 +1,19 @@
|
|||
read_ilang <<EOT
|
||||
autoidx 2
|
||||
module \top
|
||||
wire output 3 $y
|
||||
wire input 1 \a
|
||||
wire input 2 \b
|
||||
cell $and \b_$and_B
|
||||
parameter \A_SIGNED 0
|
||||
parameter \A_WIDTH 1
|
||||
parameter \B_SIGNED 0
|
||||
parameter \B_WIDTH 1
|
||||
parameter \Y_WIDTH 1
|
||||
connect \A \a
|
||||
connect \B \b
|
||||
connect \Y $y
|
||||
end
|
||||
end
|
||||
EOT
|
||||
autoname
|
||||
34
tests/various/bug1531.ys
Normal file
34
tests/various/bug1531.ys
Normal file
|
|
@ -0,0 +1,34 @@
|
|||
read_verilog <<EOT
|
||||
module top (y, clk, w);
|
||||
output reg y = 1'b0;
|
||||
input clk, w;
|
||||
reg [1:0] i = 2'b00;
|
||||
always @(posedge clk)
|
||||
// If the constant below is set to 2'b00, the correct output is generated.
|
||||
// vvvv
|
||||
for (i = 1'b0; i < 2'b01; i = i + 2'b01)
|
||||
y <= w || i[1:1];
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
synth
|
||||
design -stash gate
|
||||
|
||||
read_verilog <<EOT
|
||||
module gold (y, clk, w);
|
||||
input clk;
|
||||
wire [1:0] i;
|
||||
input w;
|
||||
output y;
|
||||
reg y = 1'h0;
|
||||
always @(posedge clk)
|
||||
y <= w;
|
||||
assign i = 2'h0;
|
||||
endmodule
|
||||
EOT
|
||||
proc gold
|
||||
|
||||
design -import gate -as gate
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -seq 10 -verify -prove-asserts -show-ports miter
|
||||
2
tests/various/help.ys
Normal file
2
tests/various/help.ys
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
help -all
|
||||
help -celltypes
|
||||
5
tests/various/scratchpad.ys
Normal file
5
tests/various/scratchpad.ys
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
scratchpad -set foo "bar baz"
|
||||
scratchpad -copy foo oof
|
||||
scratchpad -unset foo
|
||||
scratchpad -assert oof "bar baz"
|
||||
scratchpad -assert-unset foo
|
||||
Loading…
Add table
Add a link
Reference in a new issue