mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-23 00:55:32 +00:00
Merge remote-tracking branch 'origin/master' into eddie/abc9_mfs
This commit is contained in:
Eddie Hung
commit
94ab3791ce
30 changed files with 1577 additions and 1080 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)
|
||||
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
|
||||
|
|
@ -264,3 +264,30 @@ 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
|
||||
|
|
|
|||
|
|
@ -20,10 +20,12 @@ 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_ %%'"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -22,3 +22,19 @@ 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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue