mirror of
https://github.com/YosysHQ/yosys
synced 2025-11-04 05:19:11 +00:00
83 lines
1.5 KiB
Text
83 lines
1.5 KiB
Text
# based on the peepopt_formal.ys test
|
|
read_verilog -sv <<EOT
|
|
module peepopt_formal_clockgateff_0(
|
|
input logic clk_i,
|
|
input logic ena_i,
|
|
input logic enb_i,
|
|
input logic enc_i,
|
|
input logic d_0_i,
|
|
input logic d_1_i,
|
|
output logic clk_o,
|
|
output logic d_0_o,
|
|
output logic d_1_o,
|
|
output logic d_2_o
|
|
);
|
|
|
|
logic en_latched;
|
|
initial d_0_o = '0;
|
|
initial d_1_o = '0;
|
|
initial en_latched = '0;
|
|
initial d_2_o = '0;
|
|
|
|
reg mem [4];
|
|
|
|
initial begin
|
|
mem[0] = 0;
|
|
mem[1] = 0;
|
|
mem[2] = 0;
|
|
mem[3] = 0;
|
|
end
|
|
reg [1:0] counter = 0;
|
|
|
|
always_latch
|
|
if (!clk_i)
|
|
en_latched <= ena_i | enb_i;
|
|
|
|
assign clk_o = en_latched & clk_i;
|
|
|
|
always @(posedge clk_o)
|
|
d_0_o <= d_0_i;
|
|
|
|
always @(posedge clk_o)
|
|
if (enc_i)
|
|
d_1_o <= d_1_i;
|
|
|
|
|
|
always @(posedge clk_o) begin
|
|
counter <= counter + 1;
|
|
mem[counter] <= mem[counter] + 1;
|
|
d_2_o <= mem[counter] + 1;
|
|
end;
|
|
|
|
|
|
|
|
endmodule
|
|
EOT
|
|
|
|
# Check original design has latch
|
|
prep -auto-top
|
|
opt_dff
|
|
select -assert-count 1 t:$dlatch
|
|
|
|
# Manually execute equiv_opt like pattern so clk2fflogic is called with
|
|
# -nopeepopt, otherwise this doesn't test everything
|
|
design -save preopt
|
|
check -assert
|
|
formalff -declockgate
|
|
|
|
design -save postopt
|
|
|
|
delete -output */clk_o
|
|
clean -purge
|
|
select -assert-count 0 t:$dlatch
|
|
|
|
design -reset
|
|
|
|
# Create miter and clk2fflogic without peepopt
|
|
design -copy-from preopt -as gold A:top
|
|
design -copy-from postopt -as gate A:top
|
|
clk2fflogic -nopeepopt
|
|
|
|
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
|
|
memory_map -formal
|
|
sat -prove-asserts -seq 16 -show-public -verify equiv
|