mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 03:32:29 +00:00
Code Activity

intel_alm: Add global buffer insertion

Browse source 
Signed-off-by: gatecat <gatecat@ds0.me>
This commit is contained in:
gatecat 2021-05-15 14:34:48 +01:00
parent 5dba138c87
commit eb106732d9
19 changed files with 119 additions and 45 deletions
Download patch file Download diff file Expand all files Collapse all files

4
techlibs/intel_alm/common/dff_sim.v
View file

@ -56,7 +56,9 @@
(* abc9_box, lib_whitebox *) (* abc9_box, lib_whitebox *)
module MISTRAL_FF( module MISTRAL_FF(
input DATAIN, CLK, ACLR, ENA, SCLR, SLOAD, SDATA, input DATAIN,
(* clkbuf_sink *) input CLK,
input ACLR, ENA, SCLR, SLOAD, SDATA,
output reg Q output reg Q
); );

35
techlibs/intel_alm/common/megafunction_bb.v
View file

@ -662,3 +662,38 @@ input [15:0] parallelterminationcontrol;
(* iopad_external_pin *) output obar; (* iopad_external_pin *) output obar;
endmodule endmodule
(* blackbox *)
module cyclonev_clkena(inclk, ena, enaout, outclk);
parameter clock_type = "auto";
parameter ena_register_mode = "always enabled";
parameter lpm_type = "cyclonev_clkena";
parameter ena_register_power_up = "high";
parameter disable_mode = "low";
parameter test_syn = "high";
input inclk;
input ena;
output enaout;
output outclk;
endmodule
(* blackbox *)
module cyclone10gx_clkena(inclk, ena, enaout, outclk);
parameter clock_type = "auto";
parameter ena_register_mode = "always enabled";
parameter lpm_type = "cyclone10gx_clkena";
parameter ena_register_power_up = "high";
parameter disable_mode = "low";
parameter test_syn = "high";
input inclk;
input ena;
output enaout;
output outclk;
endmodule

6
techlibs/intel_alm/common/mem_sim.v
View file

@ -50,7 +50,9 @@
// model can be treated as always returning a defined result. // model can be treated as always returning a defined result.
(* abc9_box, lib_whitebox *) (* abc9_box, lib_whitebox *)
module MISTRAL_MLAB(input [4:0] A1ADDR, input A1DATA, A1EN, CLK1, input [4:0] B1ADDR, output B1DATA); module MISTRAL_MLAB(input [4:0] A1ADDR, input A1DATA, A1EN,
(* clkbuf_sink *) input CLK1,
input [4:0] B1ADDR, output B1DATA);
reg [31:0] mem = 32'b0; reg [31:0] mem = 32'b0;
@ -83,7 +85,7 @@ module MISTRAL_M10K(CLK1, A1ADDR, A1DATA, A1EN, B1ADDR, B1DATA, B1EN);
parameter CFG_ABITS = 10; parameter CFG_ABITS = 10;
parameter CFG_DBITS = 10; parameter CFG_DBITS = 10;
input CLK1; (* clkbuf_sink *) input CLK1;
input [CFG_ABITS-1:0] A1ADDR, B1ADDR; input [CFG_ABITS-1:0] A1ADDR, B1ADDR;
input [CFG_DBITS-1:0] A1DATA; input [CFG_DBITS-1:0] A1DATA;
input A1EN, B1EN; input A1EN, B1EN;

9
techlibs/intel_alm/common/misc_sim.v
View file

