Skip to content

Y
yosys-tests
Unverified Commit d280be7e by Miodrag Milanović Committed by GitHub
Options

Merge pull request #77 from SergeyDegtyar/review_backends_group 

Review backends group
parents 8da72764 48311829
Showing with 411 additions and 999 deletions
backends/.gitignore
*/work_*/
/.stamp
/run-test.mk
backends/Makefile
all: work
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 ))
PYTHON_EXECUTABLE := $(shell if python3 -c ""; then echo "python3"; else echo "python"; fi)
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
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
output reg A,
output reg cout
);
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
backends/write_aiger/top.v → backends/write_aiger/top_diff_cells.v
......@@ -7,13 +7,13 @@ module top
output reg A,
output reg cout
);
reg ASSERT = 1;
(* anyconst *) reg foo;
(* anyseq *) reg too;
initial begin
begin
A = 0;
......@@ -21,23 +21,19 @@ module top
end
end
`ifndef BUG
always @(posedge x) begin
if ($initstate)
if ($initstate)
A <= 0;
A <= y + cin + too;
assume(too);
assume(too);
assume(s_eventually too);
end
always @(negedge x) begin
if ($initstate)
if ($initstate)
cout <= 0;
cout <= y + A + foo;
assert(ASSERT);
assert(s_eventually ASSERT);
end
`else
assign {cout,A} = cin - y * x;
`endif
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
end
end
`ifndef BUG
always @(posedge x) begin
if ($initstate)
A <= 1'bX;
......@@ -39,9 +39,6 @@ always @(negedge x) begin
end
assign X = 1'bX;
`else
assign {cout,A} = cin - y * x;
`endif
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