mirror of
https://github.com/YosysHQ/yosys
synced 2025-06-18 11:58:32 +00:00
peepopt clockgateff: add testcase
This commit is contained in:
parent
236c69bed4
commit
b6ceff2aab
1 changed files with 45 additions and 0 deletions
45
tests/various/peepopt_formal.ys
Normal file
45
tests/various/peepopt_formal.ys
Normal file
|
@ -0,0 +1,45 @@
|
||||||
|
read_verilog -sv <<EOT
|
||||||
|
module peepopt_formal_clockgateff_0(
|
||||||
|
input logic clk_i,
|
||||||
|
input logic ena_i,
|
||||||
|
input logic enb_i,
|
||||||
|
output logic clk_o
|
||||||
|
);
|
||||||
|
|
||||||
|
logic en_latched;
|
||||||
|
|
||||||
|
always_latch
|
||||||
|
if (!clk_i)
|
||||||
|
en_latched <= ena_i | enb_i;
|
||||||
|
|
||||||
|
assign clk_o = en_latched & clk_i;
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
EOT
|
||||||
|
|
||||||
|
# Check original design has latch
|
||||||
|
prep -auto-top
|
||||||
|
select -assert-count 1 t:$dlatch
|
||||||
|
select -assert-count 0 t:$dff
|
||||||
|
|
||||||
|
# Manually execute equiv_opt like pattern so clk2fflogic is called with
|
||||||
|
# -nopeepopt, otherwise this doesn't test anything
|
||||||
|
design -save preopt
|
||||||
|
check -assert
|
||||||
|
peepopt -formalclk
|
||||||
|
check -assert
|
||||||
|
design -stash postopt
|
||||||
|
|
||||||
|
# Create miter and clk2fflogic without peepopt
|
||||||
|
design -copy-from preopt -as gold A:top
|
||||||
|
design -copy-from postopt -as gate A:top
|
||||||
|
clk2fflogic -nopeepopt
|
||||||
|
equiv_make gold gate equiv
|
||||||
|
equiv_induct equiv
|
||||||
|
equiv_status -assert equiv
|
||||||
|
|
||||||
|
# Check final design has dff instead of latch
|
||||||
|
design -load postopt
|
||||||
|
clean
|
||||||
|
select -assert-count 0 t:$dlatch
|
||||||
|
select -assert-count 1 t:$dff
|
Loading…
Add table
Add a link
Reference in a new issue