@ -10,3 +10,12 @@ module MISTRAL_IO((* iopad_external_pin *) inout PAD, input I, input OE, output
assign PAD = OE ? I : 1'bz; assign PAD = OE ? I : 1'bz;
assign O = PAD; assign O = PAD;
endmodule endmodule
// Eventually, we should support clock enables and model them here too.
// For now, CLKENA is used as a basic entry point to global routing.
module MISTRAL_CLKBUF (
input A,
(* clkbuf_driver *) output Q
);
assign Q = A;
endmodule

16
techlibs/intel_alm/common/quartus_rename.v
View file

@ -4,6 +4,7 @@
`define MLAB cyclonev_mlab_cell `define MLAB cyclonev_mlab_cell
`define IBUF cyclonev_io_ibuf `define IBUF cyclonev_io_ibuf
`define OBUF cyclonev_io_obuf `define OBUF cyclonev_io_obuf
`define CLKENA cyclonev_clkena
`endif `endif
`ifdef cyclone10gx `ifdef cyclone10gx
`define LCELL cyclone10gx_lcell_comb `define LCELL cyclone10gx_lcell_comb
@ -11,6 +12,7 @@
`define MLAB cyclone10gx_mlab_cell `define MLAB cyclone10gx_mlab_cell
`define IBUF cyclone10gx_io_ibuf `define IBUF cyclone10gx_io_ibuf
`define OBUF cyclone10gx_io_obuf `define OBUF cyclone10gx_io_obuf
`define CLKENA cyclone10gx_clkena
`endif `endif
module __MISTRAL_VCC(output Q); module __MISTRAL_VCC(output Q);
@ -277,3 +279,17 @@ module MISTRAL_IO(output PAD, input I, OE, output O);
.oe(OE) .oe(OE)
); );
endmodule endmodule
module MISTRAL_CLKBUF (input A, output Q);
`CLKENA #(
.clock_type("auto"),
.ena_register_mode("always enabled"),
.ena_register_power_up("high"),
.disable_mode("low"),
.test_syn("high")
) _TECHMAP_REPLACE_ (
.inclk(A),
.ena(1'b1),
.outclk(Q)
);
endmodule

12
techlibs/intel_alm/synth_intel_alm.cc
View file

@ -75,13 +75,16 @@ struct SynthIntelALMPass : public ScriptPass {
log(" -noiopad\n"); log(" -noiopad\n");
log(" do not instantiate IO buffers\n"); log(" do not instantiate IO buffers\n");
log("\n"); log("\n");
log(" -noclkbuf\n");
log(" do not insert global clock buffers\n");
log("\n");
log("The following commands are executed by this synthesis command:\n"); log("The following commands are executed by this synthesis command:\n");
help_script(); help_script();
log("\n"); log("\n");
} }
string top_opt, family_opt, bram_type, vout_file; string top_opt, family_opt, bram_type, vout_file;
bool flatten, quartus, nolutram, nobram, dff, nodsp, noiopad; bool flatten, quartus, nolutram, nobram, dff, nodsp, noiopad, noclkbuf;
void clear_flags() override void clear_flags() override
{ {
@ -96,6 +99,7 @@ struct SynthIntelALMPass : public ScriptPass {
dff = false; dff = false;
nodsp = false; nodsp = false;
noiopad = false; noiopad = false;
noclkbuf = false;
} }
void execute(std::vector<std::string> args, RTLIL::Design *design) override void execute(std::vector<std::string> args, RTLIL::Design *design) override
@ -154,6 +158,10 @@ struct SynthIntelALMPass : public ScriptPass {
noiopad = true; noiopad = true;
continue; continue;
} }
if (args[argidx] == "-noclkbuf") {
noclkbuf = true;
continue;
}
break; break;
} }
extra_args(args, argidx, design); extra_args(args, argidx, design);
@ -268,6 +276,8 @@ struct SynthIntelALMPass : public ScriptPass {
run("techmap -map +/intel_alm/common/dff_map.v"); run("techmap -map +/intel_alm/common/dff_map.v");
run("opt -full -undriven -mux_undef"); run("opt -full -undriven -mux_undef");
run("clean -purge"); run("clean -purge");
if (!noclkbuf)
run("clkbufmap -buf MISTRAL_CLKBUF Q:A", "(unless -noclkbuf)");
} }
if (check_label("map_luts")) { if (check_label("map_luts")) {

4
tests/arch/intel_alm/add_sub.ys
View file

@ -1,6 +1,6 @@
read_verilog ../common/add_sub.v read_verilog ../common/add_sub.v
hierarchy -top top hierarchy -top top
equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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
@ -10,7 +10,7 @@ select -assert-none t:MISTRAL_ALUT_ARITH %% t:* %D
design -reset design -reset
read_verilog ../common/add_sub.v read_verilog ../common/add_sub.v
hierarchy -top top hierarchy -top top
equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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

16
tests/arch/intel_alm/adffs.ys
View file

@ -3,7 +3,7 @@ design -save read
hierarchy -top adff hierarchy -top adff
proc proc
equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 adff # Constrain all select calls below inside the top module cd adff # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_FF select -assert-count 1 t:MISTRAL_FF
@ -15,7 +15,7 @@ select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D
design -load read design -load read
hierarchy -top adff hierarchy -top adff
proc proc
equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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 adff # Constrain all select calls below inside the top module cd adff # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_FF select -assert-count 1 t:MISTRAL_FF
@ -27,7 +27,7 @@ select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D
design -load read design -load read
hierarchy -top adffn hierarchy -top adffn
proc proc
equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 adffn # Constrain all select calls below inside the top module cd adffn # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_FF select -assert-count 1 t:MISTRAL_FF
@ -38,7 +38,7 @@ select -assert-none t:MISTRAL_FF %% t:* %D
design -load read design -load read
hierarchy -top adffn hierarchy -top adffn
proc proc
equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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 adffn # Constrain all select calls below inside the top module cd adffn # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_FF select -assert-count 1 t:MISTRAL_FF
@ -49,7 +49,7 @@ select -assert-none t:MISTRAL_FF %% t:* %D
design -load read design -load read
hierarchy -top dffs hierarchy -top dffs
proc proc
equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 dffs # Constrain all select calls below inside the top module cd dffs # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_FF select -assert-count 1 t:MISTRAL_FF
@ -61,7 +61,7 @@ select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 %% t:* %D
design -load read design -load read
hierarchy -top dffs hierarchy -top dffs
proc proc
equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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 dffs # Constrain all select calls below inside the top module cd dffs # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_FF select -assert-count 1 t:MISTRAL_FF
@ -73,7 +73,7 @@ select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 %% t:* %D
design -load read design -load read
hierarchy -top ndffnr hierarchy -top ndffnr
proc proc
equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 ndffnr # Constrain all select calls below inside the top module cd ndffnr # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_FF select -assert-count 1 t:MISTRAL_FF
@ -85,7 +85,7 @@ select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D
design -load read design -load read
hierarchy -top ndffnr hierarchy -top ndffnr
proc proc
equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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 ndffnr # Constrain all select calls below inside the top module cd ndffnr # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_FF select -assert-count 1 t:MISTRAL_FF

2
tests/arch/intel_alm/blockram.ys
View file

@ -1,6 +1,6 @@
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 10 sync_ram_sdp chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 10 sync_ram_sdp
synth_intel_alm -family cyclonev -noiopad synth_intel_alm -family cyclonev -noiopad -noclkbuf
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:MISTRAL_M10K select -assert-count 1 t:MISTRAL_M10K
select -assert-none t:MISTRAL_M10K %% t:* %D select -assert-none t:MISTRAL_M10K %% t:* %D

4
tests/arch/intel_alm/counter.ys
View file

@ -2,7 +2,7 @@ read_verilog ../common/counter.v
hierarchy -top top hierarchy -top top
proc proc
flatten flatten
equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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
@ -17,7 +17,7 @@ read_verilog ../common/counter.v
hierarchy -top top hierarchy -top top
proc proc
flatten flatten
equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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

8
tests/arch/intel_alm/dffs.ys
View file

@ -3,7 +3,7 @@ design -save read
hierarchy -top dff hierarchy -top dff
proc proc
equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 dff # Constrain all select calls below inside the top module cd dff # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_FF select -assert-count 1 t:MISTRAL_FF
@ -13,7 +13,7 @@ select -assert-none t:MISTRAL_FF %% t:* %D
design -load read design -load read
hierarchy -top dff hierarchy -top dff
proc proc
equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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 dff # Constrain all select calls below inside the top module cd dff # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_FF select -assert-count 1 t:MISTRAL_FF
@ -24,7 +24,7 @@ select -assert-none t:MISTRAL_FF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
proc proc
equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 dffe # Constrain all select calls below inside the top module cd dffe # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_FF select -assert-count 1 t:MISTRAL_FF
@ -35,7 +35,7 @@ select -assert-none t:MISTRAL_FF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
proc proc
equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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 dffe # Constrain all select calls below inside the top module cd dffe # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_FF select -assert-count 1 t:MISTRAL_FF

4
tests/arch/intel_alm/fsm.ys
View file

@ -3,7 +3,7 @@ hierarchy -top fsm
proc proc
flatten flatten
equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf
async2sync async2sync
miter -equiv -make_assert -flatten gold gate miter miter -equiv -make_assert -flatten gold gate miter
sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
@ -26,7 +26,7 @@ hierarchy -top fsm
proc proc
flatten flatten
equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf
async2sync async2sync
miter -equiv -make_assert -flatten gold gate miter miter -equiv -make_assert -flatten gold gate miter
sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter

4
tests/arch/intel_alm/logic.ys
View file

@ -1,7 +1,7 @@
read_verilog ../common/logic.v read_verilog ../common/logic.v
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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
@ -15,7 +15,7 @@ design -reset
read_verilog ../common/logic.v read_verilog ../common/logic.v
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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

4
tests/arch/intel_alm/lutram.ys
View file

@ -2,7 +2,7 @@ read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r hierarchy -top lutram_1w1r
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v -map +/intel_alm/common/mem_sim.v synth_intel_alm -family cyclonev -nobram -noiopad equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v -map +/intel_alm/common/mem_sim.v synth_intel_alm -family cyclonev -nobram -noiopad -noclkbuf
memory memory
opt -full opt -full
@ -24,7 +24,7 @@ read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r hierarchy -top lutram_1w1r
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v -map +/intel_alm/common/mem_sim.v synth_intel_alm -family cyclonev -nobram -noiopad equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v -map +/intel_alm/common/mem_sim.v synth_intel_alm -family cyclonev -nobram -noiopad -noclkbuf
memory memory
opt -full opt -full

10
tests/arch/intel_alm/mul.ys
View file

@ -2,7 +2,7 @@ read_verilog ../common/mul.v
chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16 chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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
@ -16,7 +16,7 @@ read_verilog ../common/mul.v
chparam -set X_WIDTH 17 -set Y_WIDTH 17 -set A_WIDTH 34 chparam -set X_WIDTH 17 -set Y_WIDTH 17 -set A_WIDTH 34
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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
@ -28,7 +28,7 @@ read_verilog ../common/mul.v
chparam -set X_WIDTH 17 -set Y_WIDTH 17 -set A_WIDTH 34 chparam -set X_WIDTH 17 -set Y_WIDTH 17 -set A_WIDTH 34
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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
@ -40,7 +40,7 @@ read_verilog ../common/mul.v
chparam -set X_WIDTH 26 -set Y_WIDTH 26 -set A_WIDTH 52 chparam -set X_WIDTH 26 -set Y_WIDTH 26 -set A_WIDTH 52
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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
@ -52,7 +52,7 @@ read_verilog ../common/mul.v
chparam -set X_WIDTH 26 -set Y_WIDTH 26 -set A_WIDTH 52 chparam -set X_WIDTH 26 -set Y_WIDTH 26 -set A_WIDTH 52
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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

16
tests/arch/intel_alm/mux.ys
View file

@ -4,7 +4,7 @@ design -save read
hierarchy -top mux2 hierarchy -top mux2
proc proc
equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 mux2 # Constrain all select calls below inside the top module cd mux2 # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_ALUT3 select -assert-count 1 t:MISTRAL_ALUT3
@ -14,7 +14,7 @@ select -assert-none t:MISTRAL_ALUT3 %% t:* %D
design -load read design -load read
hierarchy -top mux2 hierarchy -top mux2
proc proc
equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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 mux2 # Constrain all select calls below inside the top module cd mux2 # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_ALUT3 select -assert-count 1 t:MISTRAL_ALUT3
@ -24,7 +24,7 @@ select -assert-none t:MISTRAL_ALUT3 %% t:* %D
design -load read design -load read
hierarchy -top mux4 hierarchy -top mux4
proc proc
equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 mux4 # Constrain all select calls below inside the top module cd mux4 # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_ALUT6 select -assert-count 1 t:MISTRAL_ALUT6
@ -34,7 +34,7 @@ select -assert-none t:MISTRAL_ALUT6 %% t:* %D
design -load read design -load read
hierarchy -top mux4 hierarchy -top mux4
proc proc
equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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 mux4 # Constrain all select calls below inside the top module cd mux4 # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_ALUT6 select -assert-count 1 t:MISTRAL_ALUT6
@ -44,7 +44,7 @@ select -assert-none t:MISTRAL_ALUT6 %% t:* %D
design -load read design -load read
hierarchy -top mux8 hierarchy -top mux8
proc proc
equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 mux8 # Constrain all select calls below inside the top module cd mux8 # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_ALUT3 select -assert-count 1 t:MISTRAL_ALUT3
@ -55,7 +55,7 @@ select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT6 %% t:* %D
design -load read design -load read
hierarchy -top mux8 hierarchy -top mux8
proc proc
equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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 mux8 # Constrain all select calls below inside the top module cd mux8 # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_ALUT3 select -assert-count 1 t:MISTRAL_ALUT3
@ -66,7 +66,7 @@ select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT6 %% t:* %D
design -load read design -load read
hierarchy -top mux16 hierarchy -top mux16
proc proc
equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev # equivalency check equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 mux16 # Constrain all select calls below inside the top module cd mux16 # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_ALUT3 select -assert-count 1 t:MISTRAL_ALUT3
@ -78,7 +78,7 @@ select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D
design -load read design -load read
hierarchy -top mux16 hierarchy -top mux16
proc proc
equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx # equivalency check equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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 mux16 # Constrain all select calls below inside the top module cd mux16 # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_ALUT3 select -assert-count 1 t:MISTRAL_ALUT3

2
tests/arch/intel_alm/quartus_ice.ys
View file

@ -22,5 +22,5 @@ module top();
endmodule endmodule
EOT EOT
synth_intel_alm -family cyclone10gx -quartus -noiopad synth_intel_alm -family cyclone10gx -quartus -noiopad -noclkbuf
select -assert-none w:*[* w:*]* select -assert-none w:*[* w:*]*

4
tests/arch/intel_alm/shifter.ys
View file

@ -2,7 +2,7 @@ read_verilog ../common/shifter.v
hierarchy -top top hierarchy -top top
proc proc
flatten flatten
equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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
select -assert-count 8 t:MISTRAL_FF select -assert-count 8 t:MISTRAL_FF
@ -14,7 +14,7 @@ read_verilog ../common/shifter.v
hierarchy -top top hierarchy -top top
proc proc
flatten flatten
equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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
select -assert-count 8 t:MISTRAL_FF select -assert-count 8 t:MISTRAL_FF

4
tests/arch/intel_alm/tribuf.ys
View file

@ -4,7 +4,7 @@ proc
tribuf tribuf
flatten flatten
synth synth
equiv_opt -assert -map +/simcells.v synth_intel_alm -family cyclonev -noiopad # equivalency check equiv_opt -assert -map +/simcells.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 tristate # Constrain all select calls below inside the top module cd tristate # Constrain all select calls below inside the top module
#Internal cell type used. Need support it. #Internal cell type used. Need support it.
@ -19,7 +19,7 @@ proc
tribuf tribuf
flatten flatten
synth synth
equiv_opt -assert -map +/simcells.v synth_intel_alm -family cyclone10gx -noiopad # equivalency check equiv_opt -assert -map +/simcells.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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 tristate # Constrain all select calls below inside the top module cd tristate # Constrain all select calls below inside the top module
#Internal cell type used. Need support it. #Internal cell type used. Need support it.