Skip to content

Y
yosys-tests
Commit 73abab3b by SergeyDegtyar
Options

Review and update tests for intel, sf2, xilinx, xilinx_ug901 architectures.

parent abaa8979
Showing with 1761 additions and 44 deletions
architecture_reviewed/Makefile
...@@ -47,4 +47,22 @@ $(eval $(call template,synth_greenpak4,synth_greenpak4 synth_greenpak4_top synth ...@@ -47,4 +47,22 @@ $(eval $(call template,synth_greenpak4,synth_greenpak4 synth_greenpak4_top synth
#ice40 #ice40
$(eval $(call template,synth_ice40,synth_ice40 synth_ice40_top synth_ice40_blif synth_ice40_edif synth_ice40_json synth_ice40_run synth_ice40_noflatten synth_ice40_flatten synth_ice40_retime synth_ice40_nocarry synth_ice40_nodffe synth_ice40_nobram synth_ice40_abc2 synth_ice40_vpr synth_ice40_relut synth_ice40_dsp synth_ice40_min_ce synth_ice40_noabc synth_ice40_device_u synth_ice40_device_lp synth_ice40_device_hx synth_ice40_opt synth_ice40_fully_selected_fail synth_ice40_device_unknown_fail synth_ice40_abc9 synth_ice40_abc9_retime_fail synth_ice40_mem_init synth_ice40_wide_ffs)) $(eval $(call template,synth_ice40,synth_ice40 synth_ice40_top synth_ice40_blif synth_ice40_edif synth_ice40_json synth_ice40_run synth_ice40_noflatten synth_ice40_flatten synth_ice40_retime synth_ice40_nocarry synth_ice40_nodffe synth_ice40_nobram synth_ice40_abc2 synth_ice40_vpr synth_ice40_relut synth_ice40_dsp synth_ice40_min_ce synth_ice40_noabc synth_ice40_device_u synth_ice40_device_lp synth_ice40_device_hx synth_ice40_opt synth_ice40_fully_selected_fail synth_ice40_device_unknown_fail synth_ice40_abc9 synth_ice40_abc9_retime_fail synth_ice40_mem_init synth_ice40_wide_ffs))
#intel
$(eval $(call template,synth_intel,synth_intel synth_intel_a10gx synth_intel_cyclone10 synth_intel_cycloneiv synth_intel_cycloneive synth_intel_cyclonev synth_intel_fully_selected_fail synth_intel_invalid_family_fail synth_intel_iopads synth_intel_max10 synth_intel_nobram synth_intel_noflatten synth_intel_retime synth_intel_run synth_intel_top synth_intel_vpr synth_intel_vqm ))
#sf2
$(eval $(call template,synth_sf2,synth_sf2 synth_sf2_top synth_sf2_edif synth_sf2_json synth_sf2_run synth_sf2_noflatten synth_sf2_retime synth_sf2_vlog synth_sf2_noiobs synth_sf2_clkbuf synth_sf2_fully_selected_fail ))
$(eval $(call template,synth_sf2_lcov,synth_sf2 synth_sf2_top synth_sf2_edif synth_sf2_json synth_sf2_run synth_sf2_noflatten synth_sf2_retime synth_sf2_vlog synth_sf2_noiobs synth_sf2_clkbuf ))
#xilinx
$(eval $(call template,synth_xilinx,synth_xilinx synth_xilinx_top synth_xilinx_blif synth_xilinx_edif synth_xilinx_run synth_xilinx_flatten synth_xilinx_retime synth_xilinx_vpr synth_xilinx_arch_xcup synth_xilinx_arch_xcu synth_xilinx_arch_xc7 synth_xilinx_arch_xc6s synth_xilinx_nobram synth_xilinx_nodram synth_xilinx_nosrl synth_xilinx_widemux synth_xilinx_nowidelut synth_xilinx_nocarry synth_xilinx_arch_xc6s_abc9 synth_xilinx_nowidelut_abc9 synth_xilinx_nodsp synth_xilinx_noclkbuf synth_xilinx_noiopad synth_xilinx_iopad synth_xilinx_ise synth_xilinx_flatten_before_abc synth_xilinx_arch_xc6v synth_xilinx_abc9_retime_fail synth_xilinx_fully_selected_fail synth_xilinx_invalid_arch_fail synth_xilinx_widemux_1_fail xilinx_srl synth_xilinx_dsp))
ifeq ($(ENABLE_HEAVY_TESTS),1)
$(eval $(call template,synth_xilinx_srl,synth_xilinx_srl))
$(eval $(call template,synth_xilinx_mux,synth_xilinx_mux))
$(eval $(call template,synth_xilinx_dsp,synth_xilinx_dsp))
endif
#xilinx_ug901_synthesis_examples
$(eval $(call template,xilinx_ug901_synthesis_examples, xilinx_ug901_asym_ram_sdp_read_wider xilinx_ug901_asym_ram_sdp_write_wider xilinx_ug901_asym_ram_tdp_read_first xilinx_ug901_asym_ram_tdp_write_first xilinx_ug901_black_box_1 xilinx_ug901_bytewrite_ram_1b xilinx_ug901_bytewrite_tdp_ram_nc xilinx_ug901_bytewrite_tdp_ram_readfirst2 xilinx_ug901_bytewrite_tdp_ram_rf xilinx_ug901_bytewrite_tdp_ram_wf xilinx_ug901_cmacc xilinx_ug901_cmult xilinx_ug901_dynamic_shift_registers_1 xilinx_ug901_dynpreaddmultadd xilinx_ug901_fsm_1 xilinx_ug901_latches xilinx_ug901_macc xilinx_ug901_mult_unsigned xilinx_ug901_presubmult xilinx_ug901_rams_dist xilinx_ug901_ram_simple_dual_one_clock xilinx_ug901_ram_simple_dual_two_clocks xilinx_ug901_rams_init_file xilinx_ug901_rams_pipeline xilinx_ug901_rams_sp_nc xilinx_ug901_rams_sp_rf xilinx_ug901_rams_sp_rf_rst xilinx_ug901_rams_sp_rom xilinx_ug901_rams_sp_rom_1 xilinx_ug901_rams_sp_wf xilinx_ug901_rams_tdp_rf_rf xilinx_ug901_registers_1 xilinx_ug901_sfir_shifter xilinx_ug901_shift_registers_0 xilinx_ug901_shift_registers_1 xilinx_ug901_squarediffmacc xilinx_ug901_squarediffmult xilinx_ug901_top_mux xilinx_ug901_tristates_1 xilinx_ug901_tristates_2 xilinx_ug901_xilinx_ultraram_single_port_no_change xilinx_ug901_xilinx_ultraram_single_port_read_first xilinx_ug901_xilinx_ultraram_single_port_write_first))
.PHONY: all clean .PHONY: all clean
architecture_reviewed/synth_efinix/synth_efinix_fulladder.ys
read_verilog ../top_.v read_verilog ../top_fulladder.v
hierarchy -top top hierarchy -top top
proc proc
......
architecture_reviewed/synth_efinix/synth_efinix_fulladder_json.ys deleted 100644 → 0
read_verilog ../top_fulladder.v
hierarchy -top top
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -json json.json # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 7 t:EFX_ADD
select -assert-count 8 t:EFX_LUT4
select -assert-none t:EFX_ADD t:EFX_LUT4 %% t:* %D
architecture_reviewed/synth_efinix/synth_efinix_fulladder_noflatten.ys deleted 100644 → 0
read_verilog ../top_fulladder.v
hierarchy -top top
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -noflatten # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 7 t:EFX_ADD
select -assert-count 8 t:EFX_LUT4
select -assert-none t:EFX_ADD t:EFX_LUT4 %% t:* %D
architecture_reviewed/synth_efinix/synth_efinix_fulladder_retime.ys → architecture_reviewed/synth_intel/synth_intel.ys
read_verilog ../top_fulladder.v read_verilog ../top.v
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -retime # equivalency check #-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/intel/max10/cells_sim.v synth_intel # equivalency check
equiv_opt -map +/intel/max10/cells_sim.v synth_intel # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module cd top # Constrain all select calls below inside the top module
stat stat
select -assert-count 2 t:EFX_LUT4 select -assert-count 14 t:fiftyfivenm_lcell_comb
select -assert-none t:EFX_LUT4 %% t:* %D select -assert-none t:fiftyfivenm_lcell_comb %% t:* %D
architecture_reviewed/synth_intel/synth_intel_a10gx.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/intel/a10gx/cells_sim.v synth_intel -family a10gx # equivalency check
equiv_opt -map +/intel/a10gx/cells_sim.v synth_intel -family a10gx # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 12 t:$lut
select -assert-count 1 t:twentynm_lcell_comb
select -assert-none t:$lut t:twentynm_lcell_comb %% t:* %D
architecture_reviewed/synth_intel/synth_intel_cyclone10.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/intel/cyclone10/cells_sim.v synth_intel -family cyclone10 # equivalency check
equiv_opt -map +/intel/cyclone10/cells_sim.v synth_intel -family cyclone10 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 14 t:cyclone10lp_lcell_comb
select -assert-none t:cyclone10lp_lcell_comb %% t:* %D
architecture_reviewed/synth_intel/synth_intel_cycloneiv.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/intel/cycloneiv/cells_sim.v synth_intel -family cycloneiv # equivalency check
equiv_opt -map +/intel/cycloneiv/cells_sim.v synth_intel -family cycloneiv # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 14 t:cycloneiv_lcell_comb
select -assert-none t:cycloneiv_lcell_comb %% t:* %D
architecture_reviewed/synth_intel/synth_intel_cycloneive.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/intel/cycloneive/cells_sim.v synth_intel -family cycloneive # equivalency check
equiv_opt -map +/intel/cycloneive/cells_sim.v synth_intel -family cycloneive # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 14 t:cycloneive_lcell_comb
select -assert-none t:cycloneive_lcell_comb %% t:* %D
architecture_reviewed/synth_efinix/synth_efinix_fulladder_run.ys → architecture_reviewed/synth_intel/synth_intel_cyclonev.ys
read_verilog ../top_fulladder.v read_verilog ../top.v
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -run begin:json # equivalency check #-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/intel/cyclonev/cells_sim.v synth_intel -family cyclonev # equivalency check
equiv_opt -map +/intel/cyclonev/cells_sim.v synth_intel -family cyclonev # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module cd top # Constrain all select calls below inside the top module
stat stat
select -assert-count 2 t:EFX_LUT4 select -assert-count 13 t:cyclonev_lcell_comb
select -assert-none t:EFX_LUT4 %% t:* %D select -assert-none t:cyclonev_lcell_comb %% t:* %D
architecture_reviewed/synth_intel/synth_intel_fully_selected_fail.pat 0 → 100644
ERROR: This command only operates on fully selected designs!
architecture_reviewed/synth_intel/synth_intel_fully_selected_fail.ys 0 → 100644
read_verilog ../top.v
select dffe
synth_intel
write_verilog synth.v
architecture_reviewed/synth_intel/synth_intel_invalid_family_fail.ys 0 → 100644
read_verilog ../top.v
synth_intel -family u
write_verilog synth.v
architecture_reviewed/synth_intel/synth_intel_iopads.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/intel/max10/cells_sim.v synth_intel -iopads # equivalency check
equiv_opt -map +/intel/max10/cells_sim.v synth_intel -iopads # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 12 t:fiftyfivenm_io_ibuf
select -assert-count 10 t:fiftyfivenm_io_obuf
select -assert-count 14 t:fiftyfivenm_lcell_comb
select -assert-none t:fiftyfivenm_io_ibuf t:fiftyfivenm_io_obuf t:fiftyfivenm_lcell_comb %% t:* %D
architecture_reviewed/synth_intel/synth_intel_max10.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/intel/max10/cells_sim.v synth_intel -family max10 # equivalency check
equiv_opt -map +/intel/max10/cells_sim.v synth_intel -family max10 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 14 t:fiftyfivenm_lcell_comb
select -assert-none t:fiftyfivenm_lcell_comb %% t:* %D
architecture_reviewed/synth_intel/synth_intel_nobram.ys 0 → 100644
read_verilog ../top_mem.v
design -save read
hierarchy -top top
proc
memory -nomap
equiv_opt -run :prove -map +/intel/max10/cells_sim.v synth_intel
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd top
select -assert-count 1 t:altsyncram
select -assert-none t:altsyncram %% t:* %D
design -load read
hierarchy -top top
proc
memory -nomap
#ERROR: Multiple edge sensitive events found for this signal!
#equiv_opt -run :prove -map +/intel/max10/cells_sim.v synth_intel -nobram
synth_intel -nobram
#memory
#opt -full
#miter -equiv -flatten -make_assert -make_outputs gold gate miter
#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
#design -load postopt
cd top
select -assert-count 520 t:dffeas
select -assert-count 976 t:fiftyfivenm_lcell_comb
select -assert-none t:dffeas t:fiftyfivenm_lcell_comb %% t:* %D
architecture_reviewed/synth_efinix/synth_efinix_fulladder_edif.ys → architecture_reviewed/synth_intel/synth_intel_noflatten.ys
read_verilog ../top_fulladder.v read_verilog ../top.v
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -edif edif.edif # equivalency check #-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/intel/max10/cells_sim.v synth_intel -noflatten # equivalency check
equiv_opt -map +/intel/max10/cells_sim.v synth_intel -noflatten # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module cd top # Constrain all select calls below inside the top module
stat stat
select -assert-count 7 t:EFX_ADD select -assert-count 14 t:fiftyfivenm_lcell_comb
select -assert-count 8 t:EFX_LUT4 select -assert-none t:fiftyfivenm_lcell_comb %% t:* %D
select -assert-none t:EFX_ADD t:EFX_LUT4 %% t:* %D
architecture_reviewed/synth_intel/synth_intel_retime.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/intel/max10/cells_sim.v synth_intel -retime # equivalency check
equiv_opt -map +/intel/max10/cells_sim.v synth_intel -retime # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 14 t:fiftyfivenm_lcell_comb
select -assert-none t:fiftyfivenm_lcell_comb %% t:* %D
architecture_reviewed/synth_intel/synth_intel_run.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/intel/max10/cells_sim.v synth_intel -run family:vpr # equivalency check
equiv_opt -map +/intel/max10/cells_sim.v synth_intel -run family:vpr # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 2 t:$add
select -assert-none t:$add %% t:* %D
architecture_reviewed/synth_intel/synth_intel_top.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/intel/max10/cells_sim.v synth_intel -top top # equivalency check
equiv_opt -map +/intel/max10/cells_sim.v synth_intel -top top # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 14 t:fiftyfivenm_lcell_comb
select -assert-none t:fiftyfivenm_lcell_comb %% t:* %D
architecture_reviewed/synth_efinix/synth_efinix_fulladder_top.ys → architecture_reviewed/synth_intel/synth_intel_vpr.ys
read_verilog ../top_fulladder.v read_verilog ../top.v
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -top top # equivalency check #-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/intel/max10/cells_sim.v synth_intel -vpr vpr.vpr # equivalency check
equiv_opt -map +/intel/max10/cells_sim.v synth_intel -vpr vpr.vpr # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module cd top # Constrain all select calls below inside the top module
stat stat
select -assert-count 2 t:EFX_LUT4 select -assert-count 14 t:fiftyfivenm_lcell_comb
select -assert-none t:EFX_LUT4 %% t:* %D select -assert-none t:fiftyfivenm_lcell_comb %% t:* %D
architecture_reviewed/synth_intel/synth_intel_vqm.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/intel/max10/cells_sim.v synth_intel -vqm vqm.vqm # equivalency check
equiv_opt -map +/intel/max10/cells_sim.v synth_intel -vqm vqm.vqm # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 14 t:fiftyfivenm_lcell_comb
select -assert-none t:fiftyfivenm_lcell_comb %% t:* %D
architecture_reviewed/synth_intel/top.v 0 → 100644
module top
(
input [3:0] x,
input [3:0] y,
input [3:0] cin,
output [4:0] A,
output [4:0] cout
);
assign {cout,A} = cin + y + x;
endmodule
architecture_reviewed/synth_intel/top_dpram.v 0 → 100644
/*
Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 72].
*/
module top (din, write_en, waddr, wclk, raddr, rclk, dout);
parameter addr_width = 6;
parameter data_width = 6;
input [addr_width-1:0] waddr, raddr;
input [data_width-1:0] din;
input write_en, wclk, rclk;
output [data_width-1:0] dout;
reg [data_width-1:0] dout;
reg [data_width-1:0] mem [(1<<addr_width)-1:0]
/* synthesis syn_ramstyle = "no_rw_check" */ ;
always @(posedge wclk) // Write memory.
begin
if (write_en)
mem[waddr] <= din; // Using write address bus.
end
always @(posedge rclk) // Read memory.
begin
dout <= mem[raddr]; // Using read address bus.
end
endmodule
architecture_reviewed/synth_intel/top_mem.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
architecture_reviewed/synth_sf2/synth_sf2.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CLKINT
select -assert-count 2 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CFG3
select -assert-count 1 t:CLKINT
select -assert-count 3 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CFG3 t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
architecture_reviewed/synth_sf2/synth_sf2_clkbuf.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -clkbuf # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CLKINT
select -assert-count 2 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -clkbuf # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CFG3
select -assert-count 1 t:CLKINT
select -assert-count 3 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CFG3 t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
architecture_reviewed/synth_sf2/synth_sf2_edif.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -edif edif.edif # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CLKINT
select -assert-count 2 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -edif edif.edif # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CFG3
select -assert-count 1 t:CLKINT
select -assert-count 3 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CFG3 t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
architecture_reviewed/synth_sf2/synth_sf2_fully_selected_fail.pat 0 → 100644
ERROR: This command only operates on fully selected designs!
architecture_reviewed/synth_sf2/synth_sf2_fully_selected_fail.ys 0 → 100644
read_verilog ../top.v
select dffe
synth_sf2
write_verilog synth.v
architecture_reviewed/synth_sf2/synth_sf2_json.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -json json.json # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CLKINT
select -assert-count 2 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -json json.json # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CFG3
select -assert-count 1 t:CLKINT
select -assert-count 3 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CFG3 t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
architecture_reviewed/synth_sf2/synth_sf2_noflatten.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -noflatten # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CLKINT
select -assert-count 2 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -noflatten # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CFG3
select -assert-count 1 t:CLKINT
select -assert-count 3 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CFG3 t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
architecture_reviewed/synth_sf2/synth_sf2_noiobs.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -noiobs # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CLKINT
select -assert-count 2 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -noiobs # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CFG3
select -assert-count 1 t:CLKINT
select -assert-count 3 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CFG3 t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
architecture_reviewed/synth_sf2/synth_sf2_retime.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -retime # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CLKINT
select -assert-count 2 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -retime # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CFG3
select -assert-count 1 t:CLKINT
select -assert-count 3 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CFG3 t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
architecture_reviewed/synth_sf2/synth_sf2_run.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -run begin:json # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CLKINT
select -assert-count 2 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -run begin:json # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CFG3
select -assert-count 1 t:CLKINT
select -assert-count 3 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CFG3 t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
architecture_reviewed/synth_sf2/synth_sf2_top.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -top dff # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CLKINT
select -assert-count 2 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -top dffe # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CFG3
select -assert-count 1 t:CLKINT
select -assert-count 3 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CFG3 t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
architecture_reviewed/synth_sf2/synth_sf2_vlog.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -vlog vlog.v # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CLKINT
select -assert-count 2 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/sf2/cells_sim.v synth_sf2 -vlog vlog.v # equivalency check
equiv_opt -map +/sf2/cells_sim.v synth_sf2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:CFG3
select -assert-count 1 t:CLKINT
select -assert-count 3 t:INBUF
select -assert-count 1 t:OUTBUF
select -assert-count 1 t:SLE
select -assert-none t:CFG3 t:CLKINT t:INBUF t:OUTBUF t:SLE %% t:* %D
architecture_reviewed/synth_sf2/top.v 0 → 100644
module dff
( input d, clk, output reg q );
initial begin
q = 0;
end
always @( posedge clk )
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk)
if ( en )
q <= d;
endmodule
module adff
( 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
architecture_reviewed/synth_sf2_lcov/synth_sf2_clkbuf.ys 0 → 100644
read_verilog ../top.v
synth_sf2 -clkbuf
architecture_reviewed/synth_sf2_lcov/synth_sf2_edif.ys 0 → 100644
read_verilog ../top.v
synth_sf2 -edif edif.edif
architecture_reviewed/synth_sf2_lcov/synth_sf2_json.ys 0 → 100644
read_verilog ../top.v
synth_sf2 -json json.json
architecture_reviewed/synth_sf2_lcov/synth_sf2_noflatten.ys 0 → 100644
read_verilog ../top.v
synth_sf2 -noflatten
architecture_reviewed/synth_sf2_lcov/synth_sf2_noiobs.ys 0 → 100644
read_verilog ../top.v
synth_sf2 -noiobs
architecture_reviewed/synth_sf2_lcov/synth_sf2_retime.ys 0 → 100644
read_verilog ../top.v
synth_sf2 -retime
architecture_reviewed/synth_sf2_lcov/synth_sf2_run.ys 0 → 100644
read_verilog ../top.v
synth_sf2 -run begin:json
architecture_reviewed/synth_sf2_lcov/synth_sf2_top.ys 0 → 100644
read_verilog ../top.v
synth_sf2 -top dff
architecture_reviewed/synth_sf2_lcov/synth_sf2_vlog.ys 0 → 100644
read_verilog ../top.v
synth_sf2 -vlog vlog.v
architecture_reviewed/synth_sf2_lcov/top.v 0 → 100644
module dff
( input d, clk, output reg q );
initial begin
q = 0;
end
always @( posedge clk )
q <= d;
endmodule
architecture_reviewed/synth_xilinx/synth_xilinx.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top adff
proc
#-assert option was skipped because of unproven cellss
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd adff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDCE
select -assert-none t:BUFG t:FDCE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_abc9.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -abc9 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -abc9 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_abc9_retime_fail.pat 0 → 100644
ERROR: -retime option not currently compatible with -abc9!
architecture_reviewed/synth_xilinx/synth_xilinx_abc9_retime_fail.ys 0 → 100644
read_verilog ../top.v
synth_xilinx -abc9 -retime
write_verilog synth.v
architecture_reviewed/synth_xilinx/synth_xilinx_arch_xc6s.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -arch xc6s # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -arch xc6s # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_arch_xc6s_abc9.pat 0 → 100644
Warning: 'synth_xilinx -abc9' not currently supported for the 'xc6s' family, will use timing for 'xc7' instead.
architecture_reviewed/synth_xilinx/synth_xilinx_arch_xc6s_abc9.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -arch xc6s -abc9 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
tee -o result.out equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -arch xc6s -abc9 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_arch_xc6v.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -arch xc6v # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -arch xc6v # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_arch_xc7.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -arch xc7 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -arch xc7 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_arch_xcu.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -arch xcu # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -arch xcu # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_arch_xcup.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -arch xcup # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -arch xcup # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_blif.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -blif blif.blif # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -blif blif.blif # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_dsp.ys 0 → 100644
read_verilog ../top_dsp_simd.v
design -save read
hierarchy -top simd
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd simd # Constrain all select calls below inside the top module
stat
select -assert-count 3 t:DSP48E1
select -assert-none t:DSP48E1 %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_edif.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -edif edif.edif # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -edif edif.edif # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_flatten.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -flatten # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -flatten # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_flatten_before_abc.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -flatten_before_abc # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -flatten_before_abc # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_fully_selected_fail.pat 0 → 100644
ERROR: This command only operates on fully selected designs!
architecture_reviewed/synth_xilinx/synth_xilinx_invalid_arch_fail.pat 0 → 100644
ERROR: Invalid Xilinx -family setting: 'zinq7000'.
architecture_reviewed/synth_xilinx/synth_xilinx_invalid_arch_fail.ys 0 → 100644
read_verilog ../top.v
synth_xilinx -arch zinq7000
architecture_reviewed/synth_xilinx/synth_xilinx_iopad.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -iopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-count 1 t:IBUF
select -assert-count 1 t:IBUFG
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:IBUFG t:OBUF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -iopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-count 2 t:IBUF
select -assert-count 1 t:IBUFG
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:IBUFG t:OBUF %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_ise.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -ise # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-count 1 t:IBUF
select -assert-count 1 t:IBUFG
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:IBUFG t:OBUF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -ise # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-count 2 t:IBUF
select -assert-count 1 t:IBUFG
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:IBUFG t:OBUF %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_nobram.ys 0 → 100644
read_verilog ../top_bram.v
design -save read
hierarchy -top top
proc
memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd top
select -assert-count 1 t:BUFG
select -assert-count 1 t:LUT2
select -assert-count 1 t:RAMB18E1
select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D
design -load read
hierarchy -top top
proc
memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -nobram
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd top
select -assert-count 1 t:BUFG
select -assert-count 35 t:FDRE
select -assert-count 3 t:LUT2
select -assert-count 4 t:LUT4
select -assert-count 16 t:LUT6
select -assert-count 8 t:MUXF7
select -assert-count 32 t:RAM128X1D
select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT4 t:LUT6 t:MUXF7 t:RAM128X1D %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_nocarry.ys 0 → 100644
read_verilog ../top_nocarry.v
design -save read
hierarchy -top top
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:LUT2
select -assert-count 3 t:LUT4
select -assert-count 4 t:LUT6
select -assert-count 5 t:MUXCY
select -assert-count 6 t:XORCY
select -assert-none t:LUT2 t:LUT4 t:LUT6 t:MUXCY t:XORCY %% t:* %D
design -load read
hierarchy -top top
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nocarry # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:LUT2
select -assert-count 1 t:LUT4
select -assert-count 4 t:LUT6
select -assert-none t:LUT2 t:LUT4 t:LUT6 %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_noclkbuf.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noclkbuf # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:FDRE
select -assert-none t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_nodram.ys 0 → 100644
read_verilog ../top_dpram.v
design -save read
hierarchy -top top
proc
memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd top
select -assert-count 2 t:BUFG
select -assert-count 6 t:FDRE
select -assert-count 6 t:RAM64X1D
select -assert-none t:BUFG t:FDRE t:RAM64X1D %% t:* %D
design -load read
hierarchy -top top
proc
memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -nodram
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd top
select -assert-count 2 t:BUFG
select -assert-count 390 t:FDRE
select -assert-count 90 t:LUT2
select -assert-count 10 t:LUT4
select -assert-count 155 t:LUT6
select -assert-count 32 t:MUXF7
select -assert-count 2 t:MUXF8
select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT4 t:LUT6 t:MUXF7 t:MUXF8 %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_nodsp.ys 0 → 100644
read_verilog ../top_dsp.v
design -save read
hierarchy -top top
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:DSP48E1
select -assert-none t:DSP48E1 %% t:* %D
design -load read
hierarchy -top top
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nodsp # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 15 t:LUT2
select -assert-count 3 t:LUT3
select -assert-count 4 t:LUT4
select -assert-count 5 t:LUT5
select -assert-count 45 t:LUT6
select -assert-count 11 t:MUXCY
select -assert-count 9 t:MUXF7
select -assert-count 3 t:MUXF8
select -assert-count 12 t:XORCY
select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:XORCY %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_noiopad.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -ise # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-count 1 t:IBUF
select -assert-count 1 t:IBUFG
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:IBUFG t:OBUF %% t:* %D
design -load read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -ise -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_nosrl.ys 0 → 100644
read_verilog ../top_nosrl.v
design -save read
hierarchy -top xilinx_srl_static_test
proc
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd xilinx_srl_static_test # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:SRL16E
select -assert-none t:BUFG t:SRL16E %% t:* %D
design -load read
hierarchy -top xilinx_srl_static_test
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nosrl # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd xilinx_srl_static_test # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 5 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_nowidelut.ys 0 → 100644
read_verilog ../top_dsp.v
design -save read
hierarchy -top top
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nodsp # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 12 t:LUT2
select -assert-count 1 t:LUT3
select -assert-count 6 t:LUT4
select -assert-count 1 t:LUT5
select -assert-count 33 t:LUT6
select -assert-count 11 t:MUXCY
select -assert-count 1 t:MUXF7
select -assert-count 12 t:XORCY
select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:XORCY %% t:* %D
design -load read
hierarchy -top top
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nodsp -nowidelut # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 10 t:LUT2
select -assert-count 6 t:LUT3
select -assert-count 5 t:LUT4
select -assert-count 2 t:LUT5
select -assert-count 32 t:LUT6
select -assert-count 11 t:MUXCY
select -assert-count 12 t:XORCY
select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:XORCY %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_nowidelut_abc9.ys 0 → 100644
read_verilog ../top_dsp.v
hierarchy -top top
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nodsp -nowidelut -abc9 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 3 t:CARRY4
select -assert-count 12 t:LUT2
select -assert-count 1 t:LUT3
select -assert-count 8 t:LUT4
select -assert-count 21 t:LUT5
select -assert-count 16 t:LUT6
select -assert-none t:CARRY4 t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_retime.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -retime # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -retime # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_run.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -run begin:blif # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -run begin:blif # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_top.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -top dff # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -top dffe # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_vpr.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -vpr # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -vpr # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_widemux.ys 0 → 100644
read_verilog ../top_mux.v
design -save read
hierarchy -top mux16
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -widemux 2 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux16 # Constrain all select calls below inside the top module
stat
select -assert-count 14 t:MUXF7
select -assert-count 1 t:MUXF8
select -assert-none t:MUXF7 t:MUXF8 %% t:* %D
design -load read
hierarchy -top mux16
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -widemux 3 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux16 # Constrain all select calls below inside the top module
stat
select -assert-count 4 t:LUT6
select -assert-count 2 t:MUXF7
select -assert-count 1 t:MUXF8
select -assert-none t:LUT6 t:MUXF7 t:MUXF8 %% t:* %D
design -load read
hierarchy -top mux16
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -widemux 5 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux16 # Constrain all select calls below inside the top module
stat
select -assert-count 4 t:LUT6
select -assert-count 2 t:MUXF7
select -assert-count 1 t:MUXF8
select -assert-none t:LUT6 t:MUXF7 t:MUXF8 %% t:* %D
design -load read
hierarchy -top mux16
proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -widemux 9 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux16 # Constrain all select calls below inside the top module
stat
select -assert-count 4 t:LUT6
select -assert-count 2 t:MUXF7
select -assert-count 1 t:MUXF8
select -assert-none t:LUT6 t:MUXF7 t:MUXF8 %% t:* %D
architecture_reviewed/synth_xilinx/synth_xilinx_widemux_1_fail.ys 0 → 100644
read_verilog ../top.v
synth_xilinx -widemux 1
architecture_reviewed/synth_xilinx/top.v 0 → 100644
module dff
( input d, clk, output reg q );
initial begin
q = 0;
end
always @( posedge clk )
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk)
if ( en )
q <= d;
endmodule
module adff
( 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
architecture_reviewed/synth_xilinx/top_bram.v 0 → 100644
// Single-Port Block RAM Read-First Mode
// rams_sp_rf.v
module top (clk, en, we, addr, di, dout);
input clk;
input we;
input en;
input [8:0] addr;
input [7:0] di;
output [7:0] dout;
reg [7:0] RAM [511:0];
reg [7:0] dout;
always @(posedge clk)
begin
if (en)
begin
if (we)
RAM[addr]<=di;
dout <= RAM[addr];
end
end
endmodule
architecture_reviewed/synth_xilinx/top_dpram.v 0 → 100644
/*
Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 72].
*/
module top (din, write_en, waddr, wclk, raddr, rclk, dout);
parameter addr_width = 6;
parameter data_width = 6;
input [addr_width-1:0] waddr, raddr;
input [data_width-1:0] din;
input write_en, wclk, rclk;
output [data_width-1:0] dout;
reg [data_width-1:0] dout;
reg [data_width-1:0] mem [(1<<addr_width)-1:0]
/* synthesis syn_ramstyle = "no_rw_check" */ ;
always @(posedge wclk) // Write memory.
begin
if (write_en)
mem[waddr] <= din; // Using write address bus.
end
always @(posedge rclk) // Read memory.
begin
dout <= mem[raddr]; // Using read address bus.
end
endmodule
architecture_reviewed/synth_xilinx/top_dsp.v 0 → 100644
module top
(
input [5:0] x,
input [5:0] y,
output [11:0] A,
);
assign A = x * y;
endmodule
architecture_reviewed/synth_xilinx/top_dsp_simd.v 0 → 100644
module simd(input [12*4-1:0] a, input [12*4-1:0] b, (* use_dsp="simd" *) output [7*12-1:0] o12, (* use_dsp="simd" *) output [2*24-1:0] o24);
generate
genvar i;
// 4 x 12-bit adder
for (i = 0; i < 4; i++)
assign o12[i*12+:12] = a[i*12+:12] + b[i*12+:12];
// 2 x 24-bit subtract
for (i = 0; i < 2; i++)
assign o24[i*24+:24] = a[i*24+:24] - b[i*24+:24];
endgenerate
reg [3*12-1:0] ro;
always @* begin
ro[0*12+:12] = a[0*10+:10] + b[0*10+:10];
ro[1*12+:12] = a[1*10+:10] + b[1*10+:10];
ro[2*12+:12] = a[2*8+:8] + b[2*8+:8];
end
assign o12[4*12+:3*12] = ro;
endmodule
architecture_reviewed/synth_xilinx/top_mux.v 0 → 100644
module mux16 (D, S, Y);
input [15:0] D;
input [3:0] S;
output Y;
assign Y = D[S];
endmodule
architecture_reviewed/synth_xilinx/top_nocarry.v 0 → 100644
module top
(
input [2:0] x,
input [2:0] y,
output [5:0] A,
);
assign A = x * y;
endmodule
architecture_reviewed/synth_xilinx/top_nosrl.v 0 → 100644
module xilinx_srl_static_test(input i, clk, output [1:0] q);
reg head = 1'b0;
reg [3:0] shift1 = 4'b0000;
reg [3:0] shift2 = 4'b0000;
always @(posedge clk) begin
head <= i;
shift1 <= {shift1[2:0], head};
shift2 <= {shift2[2:0], head};
end
assign q = {shift2[3], shift1[3]};
endmodule
architecture_reviewed/synth_xilinx/top_srl.v 0 → 100644
module top (
out,
out1,
clk,
in
);
output [7:0] out;
output [7:0] out1;
input signed clk, in;
reg signed [7:0] out;
reg signed [7:0] out1;
always @(posedge clk)
begin
out <= out >> 1;
out[7] <= in;
end
always @(posedge clk)
begin
out1 <= out1 >> 1;
out1[7] <= in;
end
endmodule
architecture_reviewed/synth_xilinx/top_wide_ffs.v 0 → 100644
module dff
( input [3:0] d, input clk, clr, output reg [3:0] q );
initial begin
q = 4'b0000;
end
always @( posedge clk )
if ( clr )
q <= 4'b0110;
else
q <= d;
endmodule
module adff
( input [3:0] d, input clk, clr, output reg [3:0] q );
initial begin
q = 4'b0000;
end
always @( posedge clk, posedge clr )
if ( clr )
q <= 4'b0110;
else
q <= d;
endmodule
module dffe
( input [3:0] d, input clk, en, output reg [3:0] q );
initial begin
q = 4'b0010;
end
always @( posedge clk)
if ( en )
q <= d;
endmodule
module dffse
( input [3:0] d, input clk, en, pre, output reg [3:0] q );
initial begin
q = 1;
end
always @( posedge clk )
if ( !pre )
q <= 4'b0101;
else
if ( en )
q <= d;
endmodule
architecture_reviewed/synth_xilinx/xilinx_srl.ys 0 → 100644
read_verilog ../top_srl.v
design -save read
hierarchy -top top
proc
synth_xilinx
xilinx_srl -fixed
stat
select -assert-count 1 t:BUFG
select -assert-count 8 t:FDRE
#select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read
hierarchy -top top
proc
synth_xilinx
xilinx_srl -fixed -minlen 1
stat
select -assert-count 8 t:$__XILINX_SHREG_
select -assert-count 1 t:BUFG
design -load read
hierarchy -top top
proc
synth_xilinx
xilinx_srl -fixed -variable
stat
select -assert-count 1 t:BUFG
select -assert-count 8 t:FDRE
design -load read
hierarchy -top top
proc
synth_xilinx
xilinx_srl -fixed -variable -minlen 1
stat
select -assert-count 8 t:$__XILINX_SHREG_
select -assert-count 1 t:BUFG
architecture_reviewed/synth_xilinx_dsp/assert_area.py 0 → 100755
#!/usr/bin/python3
import glob
import re
import os
re_mux = re.compile(r'(mul|muladd|macc)_(\d+)(s?)_(\d+)(s?)(_(\d+)(s?))?_(A?B?C?M?P?)_A?B?C?M?P?\.v')
for fn in glob.glob('*.v'):
m = re_mux.match(fn)
if not m: continue
macc = m.group(1) == 'macc'
muladd = m.group(1) == 'muladd'
A,B = map(int, m.group(2,4))
Asigned,Bsigned = m.group(3,5)
if m.group(6):
C = int(m.group(7))
Csigned = m.group(8)
else:
C = 0
Areg = 'A' in m.group(9)
Breg = 'B' in m.group(9)
Mreg = 'M' in m.group(9)
Preg = 'P' in m.group(9) or macc
if A < B:
A,B = B,A
Asigned,Bsigned = Bsigned,Asigned
if not (Asigned and Bsigned):
A += 1
B += 1
Asigned = Bsigned = 1
if C > 0 and not Csigned:
C += 1
Csigned = 1
X = 1 + max(0,A-25+16) // 17
Y = 1 + max(0,B-18+16) // 17
count_MAC = X * Y
count_DFF = 0
if Mreg and (A > 25 or B > 18):
count_DFF += A + B
if not macc and (A > 25) ^ (B > 18):
count_DFF -= 1 # For pure multipliers with just one big dimension,
# expect last slice to absorb at least one register
if Preg and (A > 25 or B > 18 or C > 48):
count_DFF += max(A + B, C)
if macc:
count_DFF += 5 # In my testcases, accumulator is always
# 5bits bigger than multiplier result
elif ((A > 25) ^ (B > 18)) and C <= 48:
count_DFF -= 1 # For pure multipliers with just one big dimension,
# expect last slice to absorb at least one register
# TODO: More assert on number of CARRY and LUTs
count_CARRY = ''
if macc or muladd:
if A <= 25 and B <= 18 and C <= 48:
count_CARRY = '; select t:XORCY -assert-none; select t:LUT* -assert-none';
elif A <= 25 or B <= 18:
count_CARRY = '; select t:XORCY -assert-none; select t:LUT* -assert-none';
bn,_ = os.path.splitext(fn)
with open(fn, 'a') as f:
print('''
`ifndef _AUTOTB
module __test ;
wire [4095:0] assert_area = "cd {0}; select t:DSP48E1 -assert-max {1}; select t:FD* -assert-max {2}{3}";
endmodule
`endif
'''.format(os.path.splitext(fn)[0], count_MAC, count_DFF, count_CARRY), file=f)
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