Skip to content

Y
yosys-tests
Commit 4b996cba by SergeyDegtyar
Options

Review and update tests for achronix,anlogic,coolrunner2,ecp5,efinix,gowin architectures.

parent 13009106
Showing with 2277 additions and 1 deletions
Makefile
SUBDIRS := architecture backends bigsim equiv frontends misc regression simple yosys
SUBDIRS := architecture architecture_reviewed backends bigsim equiv frontends misc regression simple yosys
ifeq ($(VERIFIC),1)
export VERIFIC=1
......
architecture_reviewed/Makefile 0 → 100644
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
#achronix
$(eval $(call template,synth_achronix,synth_achronix synth_achronix_top synth_achronix_vout synth_achronix_run synth_achronix_noflatten synth_achronix_retime synth_achronix_fail))
#anlogic
$(eval $(call template,synth_anlogic,synth_anlogic synth_anlogic_top synth_anlogic_edif synth_anlogic_json synth_anlogic_run synth_anlogic_noflatten synth_anlogic_retime synth_anlogic_fail synth_anlogic_fulladder anlogic_determine_init_eqn))
#coolrunner2
$(eval $(call template,synth_coolrunner2,synth_coolrunner2 synth_coolrunner2_top synth_coolrunner2_vout synth_coolrunner2_run synth_coolrunner2_noflatten synth_coolrunner2_retime synth_coolrunner2_fail synth_coolrunner2_for_lcov synth_coolrunner2_fulladder ))
$(eval $(call template,synth_coolrunner2_lcov,synth_coolrunner2 synth_coolrunner2_top synth_coolrunner2_vout synth_coolrunner2_run synth_coolrunner2_noflatten synth_coolrunner2_retime))
#easic - issue #920
# we do not have eTools anymore available, commented until aquired
#$(eval $(call template,synth_easic,synth_easic synth_easic_top synth_easic_vlog synth_easic_run synth_easic_noflatten synth_easic_retime synth_easic_fail))
$(eval $(call template,synth_easic, synth_easic_fail))
#ecp5
$(eval $(call template,synth_ecp5,synth_ecp5 synth_ecp5_top synth_ecp5_blif synth_ecp5_edif synth_ecp5_json synth_ecp5_run synth_ecp5_flatten synth_ecp5_noflatten synth_ecp5_retime synth_ecp5_noccu2 synth_ecp5_nodffe synth_ecp5_nobram synth_ecp5_nodram synth_ecp5_nomux synth_ecp5_abc2 synth_ecp5_vpr ecp5_ffinit synth_ecp5_abc9 synth_ecp5_abc9_nowidelut synth_ecp5_nodsp synth_ecp5_fail synth_ecp5_wide_ffs))
#efinix
$(eval $(call template,synth_efinix, synth_efinix synth_efinix_edif synth_efinix_json synth_efinix_noflatten synth_efinix_retime synth_efinix_run synth_efinix_top synth_efinix_fulladder))
#gowin
$(eval $(call template,synth_gowin,synth_gowin synth_gowin_top synth_gowin_vout synth_gowin_run synth_gowin_retime synth_gowin_nobram synth_gowin_noflatten synth_gowin_nodram synth_gowin_nodffe ))
.PHONY: all clean
architecture_reviewed/common.v 0 → 100644
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
architecture_reviewed/run.sh 0 → 100755
#!/bin/bash
set -x
test -d $1
test -f $2.ys
rm -rf $1/work_$2
mkdir $1/work_$2
cd $1/work_$2
touch .start
#
if [[ $2 =~ "_fail" ]]; then
#4 - An error expected
if yosys -ql yosys.log ../$2.ys; then
echo FAIL > ${1}_${2}.status
else
if [ -f "../$2.pat" ]; then
expectation=$(<../$2.pat)
if grep "$expectation" yosys.log; then
echo PASS > ${1}_${2}.status
else
echo FAIL > ${1}_${2}.status
fi
else
echo PASS > ${1}_${2}.status
fi
fi
else
#2 - All asserts in .ys script
yosys -ql yosys.log ../$2.ys
if [ $? != 0 ] ; then
echo FAIL > ${1}_${2}.status
touch .stamp
exit 0
else
#3 Output log check
if [ -f "../$2.pat" ]; then # Expected behavior
expectation=$(<../$2.pat)
if grep "$expectation" result.out; then
echo PASS > ${1}_${2}.status
else
echo FAIL > ${1}_${2}.status
fi
elif [ -f "../$2_n.pat" ]; then # Not expected behavior
expectation=$(<../$2_n.pat)
if grep "$expectation" result.out; then
echo FAIL > ${1}_${2}.status
else
echo PASS > ${1}_${2}.status
fi
#1 Iverilog run when testbench exists
elif [ -f "../testbench.v" ]; then
if [ -f "../../../../../techlibs/common/simcells.v" ]; then
COMMON_PREFIX=../../../../../techlibs/common
TECHLIBS_PREFIX=../../../../../techlibs
else
COMMON_PREFIX=/usr/local/share/yosys
TECHLIBS_PREFIX=/usr/local/share/yosys
fi
if [ -f "../iverilog_adds.txt" ]; then
iverilog_adds=$TECHLIBS_PREFIX/$(<../iverilog_adds.txt)
else
iverilog_adds=""
fi
iverilog -o testbench ../testbench.v synth.v ../../common.v $COMMON_PREFIX/simcells.v $COMMON_PREFIX/simlib.v $iverilog_adds
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
else
echo PASS > ${1}_${2}.status
fi
fi
fi
touch .stamp
architecture_reviewed/synth_achronix/synth_achronix.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
flatten
equiv_opt -assert -map +/achronix/speedster22i/cells_sim.v synth_achronix # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top
select -assert-count 2 t:LUT4
select -assert-count 3 t:PADIN
select -assert-count 2 t:PADOUT
select -assert-none t:LUT4 t:PADIN t:PADOUT %% t:* %D
architecture_reviewed/synth_achronix/synth_achronix_fail.pat 0 → 100644
ERROR: This command only operates on fully selected designs!
architecture_reviewed/synth_achronix/synth_achronix_fail.ys 0 → 100644
read_verilog ../top.v
select top2
synth_achronix
architecture_reviewed/synth_achronix/synth_achronix_noflatten.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
flatten
equiv_opt -assert -map +/achronix/speedster22i/cells_sim.v synth_achronix -noflatten # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top
select -assert-count 2 t:LUT4
select -assert-count 3 t:PADIN
select -assert-count 2 t:PADOUT
select -assert-none t:LUT4 t:PADIN t:PADOUT %% t:* %D
architecture_reviewed/synth_achronix/synth_achronix_retime.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
flatten
equiv_opt -assert -map +/achronix/speedster22i/cells_sim.v synth_achronix -retime # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top
select -assert-count 2 t:LUT4
select -assert-count 3 t:PADIN
select -assert-count 2 t:PADOUT
select -assert-none t:LUT4 t:PADIN t:PADOUT %% t:* %D
architecture_reviewed/synth_achronix/synth_achronix_run.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
flatten
equiv_opt -assert -map +/achronix/speedster22i/cells_sim.v synth_achronix -run begin:vout # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top
select -assert-count 2 t:LUT4
select -assert-count 3 t:PADIN
select -assert-count 2 t:PADOUT
select -assert-none t:LUT4 t:PADIN t:PADOUT %% t:* %D
architecture_reviewed/synth_achronix/synth_achronix_top.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
flatten
equiv_opt -assert -map +/achronix/speedster22i/cells_sim.v synth_achronix -top top # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top
select -assert-count 2 t:LUT4
select -assert-count 3 t:PADIN
select -assert-count 2 t:PADOUT
select -assert-none t:LUT4 t:PADIN t:PADOUT %% t:* %D
architecture_reviewed/synth_achronix/synth_achronix_vout.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
flatten
equiv_opt -assert -map +/achronix/speedster22i/cells_sim.v synth_achronix -vout vout.v # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top
select -assert-count 2 t:LUT4
select -assert-count 3 t:PADIN
select -assert-count 2 t:PADOUT
select -assert-none t:LUT4 t:PADIN t:PADOUT %% t:* %D
architecture_reviewed/synth_achronix/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output A,
output cout
);
assign {cout,A} = cin + y + x;
endmodule
architecture_reviewed/synth_anlogic/anlogic_determine_init_eqn.ys 0 → 100644
read_verilog ../top_mem.v
read_verilog -lib +/anlogic/cells_sim.v +/anlogic/eagle_bb.v
proc
flatten
tribuf -logic
deminout
synth -run coarse
memory_bram -rules +/anlogic/drams.txt
techmap -map +/anlogic/drams_map.v
#anlogic_determine_init
opt -fast -mux_undef -undriven -fine
memory_map
opt -undriven -fine
techmap -map +/techmap.v -map +/anlogic/arith_map.v
dffsr2dff
techmap -D NO_LUT -map +/anlogic/cells_map.v
dffinit -strinit SET RESET -ff AL_MAP_SEQ q REGSET -noreinit
opt_expr -mux_undef
simplemap
abc -lut 5
clean
techmap -map +/anlogic/cells_map.v
clean
anlogic_eqn
write_verilog synth.v
architecture_reviewed/synth_anlogic/synth_anlogic.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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
select -assert-count 1 t:AL_MAP_SEQ
select -assert-none t:AL_MAP_SEQ %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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
select -assert-count 1 t:AL_MAP_LUT3
select -assert-count 1 t:AL_MAP_SEQ
select -assert-none t:AL_MAP_LUT3 t:AL_MAP_SEQ %% t:* %D
architecture_reviewed/synth_anlogic/synth_anlogic_edif.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic -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
select -assert-count 1 t:AL_MAP_SEQ
select -assert-none t:AL_MAP_SEQ %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic -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
select -assert-count 1 t:AL_MAP_LUT3
select -assert-count 1 t:AL_MAP_SEQ
select -assert-none t:AL_MAP_LUT3 t:AL_MAP_SEQ %% t:* %D
architecture_reviewed/synth_anlogic/synth_anlogic_fail.pat 0 → 100644
ERROR: This command only operates on fully selected designs!
architecture_reviewed/synth_anlogic/synth_anlogic_fail.ys 0 → 100644
read_verilog ../top.v
select dffe
synth_anlogic
architecture_reviewed/synth_anlogic/synth_anlogic_fulladder.ys 0 → 100644
read_verilog ../top_fulladder.v
design -save read
hierarchy -top top
proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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
select -assert-count 7 t:AL_MAP_ADDER
select -assert-count 8 t:AL_MAP_LUT3
select -assert-none t:AL_MAP_ADDER t:AL_MAP_LUT3 %% t:* %D
architecture_reviewed/synth_anlogic/synth_anlogic_json.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic -json json.json # 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
select -assert-count 1 t:AL_MAP_SEQ
select -assert-none t:AL_MAP_SEQ %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic -json json.json # 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
select -assert-count 1 t:AL_MAP_LUT3
select -assert-count 1 t:AL_MAP_SEQ
select -assert-none t:AL_MAP_LUT3 t:AL_MAP_SEQ %% t:* %D
architecture_reviewed/synth_anlogic/synth_anlogic_noflatten.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic -noflatten # 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
select -assert-count 1 t:AL_MAP_SEQ
select -assert-none t:AL_MAP_SEQ %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic -noflatten # 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
select -assert-count 1 t:AL_MAP_LUT3
select -assert-count 1 t:AL_MAP_SEQ
select -assert-none t:AL_MAP_LUT3 t:AL_MAP_SEQ %% t:* %D
architecture_reviewed/synth_anlogic/synth_anlogic_retime.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic -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
select -assert-count 1 t:AL_MAP_SEQ
select -assert-none t:AL_MAP_SEQ %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic -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
select -assert-count 1 t:AL_MAP_LUT3
select -assert-count 1 t:AL_MAP_SEQ
select -assert-none t:AL_MAP_LUT3 t:AL_MAP_SEQ %% t:* %D
architecture_reviewed/synth_anlogic/synth_anlogic_run.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic -run begin:json # 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
select -assert-count 1 t:AL_MAP_SEQ
select -assert-none t:AL_MAP_SEQ %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic -run begin:json # 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
select -assert-count 1 t:AL_MAP_LUT3
select -assert-count 1 t:AL_MAP_SEQ
select -assert-none t:AL_MAP_LUT3 t:AL_MAP_SEQ %% t:* %D
architecture_reviewed/synth_anlogic/synth_anlogic_top.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic -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
select -assert-count 1 t:AL_MAP_SEQ
select -assert-none t:AL_MAP_SEQ %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic -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
select -assert-count 1 t:AL_MAP_LUT3
select -assert-count 1 t:AL_MAP_SEQ
select -assert-none t:AL_MAP_LUT3 t:AL_MAP_SEQ %% t:* %D
architecture_reviewed/synth_anlogic/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
architecture_reviewed/synth_anlogic/top_fulladder.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_anlogic/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_coolrunner2/synth_coolrunner2.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option skipped because of unproven cells
#equiv_opt -assert -map +/coolrunner2/cells_sim.v synth_coolrunner2 # equivalency check
equiv_opt -map +/coolrunner2/cells_sim.v synth_coolrunner2 # 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
select -assert-count 1 t:FDCP
select -assert-count 2 t:IBUF
select -assert-count 1 t:IOBUFE
select -assert-none t:FDCP t:IBUF t:IOBUFE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option skipped because of unproven cells
#equiv_opt -assert -map +/coolrunner2/cells_sim.v synth_coolrunner2 # equivalency check
equiv_opt -map +/coolrunner2/cells_sim.v synth_coolrunner2 # 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
select -assert-count 2 t:ANDTERM
select -assert-count 1 t:FDCP
select -assert-count 3 t:IBUF
select -assert-count 1 t:IOBUFE
select -assert-count 1 t:MACROCELL_XOR
select -assert-count 1 t:ORTERM
select -assert-none t:ANDTERM t:FDCP t:IBUF t:IOBUFE t:MACROCELL_XOR t:ORTERM %% t:* %D
architecture_reviewed/synth_coolrunner2/synth_coolrunner2_fail.pat 0 → 100644
ERROR: This command only operates on fully selected designs!
architecture_reviewed/synth_coolrunner2/synth_coolrunner2_fail.ys 0 → 100644
read_verilog ../top.v
select dffe
synth_coolrunner2
architecture_reviewed/synth_coolrunner2/synth_coolrunner2_for_lcov.ys 0 → 100644
read_verilog ../top.v
synth_coolrunner2 -retime
design -reset
read_verilog ../top.v
synth_coolrunner2 -noflatten
design -reset
read_verilog ../top.v
synth_coolrunner2 -top dff
design -reset
read_verilog ../top.v
synth_coolrunner2 -json json.json
design -reset
read_verilog ../top.v
synth_coolrunner2 -run begin:json
architecture_reviewed/synth_coolrunner2/synth_coolrunner2_fulladder.ys 0 → 100644
read_verilog ../top_fulladder.v
hierarchy -top top
proc
#-assert option skipped because of unproven cells
#equiv_opt -assert -map +/coolrunner2/cells_sim.v synth_coolrunner2 # equivalency check
equiv_opt -map +/coolrunner2/cells_sim.v synth_coolrunner2 # 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:ANDTERM
select -assert-count 3 t:IBUF
select -assert-count 2 t:IOBUFE
select -assert-count 2 t:MACROCELL_XOR
select -assert-count 2 t:ORTERM
select -assert-none t:ANDTERM t:IBUF t:IOBUFE t:MACROCELL_XOR t:ORTERM %% t:* %D
architecture_reviewed/synth_coolrunner2/synth_coolrunner2_noflatten.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option skipped because of unproven cells
#equiv_opt -assert -map +/coolrunner2/cells_sim.v synth_coolrunner2 -noflatten # equivalency check
equiv_opt -map +/coolrunner2/cells_sim.v synth_coolrunner2 # 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
select -assert-count 1 t:FDCP
select -assert-count 2 t:IBUF
select -assert-count 1 t:IOBUFE
select -assert-none t:FDCP t:IBUF t:IOBUFE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option skipped because of unproven cells
#equiv_opt -assert -map +/coolrunner2/cells_sim.v synth_coolrunner2 -noflatten # equivalency check
equiv_opt -map +/coolrunner2/cells_sim.v synth_coolrunner2 # 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
select -assert-count 2 t:ANDTERM
select -assert-count 1 t:FDCP
select -assert-count 3 t:IBUF
select -assert-count 1 t:IOBUFE
select -assert-count 1 t:MACROCELL_XOR
select -assert-count 1 t:ORTERM
select -assert-none t:ANDTERM t:FDCP t:IBUF t:IOBUFE t:MACROCELL_XOR t:ORTERM %% t:* %D
architecture_reviewed/synth_coolrunner2/synth_coolrunner2_retime.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option skipped because of unproven cells
#equiv_opt -assert -map +/coolrunner2/cells_sim.v synth_coolrunner2 -retime # equivalency check
equiv_opt -map +/coolrunner2/cells_sim.v synth_coolrunner2 # 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
select -assert-count 1 t:FDCP
select -assert-count 2 t:IBUF
select -assert-count 1 t:IOBUFE
select -assert-none t:FDCP t:IBUF t:IOBUFE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option skipped because of unproven cells
#equiv_opt -assert -map +/coolrunner2/cells_sim.v synth_coolrunner2 -retime # equivalency check
equiv_opt -map +/coolrunner2/cells_sim.v synth_coolrunner2 # 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
select -assert-count 2 t:ANDTERM
select -assert-count 1 t:FDCP
select -assert-count 3 t:IBUF
select -assert-count 1 t:IOBUFE
select -assert-count 1 t:MACROCELL_XOR
select -assert-count 1 t:ORTERM
select -assert-none t:ANDTERM t:FDCP t:IBUF t:IOBUFE t:MACROCELL_XOR t:ORTERM %% t:* %D
architecture_reviewed/synth_coolrunner2/synth_coolrunner2_run.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option skipped because of unproven cells
#equiv_opt -assert -map +/coolrunner2/cells_sim.v synth_coolrunner2 -run begin:json # equivalency check
equiv_opt -map +/coolrunner2/cells_sim.v synth_coolrunner2 # 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
select -assert-count 1 t:FDCP
select -assert-count 2 t:IBUF
select -assert-count 1 t:IOBUFE
select -assert-none t:FDCP t:IBUF t:IOBUFE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option skipped because of unproven cells
#equiv_opt -assert -map +/coolrunner2/cells_sim.v synth_coolrunner2 -run begin:json # equivalency check
equiv_opt -map +/coolrunner2/cells_sim.v synth_coolrunner2 # 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
select -assert-count 2 t:ANDTERM
select -assert-count 1 t:FDCP
select -assert-count 3 t:IBUF
select -assert-count 1 t:IOBUFE
select -assert-count 1 t:MACROCELL_XOR
select -assert-count 1 t:ORTERM
select -assert-none t:ANDTERM t:FDCP t:IBUF t:IOBUFE t:MACROCELL_XOR t:ORTERM %% t:* %D
architecture_reviewed/synth_coolrunner2/synth_coolrunner2_top.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option skipped because of unproven cells
#equiv_opt -assert -map +/coolrunner2/cells_sim.v synth_coolrunner2 -top dff # equivalency check
equiv_opt -map +/coolrunner2/cells_sim.v synth_coolrunner2 # 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
select -assert-count 1 t:FDCP
select -assert-count 2 t:IBUF
select -assert-count 1 t:IOBUFE
select -assert-none t:FDCP t:IBUF t:IOBUFE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option skipped because of unproven cells
#equiv_opt -assert -map +/coolrunner2/cells_sim.v synth_coolrunner2 -top dffe # equivalency check
equiv_opt -map +/coolrunner2/cells_sim.v synth_coolrunner2 # 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
select -assert-count 2 t:ANDTERM
select -assert-count 1 t:FDCP
select -assert-count 3 t:IBUF
select -assert-count 1 t:IOBUFE
select -assert-count 1 t:MACROCELL_XOR
select -assert-count 1 t:ORTERM
select -assert-none t:ANDTERM t:FDCP t:IBUF t:IOBUFE t:MACROCELL_XOR t:ORTERM %% t:* %D
architecture_reviewed/synth_coolrunner2/synth_coolrunner2_vout.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
#-assert option skipped because of unproven cells
#equiv_opt -assert -map +/coolrunner2/cells_sim.v synth_coolrunner2 -json json.json # equivalency check
equiv_opt -map +/coolrunner2/cells_sim.v synth_coolrunner2 # 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
select -assert-count 1 t:FDCP
select -assert-count 2 t:IBUF
select -assert-count 1 t:IOBUFE
select -assert-none t:FDCP t:IBUF t:IOBUFE %% t:* %D
design -load read
hierarchy -top dffe
proc
#-assert option skipped because of unproven cells
#equiv_opt -assert -map +/coolrunner2/cells_sim.v synth_coolrunner2 -json json.json # equivalency check
equiv_opt -map +/coolrunner2/cells_sim.v synth_coolrunner2 # 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
select -assert-count 2 t:ANDTERM
select -assert-count 1 t:FDCP
select -assert-count 3 t:IBUF
select -assert-count 1 t:IOBUFE
select -assert-count 1 t:MACROCELL_XOR
select -assert-count 1 t:ORTERM
select -assert-none t:ANDTERM t:FDCP t:IBUF t:IOBUFE t:MACROCELL_XOR t:ORTERM %% t:* %D
architecture_reviewed/synth_coolrunner2/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
architecture_reviewed/synth_coolrunner2/top_fulladder.v 0 → 100644
module top
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
architecture_reviewed/synth_coolrunner2_lcov/synth_coolrunner2_run.ys 0 → 100644
read_verilog ../top.v
synth_coolrunner2 -run begin:json
architecture_reviewed/synth_coolrunner2_lcov/synth_coolrunner2_top.ys 0 → 100644
read_verilog ../top.v
synth_coolrunner2 -top top
architecture_reviewed/synth_coolrunner2_lcov/synth_coolrunner2_vout.ys 0 → 100644
read_verilog ../top.v
synth_coolrunner2 -json json.json
architecture_reviewed/synth_coolrunner2_lcov/top.v 0 → 100644
module adff
( input d, clk, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
module adffn
( input d, clk, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, negedge clr )
if ( !clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge en )
if ( en )
`ifndef BUG
q <= d;
`else
q <= 1'b0;
`endif
endmodule
module dffsr
( input d, clk, pre, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge pre, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if ( pre )
q <= 1'b1;
else
q <= d;
endmodule
module ndffnsnr
( input d, clk, pre, clr, output reg q );
initial begin
q = 0;
end
always @( negedge clk, negedge pre, negedge clr )
if ( !clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if ( !pre )
q <= 1'b1;
else
q <= d;
endmodule
module top (
input clk,
input clr,
input pre,
input a,
output b,b1,b2,b3,b4
);
dffsr u_dffsr (
.clk (clk ),
.clr (clr),
.pre (pre),
.d (a ),
.q (b )
);
ndffnsnr u_ndffnsnr (
.clk (clk ),
.clr (clr),
.pre (pre),
.d (a ),
.q (b1 )
);
adff u_adff (
.clk (clk ),
.clr (clr),
.d (a ),
.q (b2 )
);
adffn u_adffn (
.clk (clk ),
.clr (clr),
.d (a ),
.q (b3 )
);
dffe u_dffe (
.clk (clk ),
.en (clr),
.d (a ),
.q (b4 )
);
endmodule
architecture_reviewed/synth_easic/synth_easic.ys 0 → 100644
read_verilog ../top.v
synth_easic
write_verilog synth.v
architecture_reviewed/synth_easic/synth_easic_etools.ys 0 → 100644
read_verilog ../top.v
synth_easic -etools
write_verilog synth.v
architecture_reviewed/synth_easic/synth_easic_fail.pat 0 → 100644
ERROR: This command only operates on fully selected designs!
architecture_reviewed/synth_easic/synth_easic_fail.ys 0 → 100644
read_verilog ../top.v
select dffe
synth_easic
architecture_reviewed/synth_easic/synth_easic_noflatten.ys 0 → 100644
read_verilog ../top.v
synth_easic -noflatten
write_verilog synth.v
architecture_reviewed/synth_easic/synth_easic_retime.ys 0 → 100644
read_verilog ../top.v
synth_easic -retime
write_verilog synth.v
architecture_reviewed/synth_easic/synth_easic_run.ys 0 → 100644
read_verilog ../top.v
synth_easic -run begin:vlog
write_verilog synth.v
architecture_reviewed/synth_easic/synth_easic_top.ys 0 → 100644
read_verilog ../top.v
synth_easic -top top
write_verilog synth.v
architecture_reviewed/synth_easic/testbench.v 0 → 100644
module testbench;
reg clk;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 clk = 0;
repeat (10000) begin
#5 clk = 1;
#5 clk = 0;
end
$display("OKAY");
end
reg [2:0] dinA = 0;
wire doutB,doutB1,doutB2,doutB3,doutB4;
reg dff,ndff,adff,adffn,dffe = 0;
top uut (
.clk (clk ),
.a (dinA[0] ),
.pre (dinA[1] ),
.clr (dinA[2] ),
.b (doutB ),
.b1 (doutB1 ),
.b2 (doutB2 ),
.b3 (doutB3 ),
.b4 (doutB4 )
);
always @(posedge clk) begin
#3;
dinA <= dinA + 1;
end
always @( posedge clk, posedge dinA[1], posedge dinA[2] )
if ( dinA[2] )
dff <= 1'b0;
else if ( dinA[1] )
dff <= 1'b1;
else
dff <= dinA[0];
always @( negedge clk, negedge dinA[1], negedge dinA[2] )
if ( !dinA[2] )
ndff <= 1'b0;
else if ( !dinA[1] )
ndff <= 1'b1;
else
ndff <= dinA[0];
always @( posedge clk, posedge dinA[2] )
if ( dinA[2] )
adff <= 1'b0;
else
adff <= dinA[0];
always @( posedge clk, negedge dinA[2] )
if ( !dinA[2] )
adffn <= 1'b0;
else
adffn <= dinA[0];
always @( posedge clk, posedge dinA[2] )
if ( dinA[2] )
dffe <= dinA[0];
assert_dff dff_test(.clk(clk), .test(doutB), .pat(dff));
assert_dff ndff_test(.clk(clk), .test(doutB1), .pat(ndff));
assert_dff adff_test(.clk(clk), .test(doutB2), .pat(adff));
assert_dff adffn_test(.clk(clk), .test(doutB3), .pat(adffn));
assert_dff dffe_test(.clk(clk), .test(doutB4), .pat(dffe));
endmodule
architecture_reviewed/synth_easic/top.v 0 → 100644
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
module adffn
( input d, clk, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, negedge clr )
if ( !clr )
q <= 1'b0;
else
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge en )
if ( en )
q <= d;
endmodule
module dffsr
( input d, clk, pre, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge pre, posedge clr )
if ( clr )
q <= 1'b0;
else if ( pre )
q <= 1'b1;
else
q <= d;
endmodule
module ndffnsnr
( input d, clk, pre, clr, output reg q );
initial begin
q = 0;
end
always @( negedge clk, negedge pre, negedge clr )
if ( !clr )
q <= 1'b0;
else if ( !pre )
q <= 1'b1;
else
q <= d;
endmodule
module top (
input clk,
input clr,
input pre,
input a,
output b,b1,b2,b3,b4
);
dffsr u_dffsr (
.clk (clk ),
.clr (clr),
.pre (pre),
.d (a ),
.q (b )
);
ndffnsnr u_ndffnsnr (
.clk (clk ),
.clr (clr),
.pre (pre),
.d (a ),
.q (b1 )
);
adff u_adff (
.clk (clk ),
.clr (clr),
.d (a ),
.q (b2 )
);
adffn u_adffn (
.clk (clk ),
.clr (clr),
.d (a ),
.q (b3 )
);
dffe u_dffe (
.clk (clk ),
.en (clr),
.d (a ),
.q (b4 )
);
endmodule
architecture_reviewed/synth_ecp5/ecp5_ffinit.ys 0 → 100644
read_verilog ../top.v
read_verilog -lib +/ecp5/cells_sim.v +/ecp5/cells_bb.v
proc
flatten
tribuf -logic
deminout
synth -run coarse
memory_bram -rules +/ecp5/bram.txt
techmap -map +/ecp5/brams_map.v
opt -fast -mux_undef -undriven -fine
techmap -map +/techmap.v -map +/ecp5/arith_map.v
abc -dff
opt -fast -mux_undef -undriven -fine
dff2dffe -direct-match $_DFF_* -direct-match $__DFFS_*
techmap -D NO_LUT -map +/ecp5/cells_map.v
opt_expr -mux_undef
simplemap
ecp5_ffinit
write_verilog synth.v
architecture_reviewed/synth_ecp5/synth_ecp5.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_abc2.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -abc2 # 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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -abc2 # 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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_abc9.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_abc9_nowidelut.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -abc9 -nowidelut # 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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -abc9 -nowidelut # 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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_blif.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_edif.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_fail.pat 0 → 100644
ERROR: This command only operates on fully selected designs!
architecture_reviewed/synth_ecp5/synth_ecp5_fail.ys 0 → 100644
read_verilog ../top.v
select dffe
synth_ecp5
architecture_reviewed/synth_ecp5/synth_ecp5_flatten.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_json.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -json json.json # 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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -json json.json # 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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_nobram.ys 0 → 100644
read_verilog ../top_dpram.v
design -save read
hierarchy -top top
proc
memory -nomap
equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
#Blocked by issue #1358 (Missing ECP5 simulation models)
#ERROR: Failed to import cell gate.mem.0.0.0 (type DP16KD) to SAT database.
#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd top
select -assert-count 1 t:DP16KD
select -assert-none t:DP16KD %% t:* %D
design -load read
hierarchy -top top
proc
memory -nomap
equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5 -nobram
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
#Blocked by issue #1358 (Missing ECP5 simulation models)
#ERROR: Failed to import cell gate.mem.0.0.0 (type DP16KD) to SAT database.
#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd top
select -assert-count 144 t:LUT4
select -assert-count 17 t:PFUMX
select -assert-count 32 t:TRELLIS_DPR16X4
select -assert-count 143 t:TRELLIS_FF
select -assert-none t:LUT4 t:PFUMX t:TRELLIS_DPR16X4 t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_noccu2.ys 0 → 100644
read_verilog ../top_counter.v
design -save read
hierarchy -top top
proc
equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # 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 4 t:CCU2C
select -assert-count 8 t:TRELLIS_FF
select -assert-none t:CCU2C t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top top
proc
equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 -noccu2 # 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:LUT4
select -assert-count 1 t:PFUMX
select -assert-count 8 t:TRELLIS_FF
select -assert-none t:LUT4 t:PFUMX t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_nodffe.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -nodffe # 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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -nodffe # 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:LUT4
select -assert-count 1 t:TRELLIS_FF
select -assert-none t:TRELLIS_FF t:LUT4 %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_nodram.ys 0 → 100644
read_verilog ../top_dpram.v
hierarchy -top top
proc
memory -nomap
equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5 -nodram
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
#Blocked by issue #1358 (Missing ECP5 simulation models)
#ERROR: Failed to import cell gate.mem.0.0.0 (type DP16KD) to SAT database.
#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd top
select -assert-count 1 t:DP16KD
select -assert-none t:DP16KD %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_nodsp.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -nodsp # 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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -nodsp # 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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_noflatten.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -noflatten # 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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -noflatten # 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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_nomux.ys 0 → 100644
read_verilog ../top_mux.v
design -save read
hierarchy -top mux8
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux8 # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:L6MUX21
select -assert-count 7 t:LUT4
select -assert-count 2 t:PFUMX
select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D
design -load read
hierarchy -top mux8
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -nomux # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux8 # Constrain all select calls below inside the top module
stat
select -assert-count 5 t:LUT4
select -assert-none t:LUT4 %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_retime.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_run.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -run begin:json # 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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -run begin:json # 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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_top.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_vpr.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 -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:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
architecture_reviewed/synth_ecp5/synth_ecp5_wide_ffs.ys 0 → 100644
read_verilog ../top_wide_ffs.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 2 t:LUT4
select -assert-count 4 t:TRELLIS_FF
select -assert-none t:LUT4 t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 4 t:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top adff
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # 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 4 t:TRELLIS_FF
select -assert-none t:TRELLIS_FF %% t:* %D
design -load read
hierarchy -top dffsr
proc
flatten
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffsr # Constrain all select calls below inside the top module
stat
select -assert-count 4 t:TRELLIS_FF
select -assert-count 5 t:LUT4
select -assert-none t:TRELLIS_FF t:LUT4 %% t:* %D
write_verilog synth.v
architecture_reviewed/synth_ecp5/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_ecp5/top_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
architecture_reviewed/synth_ecp5/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 = 8;
parameter data_width = 8;
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_ecp5/top_mux.v 0 → 100644
module mux2 (S,A,B,Y);
input S;
input A,B;
output reg Y;
always @(*)
Y = (S)? B : A;
endmodule
module mux4 ( S, D, Y );
input[1:0] S;
input[3:0] D;
output Y;
reg Y;
wire[1:0] S;
wire[3:0] D;
always @*
begin
case( S )
0 : Y = D[0];
1 : Y = D[1];
2 : Y = D[2];
3 : Y = D[3];
endcase
end
endmodule
module mux8 ( 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
module mux16 (D, S, Y);
input [15:0] D;
input [3:0] S;
output Y;
assign Y = D[S];
endmodule
architecture_reviewed/synth_ecp5/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 dffsr
( 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_efinix/synth_efinix.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
select -assert-count 1 t:EFX_LUT4
select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D
architecture_reviewed/synth_efinix/synth_efinix_edif.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -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:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -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:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
select -assert-count 1 t:EFX_LUT4
select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D
architecture_reviewed/synth_efinix/synth_efinix_fulladder.ys 0 → 100644
read_verilog ../top_.v
hierarchy -top top
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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_edif.ys 0 → 100644
read_verilog ../top_fulladder.v
hierarchy -top top
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -edif edif.edif # 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_json.ys 0 → 100644
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 0 → 100644
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 0 → 100644
read_verilog ../top_fulladder.v
hierarchy -top top
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -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 2 t:EFX_LUT4
select -assert-none t:EFX_LUT4 %% t:* %D
architecture_reviewed/synth_efinix/synth_efinix_fulladder_run.ys 0 → 100644
read_verilog ../top_fulladder.v
hierarchy -top top
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -run begin: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 2 t:EFX_LUT4
select -assert-none t:EFX_LUT4 %% t:* %D
architecture_reviewed/synth_efinix/synth_efinix_fulladder_top.ys 0 → 100644
read_verilog ../top_fulladder.v
hierarchy -top top
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -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 2 t:EFX_LUT4
select -assert-none t:EFX_LUT4 %% t:* %D
architecture_reviewed/synth_efinix/synth_efinix_json.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
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 dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D
design -load read
hierarchy -top dffe
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 dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
select -assert-count 1 t:EFX_LUT4
select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D
architecture_reviewed/synth_efinix/synth_efinix_noflatten.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
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 dff # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D
design -load read
hierarchy -top dffe
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 dffe # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
select -assert-count 1 t:EFX_LUT4
select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D
architecture_reviewed/synth_efinix/synth_efinix_retime.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -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:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -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:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
select -assert-count 1 t:EFX_LUT4
select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D
architecture_reviewed/synth_efinix/synth_efinix_run.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -run begin:json # 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:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -run begin:json # 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:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
select -assert-count 1 t:EFX_LUT4
select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D
architecture_reviewed/synth_efinix/synth_efinix_top.ys 0 → 100644
read_verilog ../top.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -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:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix -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:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
select -assert-count 1 t:EFX_LUT4
select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D
architecture_reviewed/synth_efinix/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
architecture_reviewed/synth_efinix/top_fulladder.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_gowin/synth_gowin.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
equiv_opt -assert -map +/gowin/cells_sim.v synth_gowin # 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
select -assert-count 6 t:ALU
select -assert-count 15 t:GND
select -assert-count 12 t:IBUF
select -assert-count 8 t:LUT3
select -assert-count 10 t:OBUF
select -assert-none t:ALU t:GND t:IBUF t:LUT3 t:OBUF %% t:* %D
architecture_reviewed/synth_gowin/synth_gowin_fail.pat 0 → 100644
ERROR: This command only operates on fully selected designs!
architecture_reviewed/synth_gowin/synth_gowin_fail.ys 0 → 100644
read_verilog ../top.v
select top2
synth_gowin
architecture_reviewed/synth_gowin/synth_gowin_nobram.ys 0 → 100644
read_verilog ../top_mem.v
hierarchy -top top
proc
memory -nomap
equiv_opt -run :prove -map +/gowin/cells_sim.v synth_gowin -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
stat
select -assert-count 35 t:DFF
select -assert-count 16 t:IBUF
select -assert-count 6 t:LUT2
select -assert-count 1 t:LUT3
select -assert-count 24 t:LUT4
select -assert-count 8 t:OBUF
select -assert-count 8 t:RAM16S4
select -assert-none t:DFF t:IBUF t:LUT2 t:LUT3 t:LUT4 t:OBUF t:RAM16S4 %% t:* %D
architecture_reviewed/synth_gowin/synth_gowin_nodffe.ys 0 → 100644
read_verilog ../top_dffe.v
design -save read
hierarchy -top top
proc
#-assert option was skipped because of unproven cells
#equiv_opt -assert -map +/gowin/cells_sim.v synth_gowin # equivalency check
equiv_opt -map +/gowin/cells_sim.v synth_gowin # 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:$_DFFE_PP_
select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:$_DFFE_PP_ t:IBUF t:OBUF %% t:* %D
design -load read
hierarchy -top top
proc
#-assert option was skipped because of unproven cells
equiv_opt -assert -map +/gowin/cells_sim.v synth_gowin -nodffe # equivalency check
#equiv_opt -map +/gowin/cells_sim.v synth_gowin -nodffe # 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:DFF
select -assert-count 3 t:IBUF
select -assert-count 1 t:LUT3
select -assert-count 1 t:OBUF
select -assert-none t:DFF t:IBUF t:LUT3 t:OBUF %% t:* %D
architecture_reviewed/synth_gowin/synth_gowin_nodram.ys 0 → 100644
read_verilog ../top_mem.v
design -save read
hierarchy -top top
proc
memory -nomap
equiv_opt -run :prove -map +/gowin/cells_sim.v synth_gowin
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
stat
select -assert-count 35 t:DFF
select -assert-count 16 t:IBUF
select -assert-count 6 t:LUT2
select -assert-count 1 t:LUT3
select -assert-count 24 t:LUT4
select -assert-count 8 t:OBUF
select -assert-count 8 t:RAM16S4
select -assert-none t:DFF t:IBUF t:LUT2 t:LUT3 t:LUT4 t:OBUF t:RAM16S4 %% t:* %D
design -load read
hierarchy -top top
proc
memory -nomap
equiv_opt -run :prove -map +/gowin/cells_sim.v synth_gowin -nodram -nodffe
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
stat
select -assert-count 520 t:DFF
select -assert-count 16 t:IBUF
select -assert-count 9 t:LUT2
select -assert-count 622 t:LUT3
select -assert-count 345 t:LUT4
select -assert-count 8 t:OBUF
select -assert-none t:DFF t:IBUF t:LUT2 t:LUT3 t:LUT4 t:OBUF %% t:* %D
architecture_reviewed/synth_gowin/synth_gowin_noflatten.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
equiv_opt -assert -map +/gowin/cells_sim.v synth_gowin -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
select -assert-count 6 t:ALU
select -assert-count 15 t:GND
select -assert-count 12 t:IBUF
select -assert-count 8 t:LUT3
select -assert-count 10 t:OBUF
select -assert-none t:ALU t:GND t:IBUF t:LUT3 t:OBUF %% t:* %D
architecture_reviewed/synth_gowin/synth_gowin_retime.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
equiv_opt -assert -map +/gowin/cells_sim.v synth_gowin -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
select -assert-count 6 t:ALU
select -assert-count 15 t:GND
select -assert-count 12 t:IBUF
select -assert-count 8 t:LUT3
select -assert-count 10 t:OBUF
select -assert-none t:ALU t:GND t:IBUF t:LUT3 t:OBUF %% t:* %D
architecture_reviewed/synth_gowin/synth_gowin_run.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
equiv_opt -assert -map +/gowin/cells_sim.v synth_gowin -run begin:vout # 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
select -assert-count 6 t:ALU
select -assert-count 15 t:GND
select -assert-count 12 t:IBUF
select -assert-count 8 t:LUT3
select -assert-count 10 t:OBUF
select -assert-none t:ALU t:GND t:IBUF t:LUT3 t:OBUF %% t:* %D
architecture_reviewed/synth_gowin/synth_gowin_top.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
equiv_opt -assert -map +/gowin/cells_sim.v synth_gowin -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
select -assert-count 6 t:ALU
select -assert-count 15 t:GND
select -assert-count 12 t:IBUF
select -assert-count 8 t:LUT3
select -assert-count 10 t:OBUF
select -assert-none t:ALU t:GND t:IBUF t:LUT3 t:OBUF %% t:* %D
architecture_reviewed/synth_gowin/synth_gowin_vout.ys 0 → 100644
read_verilog ../top.v
hierarchy -top top
proc
equiv_opt -assert -map +/gowin/cells_sim.v synth_gowin -vout vout.v # 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
select -assert-count 6 t:ALU
select -assert-count 15 t:GND
select -assert-count 12 t:IBUF
select -assert-count 8 t:LUT3
select -assert-count 10 t:OBUF
select -assert-none t:ALU t:GND t:IBUF t:LUT3 t:OBUF %% t:* %D
architecture_reviewed/synth_gowin/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_gowin/top_dffe.v 0 → 100644
module top
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk)
if ( en )
q <= d;
endmodule
architecture_reviewed/synth_gowin/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
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