diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index e5f678820..60be79d62 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -216,7 +216,7 @@ struct SatHelper int import_cell_counter = 0; for (auto &c : module->cells) - if (design->selected(module, c.second) && ct.cell_known(c.second->type)) { + if (design->selected(module, c.second)) { // log("Import cell: %s\n", RTLIL::id2cstr(c.first)); if (satgen.importCell(c.second, timestep)) { for (auto &p : c.second->connections) diff --git a/tests/xsthammer/run-check.sh b/tests/xsthammer/run-check.sh index 6a77e2367..b2d9193ae 100644 --- a/tests/xsthammer/run-check.sh +++ b/tests/xsthammer/run-check.sh @@ -9,12 +9,12 @@ job="$1" set -- set -e -mkdir -p check check_temp -cd check_temp +mkdir -p check check_temp/$job +cd check_temp/$job { echo "module ${job}_top(a, b, y_rtl, y_xst);" - sed -r '/^(input|output) / !d; /output/ { s/ y;/ y_rtl;/; p; }; s/ y_rtl;/ y_xst;/;' ../rtl/$job.v + sed -r '/^(input|output) / !d; /output/ { s/ y;/ y_rtl;/; p; }; s/ y_rtl;/ y_xst;/;' ../../rtl/$job.v echo "${job}_rtl rtl_variant (.a(a), .b(b), .y(y_rtl));" echo "${job}_xst xst_variant (.a(a), .b(b), .y(y_xst));" echo "endmodule" @@ -22,17 +22,17 @@ cd check_temp for mode in nomap techmap; do { - echo "read_verilog -DGLBL ../xst/$job.v" + echo "read_verilog -DGLBL ../../xst/$job.v" echo "rename $job ${job}_xst" - echo "read_verilog ../rtl/$job.v" + echo "read_verilog ../../rtl/$job.v" echo "rename $job ${job}_rtl" if [ $mode = techmap ]; then echo "techmap ${job}_rtl" fi echo "read_verilog ${job}_top.v" - echo "read_verilog ../xl_cells.v" + echo "read_verilog ../../xl_cells.v" echo "hierarchy -top ${job}_top" echo "flatten ${job}_top" @@ -42,7 +42,7 @@ for mode in nomap techmap; do echo "rename ${job}_top ${job}_top_${mode}" echo "write_ilang ${job}_top_${mode}.il" } > ${job}_top_${mode}.ys - ../../../yosys -q ${job}_top_${mode}.ys + ../../../../yosys -q ${job}_top_${mode}.ys done { @@ -52,12 +52,12 @@ done echo "sat -verify -show a,b,y_rtl,y_xst -prove y_rtl y_xst ${job}_top_techmap" } > ${job}_cmp.ys -if ../../../yosys -l ${job}.log ${job}_cmp.ys; then - mv ${job}.log ../check/${job}.log - rm -f ../check/${job}.err +if ../../../../yosys -l ${job}.log ${job}_cmp.ys; then + mv ${job}.log ../../check/${job}.log + rm -f ../../check/${job}.err else - mv ${job}.log ../check/${job}.err - rm -f ../check/${job}.log + mv ${job}.log ../../check/${job}.err + rm -f ../../check/${job}.log exit 1 fi diff --git a/tests/xsthammer/run-xst.sh b/tests/xsthammer/run-xst.sh index 216707072..b421e2954 100644 --- a/tests/xsthammer/run-xst.sh +++ b/tests/xsthammer/run-xst.sh @@ -14,59 +14,16 @@ cd xst_temp/$job cat > $job.xst <<- EOT run - -ifn $job.prj - -ifmt mixed - -ofn $job - -ofmt NGC - -p xc6vlx75t-2-ff784 - -top $job - -opt_mode Speed - -opt_level 1 - -power NO - -iuc NO - -keep_hierarchy NO - -rtlview Yes - -glob_opt AllClockNets - -read_cores YES - -write_timing_constraints NO - -cross_clock_analysis NO - -hierarchy_separator / - -bus_delimiter <> - -case maintain - -slice_utilization_ratio 100 - -bram_utilization_ratio 100 - -dsp_utilization_ratio 100 + -ifn $job.prj -ofn $job -p artix7 -top $job + -iobuf NO -ram_extract NO -rom_extract NO -use_dsp48 NO -fsm_extract YES -fsm_encoding Auto - -safe_implementation No - -fsm_style lut - -ram_extract Yes - -ram_style Auto - -rom_extract Yes - -shreg_extract YES - -rom_style Auto - -auto_bram_packing NO - -resource_sharing YES - -async_to_sync NO - -use_dsp48 auto - -iobuf NO - -max_fanout 100000 - -bufg 32 - -register_duplication YES - -register_balancing No - -optimize_primitives NO - -use_clock_enable Auto - -use_sync_set Auto - -use_sync_reset Auto - -iob auto - -equivalent_register_removal YES - -slice_utilization_ratio_maxmargin 5 EOT cat > $job.prj <<- EOT verilog work "../../rtl/$job.v" EOT -. /opt/Xilinx/14.2/ISE_DS/settings64.sh +. /opt/Xilinx/14.5/ISE_DS/settings64.sh xst -ifn $job.xst netgen -w -ofmt verilog $job.ngc $job diff --git a/tests/xsthammer/xl_cells.v b/tests/xsthammer/xl_cells.v index 6a3fa7996..775c84d24 100644 --- a/tests/xsthammer/xl_cells.v +++ b/tests/xsthammer/xl_cells.v @@ -8,6 +8,14 @@ input I; output O = !I; endmodule +module LUT1(O, I0); +parameter INIT = 0; +input I0; +wire [1:0] lutdata = INIT; +wire [0:0] idx = { I0 }; +output O = lutdata[idx]; +endmodule + module LUT2(O, I0, I1); parameter INIT = 0; input I0, I1; diff --git a/tests/xsthammer/xl_cells_tb.v b/tests/xsthammer/xl_cells_tb.v index a7472e4f1..17e0a2798 100644 --- a/tests/xsthammer/xl_cells_tb.v +++ b/tests/xsthammer/xl_cells_tb.v @@ -14,6 +14,17 @@ XL_INV XL(.O(XL_O), .I(I)); output ok = MY_O == XL_O; endmodule +module TB_LUT1(ok, I0); +input I0; +wire [1:0] MY_O, XL_O; +genvar i; +generate for (i=0; i<2; i=i+1) begin:V + MY_LUT1 #(.INIT(i)) MY(.O(MY_O[i]), .I0(I0)); + XL_LUT1 #(.INIT(i)) XL(.O(XL_O[i]), .I0(I0)); +end endgenerate +output ok = MY_O == XL_O; +endmodule + module TB_LUT2(ok, I0, I1); input I0, I1; wire [3:0] MY_O, XL_O; diff --git a/tests/xsthammer/xl_cells_tb.ys b/tests/xsthammer/xl_cells_tb.ys index 616f1b278..536c64a15 100644 --- a/tests/xsthammer/xl_cells_tb.ys +++ b/tests/xsthammer/xl_cells_tb.ys @@ -6,6 +6,7 @@ read_verilog xl_cells_tb.v rename GND MY_GND rename INV MY_INV +rename LUT1 MY_LUT1 rename LUT2 MY_LUT2 rename LUT3 MY_LUT3 rename LUT4 MY_LUT4 @@ -16,20 +17,22 @@ rename MUXF7 MY_MUXF7 rename VCC MY_VCC rename XORCY MY_XORCY -read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/GND.v -read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/INV.v -read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/LUT2.v -read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/LUT3.v -read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/LUT4.v -read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/LUT5.v -read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/LUT6.v -read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/MUXCY.v -read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/MUXF7.v -read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/VCC.v -read_verilog /opt/Xilinx/14.2/ISE_DS/ISE/verilog/src/unisims/XORCY.v +read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/GND.v +read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/INV.v +read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/LUT1.v +read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/LUT2.v +read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/LUT3.v +read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/LUT4.v +read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/LUT5.v +read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/LUT6.v +read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/MUXCY.v +read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/MUXF7.v +read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/VCC.v +read_verilog /opt/Xilinx/14.5/ISE_DS/ISE/verilog/src/unisims/XORCY.v rename GND XL_GND rename INV XL_INV +rename LUT1 XL_LUT1 rename LUT2 XL_LUT2 rename LUT3 XL_LUT3 rename LUT4 XL_LUT4 @@ -47,6 +50,7 @@ opt_clean sat -verify -prove ok 1'b1 TB_GND sat -verify -prove ok 1'b1 TB_INV +sat -verify -prove ok 1'b1 TB_LUT1 sat -verify -prove ok 1'b1 TB_LUT2 sat -verify -prove ok 1'b1 TB_LUT3 sat -verify -prove ok 1'b1 TB_LUT4