mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-06-19 07:16:27 +00:00
Code Activity

Fixup issue test.

Browse source
This commit is contained in:
nella 2026-06-15 16:23:44 +02:00
parent eb4703808a
commit c0709b1b4e
1 changed files with 44 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

44
tests/proc/proc_dlatch.ys
View file

@ -87,3 +87,47 @@ EOT
proc
select -assert-count 1 t:$dlatch
select -assert-count 0 t:$adlatch
design -reset
read_verilog -formal <<EOT
module gold(input g, rn, d, zero, output reg q);
always @* if (~rn | g) q <= (~rn ? zero : d);
always @* assume(zero == 1'b0);
endmodule
module gate(input g, rn, d, zero, output reg q);
always @* if (~rn) q <= 1'b0; else if (g) q <= d;
endmodule
EOT
proc
select -assert-count 1 -module gold t:$dlatch
select -assert-count 1 -module gate t:$adlatch
select -clear
equiv_make gold gate equiv
hierarchy -top equiv
clk2fflogic
equiv_induct -set-assumes
equiv_status -assert
design -reset
read_verilog -formal <<EOT
module gold(input g, sn, d, one, output reg q);
always @* if (~sn | g) q <= (~sn ? one : d);
always @* assume(one == 1'b1);
endmodule
module gate(input g, sn, d, one, output reg q);
always @* if (~sn) q <= 1'b1; else if (g) q <= d;
endmodule
EOT
proc
select -assert-count 1 -module gold t:$dlatch
select -assert-count 1 -module gate t:$adlatch
select -clear
equiv_make gold gate equiv
hierarchy -top equiv
clk2fflogic
equiv_induct -set-assumes
equiv_status -assert