Skip to content

Y
yosys-tests
Commit 48311829 by SergeyDegtyar
Options

Rename test group back to 'backends'.

parent 9af3cae7
Showing with 411 additions and 999 deletions

Too many changes to show.
Plain diff Email patch

To preserve performance only 1000 of 1000+ files are displayed.

backends/.gitignore
*/work_*/ */work_*/
/.stamp /.stamp
/run-test.mk
backends/Makefile
all: work PYTHON_EXECUTABLE := $(shell if python3 -c ""; then echo "python3"; else echo "python"; fi)
touch .stamp
clean::
rm -f .stamp
define template
$(foreach design,$(1),
$(foreach script,$(2),
work:: $(design)/work_$(script)/.stamp
$(design)/work_$(script)/.stamp:
bash run.sh $(design) $(script)
clean::
rm -rf $(design)/work_$(script)
))
endef
#write_aiger
$(eval $(call template,write_aiger,write_aiger write_aiger_ascii write_aiger_zinit write_aiger_miter write_aiger_symbols write_aiger_map write_aiger_vmap write_aiger_I write_aiger_O write_aiger_B ))
$(eval $(call template,write_aiger_error, write_aiger_cant_find_top_module write_aiger_cant_open_file write_aiger_miter_and_asserts write_aiger_unsupported_cell_type ))
#write_xaiger
$(eval $(call template,write_xaiger,write_xaiger write_xaiger_ascii write_xaiger_map write_xaiger_vmap ))
$(eval $(call template,write_xaiger_fsm,write_xaiger write_xaiger_ascii write_xaiger_map write_xaiger_vmap ))
$(eval $(call template,write_xaiger_mem,write_xaiger write_xaiger_ascii write_xaiger_map write_xaiger_vmap ))
$(eval $(call template,write_xaiger_error, write_xaiger_cant_find_top_module write_xaiger_cant_open_file ))
#write_blif
$(eval $(call template,write_blif,write_blif write_blif_top write_blif_buf write_blif_unbuf write_blif_true write_blif_false write_blif_undef write_blif_noalias write_blif_icells write_blif_gates write_blif_conn write_blif_attr write_blif_param write_blif_cname write_blif_iname write_blif_iattr write_blif_blackbox write_blif_impltf))
$(eval $(call template,write_blif_error, write_blif_unmapped_mem write_blif_cant_find_top_module write_blif_unmapped_proc))
#write_btor
$(eval $(call template,write_btor,write_btor write_btor_v write_btor_s))
$(eval $(call template,write_btor_shift,write_btor write_btor_v write_btor_s))
$(eval $(call template,write_btor_div_mod,write_btor write_btor_v write_btor_s))
$(eval $(call template,write_btor_fsm,write_btor write_btor_v write_btor_s write_btor_shift))
$(eval $(call template,write_btor_shift_shiftx,write_btor_shift))
$(eval $(call template,write_btor_logic,write_btor write_btor_v write_btor_s))
$(eval $(call template,write_btor_mem,write_btor_mem write_btor_mem_v write_btor_mem_s))
$(eval $(call template,write_btor_pmux,write_btor_pmux))
$(eval $(call template,write_btor_and_or,write_btor_and_or))
$(eval $(call template,write_btor_shiftx,write_btor write_btor_v write_btor_s))
$(eval $(call template,write_btor_init_assert,write_btor write_btor_v write_btor_s))
$(eval $(call template,write_btor_error, write_btor_no_top_module write_btor_unsupported_cell_type))
#write_edif
$(eval $(call template,write_edif,write_edif write_edif_top write_edif_nogndvcc write_edif_pvector_par write_edif_pvector_bra write_edif_pvector_ang write_edif_attrprop ))
$(eval $(call template,write_edif_error, write_edif_cyclic_dependency write_edif_constant_nodes write_edif_unmapped_mem write_edif_unmapped_proc write_edif_no_module_found ))
#write_firrtl
$(eval $(call template,write_firrtl,write_firrtl))
$(eval $(call template,write_firrtl_fsm,write_firrtl_fsm))
$(eval $(call template,write_firrtl_mem,write_firrtl_mem write_firrtl_mem_wr))
$(eval $(call template,write_firrtl_logic,write_firrtl ))
$(eval $(call template,write_firrtl_reduce,write_firrtl ))
$(eval $(call template,write_firrtl_shift,write_firrtl ))
$(eval $(call template,write_firrtl_shiftx,write_firrtl ))
$(eval $(call template,write_firrtl_paramod,write_firrtl))
$(eval $(call template,write_firrtl_mul,write_firrtl))
$(eval $(call template,write_firrtl_sub,write_firrtl))
$(eval $(call template,write_firrtl_pow,write_firrtl))
$(eval $(call template,write_firrtl_error, write_firrtl_fully_selected write_firrtl_negative_edge_ff write_firrtl_inout_port write_firrtl_unclocked_write_port write_firrtl_complex_write_enable ))
#write_ilang
$(eval $(call template,write_ilang,write_ilang write_ilang_selected))
$(eval $(call template,write_ilang_mem,write_ilang_mem))
$(eval $(call template,write_ilang_mux,write_ilang write_ilang_selected))
$(eval $(call template,write_ilang_fsm,write_ilang write_ilang_selected))
$(eval $(call template,write_ilang_tri,write_ilang write_ilang_selected))
$(eval $(call template,write_ilang_error,write_ilang_error))
#write_intersynth
$(eval $(call template,write_intersynth,write_intersynth write_intersynth_selected write_intersynth_lib write_intersynth_notypes))
$(eval $(call template,write_intersynth_error, write_intersynth_cant_export write_intersynth_unprocessed_proc write_intersynth_cant_open_lib_file))
#write_json
$(eval $(call template,write_json,write_json write_json_aig json json_o json_o_aig json_aig))
$(eval $(call template,write_json_error,write_json_error))
#write_simplec
$(eval $(call template,write_simplec,write_simplec write_simplec_cmos3 write_simplec_cmos4 write_simplec_verbose write_simplec_i8 write_simplec_i16 write_simplec_i32 write_simplec_i64))
$(eval $(call template,write_simplec_mux,write_simplec write_simplec_cmos3 write_simplec_cmos4 write_simplec_verbose write_simplec_i8 write_simplec_i16 write_simplec_i32 write_simplec_i64))
$(eval $(call template,write_simplec_logic,write_simplec write_simplec_cmos3 write_simplec_cmos4 write_simplec_verbose write_simplec_i8 write_simplec_i16 write_simplec_i32 write_simplec_i64))
$(eval $(call template,write_simplec_error,write_simplec_no_c_model write_simplec_not_top_module ))
#write_smt2
$(eval $(call template,write_smt2,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
$(eval $(call template,write_smt2_logic,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
$(eval $(call template,write_smt2_mem,write_smt2 write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_mem_memtest write_smt2_memtest write_smt2_stbv_memtest write_smt2_anyseq))
$(eval $(call template,write_smt2_fsm,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
$(eval $(call template,write_smt2_init_assert,write_smt2_init_assert))
$(eval $(call template,write_smt2_reduce,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
$(eval $(call template,write_smt2_shiftx,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
$(eval $(call template,write_smt2_error, write_smt2_cyclic_dependency write_smt2_cant_open_tpl write_smt2_multiple_drivers write_smt2_logic_loop ))
#write_smv
$(eval $(call template,write_smv,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
$(eval $(call template,write_smv_wide,write_smv write_smv_verbose write_smv_tpl))
$(eval $(call template,write_smv_shift,write_smv_shift))
$(eval $(call template,write_smv_fsm,write_smv write_smv_noproc write_smv_verbose write_smv_tpl))
$(eval $(call template,write_smv_reduce,write_smv_noproc))
$(eval $(call template,write_smv_logic,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
$(eval $(call template,write_smv_init_assert,write_smv_init_assert))
$(eval $(call template,write_smv_cmos4,write_smv_cmos4))
$(eval $(call template,write_smv_shiftx,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
$(eval $(call template,write_smv_error,write_smv_cant_open_template write_smv_unsupported_cell))
#write_spice
$(eval $(call template,write_spice,write_spice write_spice_top write_spice_big_endian write_spice_neg_i write_spice_pos_i write_spice_nc_prefix write_spice_inames ))
$(eval $(call template,write_spice_error, write_spice_cant_find_top_module write_spice_unmapped_mem write_spice_unmapped_proc))
#write_table
$(eval $(call template,write_table,write_table ))
#write_verilog
$(eval $(call template,write_verilog,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v write_verilog_slice write_verilog_lut))
$(eval $(call template,write_verilog_tri,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
$(eval $(call template,write_verilog_ffs,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
$(eval $(call template,write_verilog_latch,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
$(eval $(call template,write_verilog_concat,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
$(eval $(call template,write_verilog_shiftx,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
$(eval $(call template,write_verilog_shift_shiftx,write_verilog_shift ))
all:: run-test.mk
@touch .stamp
@$(MAKE) -f run-test.mk
clean:: run-test.mk
@rm -f .stamp
@$(MAKE) -f run-test.mk clean
run-test.mk: ../generate.py
@$(PYTHON_EXECUTABLE) ../generate.py > run-test.mk
.PHONY: all clean .PHONY: all clean
backends/common.v deleted 100644 → 0
module assert_equal(input clk, input test, input pat);
always @(posedge clk)
begin
if (test != pat)
begin
$display("ERROR: ASSERTION FAILED in %m:",$time);
$stop;
end
end
endmodule
module assert_dff(input clk, input test, input pat);
always @(posedge clk)
begin
#1;
if (test != pat)
begin
$display("ERROR: ASSERTION FAILED in %m:",$time);
$stop;
end
end
endmodule
module assert_tri(input en, input A, input B);
always @(posedge en)
begin
#1;
if (A !== B)
begin
$display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
$stop;
end
end
endmodule
module assert_Z(input clk, input A);
always @(posedge clk)
begin
#1;
if (A === 1'bZ)
begin
$display("ERROR: ASSERTION FAILED in %m:",$time," ",A);
$stop;
end
end
endmodule
module assert_comb(input A, input B);
always @(*)
begin
#1;
if (A !== B)
begin
$display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
$stop;
end
end
endmodule
backends/common/add_sub.v 0 → 100644
module top
(
input [3:0] x,
input [3:0] y,
output [3:0] A,
output [3:0] B
);
assign A = x + y;
assign B = x - y;
endmodule
backends/common/adffs.v 0 → 100644
module top( input d, clk, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge clr )
if ( clr )
q <= 1'b0;
else
q <= d;
endmodule
backends/common/counter.v 0 → 100644
module top ( out, clk, reset );
output [7:0] out;
input clk, reset;
reg [7:0] out;
always @(posedge clk, posedge reset)
if (reset)
out <= 8'b0;
else
out <= out + 1;
endmodule
backends/common/dffs.v 0 → 100644
module top ( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
backends/common/latches.v 0 → 100644
module top ( input d, clk, en, output reg q );
always @*
if ( en )
q <= d;
endmodule
backends/common/logic.v 0 → 100644
module top
(
input [0:7] in,
output B1,B2,B3,B4,B5,B6,B7,B8,B9,B10
);
assign B1 = in[0] & in[1];
assign B2 = in[0] | in[1];
assign B3 = in[0] ~& in[1];
assign B4 = in[0] ~| in[1];
assign B5 = in[0] ^ in[1];
assign B6 = in[0] ~^ in[1];
assign B7 = ~in[0];
assign B8 = in[0];
assign B9 = in[0:1] && in [2:3];
assign B10 = in[0:1] || in [2:3];
endmodule
backends/common/memory.v 0 → 100644
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
backends/common/mul.v 0 → 100644
module top
(
input [5:0] x,
input [5:0] y,
output [11:0] A,
);
assign A = x * y;
endmodule
backends/common/mux.v 0 → 100644
module top ( S, D, Y );
input[2:0] S;
input[7:0] D;
output Y;
reg Y;
wire[2:0] S;
wire[7:0] D;
always @*
begin
case( S )
0 : Y = D[0];
1 : Y = D[1];
2 : Y = D[2];
3 : Y = D[3];
4 : Y = D[4];
5 : Y = D[5];
6 : Y = D[6];
7 : Y = D[7];
endcase
end
endmodule
backends/common/shifter.v 0 → 100644
module top(out, clk, in);
output [7:0] out;
input signed clk, in;
reg signed [7:0] out = 0;
always @(posedge clk)
begin
out <= out >> 1;
out[7] <= in;
end
endmodule
backends/common/tribuf.v 0 → 100644
module top(en, i, o);
input en;
input i;
output reg o;
always @(en or i)
o <= (en)? i : 1'bZ;
endmodule
backends/run.sh deleted 100644 → 0
#!/bin/bash
set -x
test -d $1
test -f scripts/$2.ys
rm -rf $1/work_$2
mkdir $1/work_$2
cd $1/work_$2
touch .start
# cases where 'syntax error' or other errors are expected
if echo "$1" | grep ".*_error"; then
expected_string=""
#Change checked string for check other errors
if [ "$2" = "write_aiger_cant_find_top_module" ]; then
expected_string="ERROR: Can't find top module in current design!"
elif [ "$2" = "write_aiger_cant_open_file" ]; then
expected_string="ERROR: Can't open file "
elif [ "$2" = "write_aiger_miter_and_asserts" ]; then
expected_string="ERROR: Running AIGER back-end in -miter mode, but design contains \$assert, \$assume, \$live and/or \$fair cells!"
elif [ "$2" = "write_aiger_unsupported_cell_type" ]; then
expected_string="ERROR: Unsupported cell type: "
elif [ "$2" = "write_xaiger_cant_find_top_module" ]; then
expected_string="ERROR: Can't find top module in current design!"
elif [ "$2" = "write_xaiger_cant_open_file" ]; then
expected_string="ERROR: Can't open file "
elif [ "$2" = "write_blif_unmapped_mem" ]; then
expected_string="ERROR: Found unmapped memories in module "
elif [ "$2" = "write_blif_cant_find_top_module" ]; then
expected_string="ERROR: Can't find top module "
elif [ "$2" = "write_blif_unmapped_proc" ]; then
expected_string="ERROR: Found unmapped processes in module "
elif [ "$2" = "write_btor_no_top_module" ]; then
expected_string="ERROR: No top module found."
elif [ "$2" = "write_btor_unsupported_cell_type" ]; then
expected_string="ERROR: Unsupported cell type: "
elif [ "$2" = "write_btor_no_driver" ]; then
expected_string="ERROR: No driver for signal bit "
elif [ "$2" = "write_edif_cyclic_dependency" ]; then
expected_string="ERROR: Cyclic dependency between modules found! Cycle includes module "
elif [ "$2" = "write_edif_constant_nodes" ]; then
expected_string="ERROR: Design contains constant nodes (map with \"hilomap\" first)."
elif [ "$2" = "write_edif_unmapped_mem" ]; then
expected_string="ERROR: Found unmapped memories in module "
elif [ "$2" = "write_edif_unmapped_proc" ]; then
expected_string="ERROR: Found unmapped processes in module "
elif [ "$2" = "write_edif_no_module_found" ]; then
expected_string="ERROR: No module found in design!"
elif [ "$2" = "write_firrtl_fully_selected" ]; then
expected_string="ERROR: This command only operates on fully selected designs!"
elif [ "$2" = "write_firrtl_negative_edge_ff" ]; then
expected_string="ERROR: Negative edge clock on FF "
elif [ "$2" = "write_firrtl_inout_port" ]; then
expected_string="ERROR: Module port top.q_a is inout!"
elif [ "$2" = "write_firrtl_unclocked_write_port" ]; then
expected_string="ERROR: Unclocked write port "
elif [ "$2" = "write_firrtl_complex_write_enable" ]; then
expected_string="ERROR: Complex write enable on port "
elif [ "$2" = "write_ilang_error" ]; then
expected_string="ERROR: Can't open file \`tt/file1.il' for writing: No such file or directory"
elif [ "$2" = "write_intersynth_cant_export" ]; then
expected_string="ERROR: Can't export composite or non-word-wide signal "
elif [ "$2" = "write_intersynth_unprocessed_proc" ]; then
expected_string="ERROR: Can't generate a netlist for a module with unprocessed memories or processes!"
elif [ "$2" = "write_intersynth_cant_open_lib_file" ]; then
expected_string="ERROR: Can't open lib file "
elif [ "$2" = "write_json_error" ]; then
expected_string="ERROR: Can't open file "
elif [ "$2" = "write_simplec_no_c_model" ]; then
expected_string="ERROR: No C model for \$lut available at the moment (FIXME)."
elif [ "$2" = "write_simplec_not_top_module" ]; then
expected_string="ERROR: Current design has no top module."
elif [ "$2" = "write_smt2_cyclic_dependency" ]; then
expected_string="ERROR: Cyclic dependency between modules found! Cycle includes module "
elif [ "$2" = "write_smt2_cant_open_tpl" ]; then
expected_string="ERROR: Can't open template file "
elif [ "$2" = "write_smt2_multiple_drivers" ]; then
expected_string="ERROR: Found multiple drivers for "
elif [ "$2" = "write_smt2_logic_loop" ]; then
expected_string="ERROR: Found logic loop in module "
elif [ "$2" = "write_smv_cant_open_template" ]; then
expected_string="ERROR: Can't open template file "
elif [ "$2" = "write_smv_unsupported_cell" ]; then
expected_string="ERROR: Found currently unsupported cell type "
elif [ "$2" = "write_spice_cant_find_top_module" ]; then
expected_string="ERROR: Can't find top module "
elif [ "$2" = "write_spice_unmapped_mem" ]; then
expected_string="ERROR: Found unmapped memories in module "
elif [ "$2" = "write_spice_unmapped_proc" ]; then
expected_string="ERROR: Found unmapped processes in module"
fi
if yosys -ql yosys.log ../../scripts/$2.ys; then
echo FAIL > ${1}_${2}.status
else
if grep "$expected_string" yosys.log && [ "$expected_string" != "" ]; then
echo PASS > ${1}_${2}.status
else
echo FAIL > ${1}_${2}.status
fi
fi
else
yosys -ql yosys.log ../../scripts/$2.ys
if [ $? != 0 ] ; then
echo FAIL > ${1}_${2}.status
touch .stamp
exit 0
fi
sed -i 's/reg =/dummy =/' ./synth.v
if [ -f "../../../../../techlibs/common/simcells.v" ]; then
COMMON_PREFIX=../../../../../techlibs/common
else
COMMON_PREFIX=/usr/local/share/yosys
fi
iverilog -o testbench ../testbench.v synth.v ../../common.v $COMMON_PREFIX/simcells.v $COMMON_PREFIX/simlib.v
if [ $? != 0 ] ; then
echo FAIL > ${1}_${2}.status
touch .stamp
exit 0
fi
if ! vvp -N testbench > testbench.log 2>&1; then
grep 'ERROR' testbench.log
echo FAIL > ${1}_${2}.status
elif grep 'ERROR' testbench.log || ! grep 'OKAY' testbench.log; then
echo FAIL > ${1}_${2}.status
else
echo PASS > ${1}_${2}.status
fi
fi
touch .stamp
backends/scripts/write_aiger.ys deleted 100644 → 0
read_verilog -sv ../top.v
aigmap
write_aiger aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_B.ys deleted 100644 → 0
read_verilog -sv ../top.v
aigmap
write_aiger -B aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_I.ys deleted 100644 → 0
read_verilog -sv ../top.v
aigmap
write_aiger -I aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_O.ys deleted 100644 → 0
read_verilog -sv ../top.v
aigmap
write_aiger -O aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_ascii.ys deleted 100644 → 0
read_verilog -sv ../top.v
aigmap
write_aiger -ascii aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_cant_find_top_module.ys deleted 100644 → 0
read_verilog -sv ../top.v
aigmap
write_aiger aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_cant_open_file.ys deleted 100644 → 0
read_verilog -sv ../top2.v
aigmap
write_aiger -map tt/tt.map aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_map.ys deleted 100644 → 0
read_verilog -sv ../top.v
aigmap
write_aiger -map a.map aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_miter.ys deleted 100644 → 0
read_verilog -sv ../top_clean.v
synth -top top
aigmap
write_aiger -miter aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_miter_and_asserts.ys deleted 100644 → 0
read_verilog -sv ../top2.v
aigmap
write_aiger -miter aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_symbols.ys deleted 100644 → 0
read_verilog -sv ../top.v
aigmap
write_aiger -symbols aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_unsupported_cell_type.ys deleted 100644 → 0
read_verilog -sv ../top2.v
synth
write_aiger aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_vmap.ys deleted 100644 → 0
read_verilog -sv ../top.v
aigmap
write_aiger -vmap a.map aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_zinit.ys deleted 100644 → 0
read_verilog -sv ../top_clean.v
aigmap
write_aiger -zinit aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_blif.ys deleted 100644 → 0
read_verilog -sv ../top.v
proc
write_blif blif1.blif
design -reset
read_verilog -sv ../top.v
proc
opt
write_blif blif2.blif
design -reset
read_verilog -sv ../top.v
synth
abc -lut 2
write_blif blif3.blif
design -reset
read_verilog -sv ../top.v
synth
abc -sop
write_blif blif4.blif
design -reset
read_verilog -sv ../top.v
synth
abc -g AND,XOR,NOR
write_blif blif4.blif
design -reset
read_verilog -sv ../top.v
synth
abc -g ANDNOT,ORNOT
write_blif blif4.blif
design -reset
read_verilog -sv ../top.v
synth
abc -g cmos3
write_blif blif4.blif
design -reset
read_verilog -sv ../top.v
abc -g AOI4
synth -top top
write_blif blif4.blif
design -reset
read_verilog -sv ../top.v
synth -top top
write_blif blif5.blif
write_verilog synth.v
backends/scripts/write_btor.ys deleted 100644 → 0
read_verilog -sv ../top.v
hierarchy -top top
proc
write_btor btor.btor
design -reset
read_verilog -sv ../top.v
synth -top top
write_btor btor1.btor
design -reset
read_verilog -sv ../top.v
proc_prune
proc_init
proc_mux
proc_dff
write_btor btor2.btor
design -reset
read_verilog -sv ../top.v
synth
abc
write_btor btor3.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g AND,XOR,NOR
write_btor btor4.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g ANDNOT,ORNOT
write_btor btor5.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g cmos3
write_btor btor6.btor
design -reset
read_verilog -sv ../top.v
abc -g AOI4
synth -top top
write_btor btor7.btor
design -reset
read_verilog -sv ../top.v
abc -g OAI4
synth -top top
write_btor btor8.btor
design -reset
read_verilog -sv ../top.v
aigmap
proc
write_btor btor9.btor
synth -top top
write_btor btor10.btor
design -reset
read_verilog -sv ../top_clean.v
synth -top top
write_verilog synth.v
backends/scripts/write_btor_mem.ys deleted 100644 → 0
read_verilog -sv ../top.v
memory
proc
write_btor btor.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
write_btor btor1.btor
design -reset
read_verilog -sv ../top.v
memory
synth
abc
write_btor btor3.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g AND,XOR,NOR
write_btor btor4.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g ANDNOT,ORNOT
write_btor btor5.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g cmos3
write_btor btor6.btor
design -reset
read_verilog -sv ../top.v
memory
abc -g AOI4
synth -top top
write_btor btor7.btor
design -reset
read_verilog -sv ../top.v
memory
abc -g OAI4
synth -top top
write_btor btor8.btor
design -reset
read_verilog -sv ../top.v
memory
aigmap
proc
write_btor btor9.btor
synth -top top
write_btor btor10.btor
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
backends/scripts/write_btor_mem_s.ys deleted 100644 → 0
read_verilog -sv ../top.v
memory_collect
proc
write_btor -s btor.btor
design -reset
read_verilog -sv ../top.v
synth -top top
design -reset
read_verilog -sv ../top.v
memory
synth
abc
write_btor -s btor3.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g AND,XOR,NOR
write_btor -s btor4.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g ANDNOT,ORNOT
write_btor -s btor5.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g cmos3
write_btor -s btor6.btor
design -reset
read_verilog -sv ../top.v
memory
abc -g AOI4
synth -top top
write_btor -s btor7.btor
design -reset
read_verilog -sv ../top.v
memory
abc -g OAI4
synth -top top
write_btor -s btor8.btor
design -reset
read_verilog -sv ../top.v
memory
aigmap
proc
write_btor -s btor9.btor
synth -top top
write_btor -v btor10.btor
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
backends/scripts/write_btor_mem_v.ys deleted 100644 → 0
read_verilog -sv ../top.v
memory_collect
proc
write_btor -v btor.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
write_btor -v btor1.btor
design -reset
read_verilog -sv ../top.v
synth -top top
design -reset
read_verilog -sv ../top.v
memory
synth
abc
write_btor -v btor3.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g AND,XOR,NOR
write_btor -v btor4.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g ANDNOT,ORNOT
write_btor -v btor5.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g cmos3
write_btor -v btor6.btor
design -reset
read_verilog -sv ../top.v
memory
abc -g AOI4
synth -top top
write_btor -v btor7.btor
design -reset
read_verilog -sv ../top.v
memory
abc -g OAI4
synth -top top
write_btor -v btor8.btor
design -reset
read_verilog -sv ../top.v
memory
aigmap
proc
write_btor -v btor9.btor
synth -top top
write_btor -v btor10.btor
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
backends/scripts/write_btor_s.ys deleted 100644 → 0
read_verilog -sv ../top.v
proc
write_btor -s btor.btor
design -reset
read_verilog -sv ../top.v
synth -top top
write_btor -s btor1.btor
design -reset
read_verilog -sv ../top.v
proc_prune
proc_init
proc_mux
proc_dff
write_btor -s btor2.btor
design -reset
read_verilog -sv ../top.v
synth
abc
write_btor -s btor3.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g AND,XOR,NOR
write_btor -s btor4.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g ANDNOT,ORNOT
write_btor -s btor5.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g cmos3
write_btor -s btor6.btor
design -reset
read_verilog -sv ../top.v
abc -g AOI4
synth -top top
write_btor -s btor7.btor
design -reset
read_verilog -sv ../top.v
abc -g OAI4
synth -top top
write_btor -s btor8.btor
design -reset
read_verilog -sv ../top.v
aigmap
proc
write_btor -s btor9.btor
synth -top top
write_btor -s btor10.btor
design -reset
read_verilog -sv ../top_clean.v
synth -top top
write_verilog synth.v
backends/scripts/write_btor_unsupported_cell_type.ys deleted 100644 → 0
read_verilog ../top3.v
synth_ice40
write_btor btor.btor
backends/scripts/write_btor_v.ys deleted 100644 → 0
read_verilog -sv ../top.v
proc
write_btor -v btor.btor
design -reset
read_verilog -sv ../top.v
synth -top top
write_btor -v btor1.btor
design -reset
read_verilog -sv ../top.v
proc_prune
proc_init
proc_mux
proc_dff
write_btor -v btor2.btor
design -reset
read_verilog -sv ../top.v
synth
abc
write_btor -v btor3.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g AND,XOR,NOR
write_btor -v btor4.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g ANDNOT,ORNOT
write_btor -v btor5.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g cmos3
write_btor -v btor6.btor
design -reset
read_verilog -sv ../top.v
abc -g AOI4
synth -top top
write_btor -v btor7.btor
design -reset
read_verilog -sv ../top.v
abc -g OAI4
synth -top top
write_btor -v btor8.btor
design -reset
read_verilog -sv ../top.v
aigmap
proc
write_btor -v btor9.btor
synth -top top
write_btor -v btor10.btor
design -reset
read_verilog -sv ../top_clean.v
synth -top top
write_verilog synth.v
backends/scripts/write_edif_constant_nodes.ys deleted 100644 → 0
read_verilog -sv ../top3.v
proc
write_edif -nogndvcc blif1.blif
backends/scripts/write_edif_cyclic_dependency.ys deleted 100644 → 0
read_verilog -sv ../top4.v
proc
write_edif blif1.blif
backends/scripts/write_firrtl_mem_wr.ys deleted 100644 → 0
read_verilog ../top.v
proc
memory_dff -nordff
memory_collect
opt_reduce
clean
write_firrtl firrtl.firrtl
write_verilog synth.v
backends/scripts/write_smt2_multiple_drivers.ys deleted 100644 → 0
read_verilog ../top2.v
proc
memory
write_smt2 smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_stdt.ys deleted 100644 → 0
read_verilog ../top.v
proc
memory
write_smt2 -stdt smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_tpl.ys deleted 100644 → 0
read_verilog ../top.v
proc
memory
write_smt2 -tpl ../top.tpl smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_verbose.ys deleted 100644 → 0
read_verilog ../top.v
proc
memory
write_smt2 -verbose smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_wires.ys deleted 100644 → 0
read_verilog ../top.v
proc
memory
write_smt2 -wires smt2.smt2
write_verilog synth.v
backends/scripts/write_smv_cmos4.ys deleted 100644 → 0
read_verilog ../top.v
synth -top top
abc -g cmos4
write_smv smv.smv
write_verilog synth.v
backends/scripts/write_smv_shift.ys deleted 100644 → 0
read_verilog ../top.v
proc
write_smv smv.smv
design -reset
read_verilog ../top_clean.v
proc
write_smv smv.smv
write_verilog synth.v
backends/scripts/write_smv_synth.ys deleted 100644 → 0
read_verilog ../top.v
synth -top top
write_smv smv.smv
write_verilog synth.v
backends/scripts/write_xaiger.ys deleted 100644 → 0
read_verilog -sv ../top.v
aigmap
write_xaiger xaiger.xaiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_xaiger xaiger.xaiger
synth -top top
write_verilog synth.v
backends/scripts/write_xaiger_ascii.ys deleted 100644 → 0
read_verilog -sv ../top.v
aigmap
write_xaiger -ascii xaiger.xaiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_xaiger xaiger.xaiger
synth -top top
write_verilog synth.v
backends/scripts/write_xaiger_cant_find_top_module.ys deleted 100644 → 0
read_verilog -sv ../top.v
aigmap
write_xaiger xaiger.xaiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_xaiger xaiger.xaiger
synth -top top
write_verilog synth.v
backends/scripts/write_xaiger_cant_open_file.ys deleted 100644 → 0
read_verilog -sv ../top2.v
aigmap
write_xaiger -map tt/tt.map xaiger.xaiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_xaiger xaiger.xaiger
synth -top top
write_verilog synth.v
backends/scripts/write_xaiger_map.ys deleted 100644 → 0
read_verilog -sv ../top.v
proc
aigmap
write_xaiger -map a.map xaiger.xaiger
design -reset
read_verilog -sv ../top_clean.v
synth
aigmap
write_xaiger xaiger.xaiger
synth -top top
write_verilog synth.v
backends/scripts/write_xaiger_vmap.ys deleted 100644 → 0
read_verilog -sv ../top.v
aigmap
write_xaiger -vmap a.map xaiger.xaiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_xaiger xaiger.xaiger
synth -top top
write_verilog synth.v
backends/write_aiger/testbench.v deleted 100644 → 0
module testbench;
reg [2:0] in;
reg patt_out = 0;
reg patt_carry_out = 0;
wire out;
wire carryout;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
top uut (
.x(in[0]),
.y(in[1]),
.cin(in[2]),
.A(out),
.cout(carryout)
);
always @(posedge in[0])
patt_out <= in[1] + in[2];
always @(negedge in[0])
patt_carry_out <= in[1] + patt_out;
assert_comb out_test(.A(patt_out), .B(out));
assert_comb carry_test(.A(patt_carry_out), .B(carryout));
endmodule
backends/write_aiger/top_clean.v → backends/write_aiger/top3.v
...@@ -7,21 +7,18 @@ module top ...@@ -7,21 +7,18 @@ module top
output reg A, output reg A,
output reg cout output reg cout
); );
initial begin initial begin
A = 0; A = 0;
cout = 0; cout = 0;
end end
`ifndef BUG
always @(posedge x) begin always @(posedge x) begin
A <= y + cin; A <= y + cin;
end end
always @(negedge x) begin always @(negedge x) begin
cout <= y + A; cout <= y + A;
end end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
backends/write_aiger/top.v → backends/write_aiger/top_diff_cells.v
...@@ -7,13 +7,13 @@ module top ...@@ -7,13 +7,13 @@ module top
output reg A, output reg A,
output reg cout output reg cout
); );
reg ASSERT = 1; reg ASSERT = 1;
(* anyconst *) reg foo; (* anyconst *) reg foo;
(* anyseq *) reg too; (* anyseq *) reg too;
initial begin initial begin
begin begin
A = 0; A = 0;
...@@ -21,23 +21,19 @@ module top ...@@ -21,23 +21,19 @@ module top
end end
end end
`ifndef BUG
always @(posedge x) begin always @(posedge x) begin
if ($initstate) if ($initstate)
A <= 0; A <= 0;
A <= y + cin + too; A <= y + cin + too;
assume(too); assume(too);
assume(s_eventually too); assume(s_eventually too);
end end
always @(negedge x) begin always @(negedge x) begin
if ($initstate) if ($initstate)
cout <= 0; cout <= 0;
cout <= y + A + foo; cout <= y + A + foo;
assert(ASSERT); assert(ASSERT);
assert(s_eventually ASSERT); assert(s_eventually ASSERT);
end end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
backends/write_aiger/top_two_mods.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
reg ASSERT = 1;
(* anyconst *) reg foo;
(* anyseq *) reg too;
initial begin
begin
A = 0;
cout = 0;
end
end
always @(posedge x) begin
if ($initstate)
A <= 0;
A <= y + cin + too;
assume(too);
assume(s_eventually too);
end
always @(negedge x) begin
if ($initstate)
cout <= 0;
cout <= y + A + foo;
assert(ASSERT);
assert(s_eventually ASSERT);
end
endmodule
module top2
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
reg ASSERT = 1;
(* anyconst *) reg foo;
(* anyseq *) reg too;
initial begin
begin
A = 0;
cout = 0;
end
end
always @(posedge x) begin
if ($initstate)
A <= 0;
A <= y + cin + too;
assume(too);
assume(s_eventually too);
end
always @(negedge x) begin
if ($initstate)
cout <= 0;
cout <= y + A + foo;
assert(ASSERT);
assert(s_eventually ASSERT);
end
endmodule
backends/write_aiger_error/top2.v → backends/write_aiger/top_x_z.v
...@@ -22,7 +22,7 @@ module top ...@@ -22,7 +22,7 @@ module top
end end
end end
`ifndef BUG
always @(posedge x) begin always @(posedge x) begin
if ($initstate) if ($initstate)
A <= 1'bX; A <= 1'bX;
...@@ -39,9 +39,6 @@ always @(negedge x) begin ...@@ -39,9 +39,6 @@ always @(negedge x) begin
end end
assign X = 1'bX; assign X = 1'bX;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
backends/write_aiger/write_aiger.ys 0 → 100644
read_verilog -sv ../top3.v
aigmap
write_aiger result.out
design -reset
read_aiger result.out
backends/write_aiger/write_aiger_B.pat 0 → 100644
aig 5 5 0 2 0 1 0 0 0
2
10
0
c
backends/write_aiger/write_aiger_B.ys 0 → 100644
read_verilog -sv ../top3.v
aigmap
write_aiger -B result.out
design -reset
read_aiger result.out
backends/write_aiger/write_aiger_I.ys 0 → 100644
read_verilog -sv ../top3.v
aigmap
write_aiger -I aiger.aiger
design -reset
read_aiger aiger.aiger
backends/write_aiger/write_aiger_O.ys 0 → 100644
read_verilog -sv ../top3.v
aigmap
write_aiger -O aiger.aiger
design -reset
read_aiger aiger.aiger
backends/write_aiger/write_aiger__add_sub.pat 0 → 100644
aig 72 8 0 8 64
22
38
58
78
85
104
124
144
backends/write_aiger/write_aiger__add_sub.ys 0 → 100644
read_verilog -sv ../../common/add_sub.v
aigmap
write_aiger result.out
design -reset
read_aiger result.out
backends/write_aiger/write_aiger__adffs.ys 0 → 100644
read_verilog -sv ../../common/adffs.v
aigmap
write_aiger result.out
design -reset
read_aiger result.out
backends/write_aiger/write_aiger__counter.pat 0 → 100644
aig 10 10 0 8 0
2
4
6
8
10
12
14
16
c
backends/write_aiger/write_aiger__counter.ys 0 → 100644
read_verilog -sv ../../common/counter.v
aigmap
write_aiger result.out
design -reset
read_aiger result.out
backends/write_aiger/write_aiger__dffs.ys 0 → 100644
read_verilog -sv ../../common/dffs.v
aigmap
write_aiger result.out
design -reset
read_aiger result.out
backends/write_aiger/write_aiger__latches.ys 0 → 100644
read_verilog -sv ../../common/latches.v
aigmap
write_aiger result.out
design -reset
read_aiger result.out
backends/write_aiger/write_aiger__logic.pat 0 → 100644
aig 24 8 0 10 16
18
21
23
24
30
37
17
16
42
49
backends/write_aiger/write_aiger__logic.ys 0 → 100644
read_verilog -sv ../../common/logic.v
aigmap
write_aiger result.out
design -reset
read_aiger result.out
backends/write_aiger/write_aiger__mux.ys 0 → 100644
read_verilog -sv ../../common/mux.v
aigmap
write_aiger result.out
design -reset
read_aiger result.out
backends/write_aiger/write_aiger__tribuf.ys 0 → 100644
read_verilog -sv ../../common/tribuf.v
aigmap
write_aiger result.out
design -reset
read_aiger result.out
backends/write_aiger/write_aiger_ascii.pat 0 → 100644
aag 5 5 0 2 0
2
4
6
8
10
2
10
c
backends/write_aiger/write_aiger_ascii.ys 0 → 100644
read_verilog -sv ../top3.v
aigmap
write_aiger -ascii result.out
design -reset
read_aiger result.out
backends/write_aiger/write_aiger_ascii_diff_cells.ys 0 → 100644
read_verilog -sv ../top_diff_cells.v
aigmap
write_aiger -ascii aiger.aiger
backends/write_aiger/write_aiger_cant_find_top_module_fail.pat 0 → 100644
ERROR: Can't find top module in current design!
backends/write_aiger/write_aiger_cant_find_top_module_fail.ys 0 → 100644
read_verilog -sv ../top_two_mods.v
aigmap
write_aiger aiger.aiger
backends/write_aiger/write_aiger_cant_open_file_fail.ys 0 → 100644
read_verilog -sv ../top_x_z.v
aigmap
write_aiger -map tt/tt.map aiger.aiger
backends/write_aiger/write_aiger_diff_cells.ys 0 → 100644
read_verilog -sv ../top_diff_cells.v
aigmap
write_aiger aiger.aiger
backends/write_aiger/write_aiger_diff_cells_proc.ys 0 → 100644
read_verilog -sv ../top_diff_cells.v
synth
aigmap
write_aiger aiger.aiger
backends/write_aiger/write_aiger_map.ys 0 → 100644
read_verilog -sv ../top3.v
aigmap
write_aiger -map a.map aiger.aiger
design -reset
read_aiger aiger.aiger
backends/write_aiger/write_aiger_miter.ys 0 → 100644
read_verilog -sv ../top3.v
synth -top top
aigmap
write_aiger -miter result.out
design -reset
read_aiger result.out
backends/write_aiger/write_aiger_miter_and_asserts_fail.pat 0 → 100644
ERROR: Running AIGER back-end in -miter mode, but design contains \$assert, \$assume, \$live and/or \$fair cells!
backends/write_aiger/write_aiger_miter_and_asserts_fail.ys 0 → 100644
read_verilog -sv ../top_x_z.v
aigmap
write_aiger -miter aiger.aiger
backends/write_aiger/write_aiger_symbols.ys 0 → 100644
read_verilog -sv ../top3.v
aigmap
write_aiger -symbols result.out
design -reset
read_aiger result.out
backends/write_aiger/write_aiger_symbols_diff_cells.ys 0 → 100644
read_verilog -sv ../top_diff_cells.v
aigmap
write_aiger -symbols aiger.aiger
backends/write_aiger/write_aiger_unsupported_cell_type_fail.ys 0 → 100644
read_verilog -sv ../top_x_z.v
synth
write_aiger aiger.aiger
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment