mirror of https://github.com/YosysHQ/yosys.git
dlatchlibmap: added more formal testscases
This commit is contained in:
Iztok Jeras
parent
6b44f4321e
commit
92d4f60977
|
|
@ -25,6 +25,8 @@ equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -prepare -libert
|
|||
dfflibmap -prepare -liberty dlatchlibmap.lib
|
||||
equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dlatchlibmap.lib
|
||||
|
||||
##################################################################
|
||||
|
||||
design -load orig
|
||||
dfflibmap -liberty dlatchlibmap.lib
|
||||
clean
|
||||
|
|
@ -73,6 +75,8 @@ select -assert-count 1 t:dlatchn
|
|||
select -assert-count 4 t:dlatchsr
|
||||
select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i
|
||||
|
||||
##################################################################
|
||||
|
||||
design -load orig
|
||||
dfflibmap -liberty dlatchlibmap.lib -dont_use *latchn
|
||||
clean
|
||||
|
|
@ -80,6 +84,12 @@ clean
|
|||
select -assert-count 0 t:dlatchn
|
||||
select -assert-count 5 t:dlatchsr
|
||||
|
||||
##################################################################
|
||||
|
||||
design -load orig
|
||||
read_liberty -lib dlatchlibmap.lib dlatchlibmap_dlatchsr_mixedpol.lib
|
||||
equiv_opt -map dlatchlibmap-sim.v -map dlatchlibmap_dlatchsr_mixedpol-sim.v -assert -multiclock dfflibmap -liberty dlatchlibmap.lib -liberty dlatchlibmap_dlatchsr_mixedpol.lib -dont_use dlatchsr
|
||||
|
||||
design -load orig
|
||||
dfflibmap -liberty dlatchlibmap.lib -liberty dlatchlibmap_dlatchsr_mixedpol.lib -dont_use dlatchsr
|
||||
clean
|
||||
|
|
|
|||
|
|
@ -0,0 +1,34 @@
|
|||
library(test) {
|
||||
cell (dlatchsr) {
|
||||
area : 6;
|
||||
latch("IQ", "IQN") {
|
||||
data_in : "D";
|
||||
enable : "ENA";
|
||||
clear : "CLEAR";
|
||||
preset : "PRESET";
|
||||
clear_preset_var1 : H;
|
||||
clear_preset_var2 : H;
|
||||
}
|
||||
pin(D) {
|
||||
direction : input;
|
||||
}
|
||||
pin(ENA) {
|
||||
direction : input;
|
||||
clock : true;
|
||||
}
|
||||
pin(CLEAR) {
|
||||
direction : input;
|
||||
}
|
||||
pin(PRESET) {
|
||||
direction : input;
|
||||
}
|
||||
pin(Q) {
|
||||
direction: output;
|
||||
function : "IQ";
|
||||
}
|
||||
pin(QN) {
|
||||
direction: output;
|
||||
function : "IQN";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,34 @@
|
|||
library(test) {
|
||||
cell (dlatchsr) {
|
||||
area : 6;
|
||||
latch("IQ", "IQN") {
|
||||
data_in : "D";
|
||||
enable : "ENA";
|
||||
clear : "CLEAR";
|
||||
preset : "PRESET";
|
||||
clear_preset_var1 : L;
|
||||
clear_preset_var2 : L;
|
||||
}
|
||||
pin(D) {
|
||||
direction : input;
|
||||
}
|
||||
pin(ENA) {
|
||||
direction : input;
|
||||
clock : true;
|
||||
}
|
||||
pin(CLEAR) {
|
||||
direction : input;
|
||||
}
|
||||
pin(PRESET) {
|
||||
direction : input;
|
||||
}
|
||||
pin(Q) {
|
||||
direction: output;
|
||||
function : "IQ";
|
||||
}
|
||||
pin(QN) {
|
||||
direction: output;
|
||||
function : "IQN";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,10 @@
|
|||
module dlatchsr_mixedpol(input ENA, D, CLEAR, PRESET, output reg Q, output QN);
|
||||
|
||||
always @*
|
||||
if (PRESET) Q <= 1'b1;
|
||||
else if (~CLEAR) Q <= 1'b0;
|
||||
else if (ENA) Q <= ~D;
|
||||
|
||||
assign QN = ~Q;
|
||||
|
||||
endmodule
|
||||
|
|
@ -84,6 +84,82 @@ $_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
|||
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
||||
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
||||
|
||||
assume property (~R || ~S);
|
||||
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
|
||||
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||
|
||||
assign Q[9:5] = ~Q[4:0];
|
||||
|
||||
endmodule
|
||||
|
||||
EOT
|
||||
|
||||
proc
|
||||
opt
|
||||
read_liberty dlatchlibmap_dlatchsr_l.lib
|
||||
|
||||
copy top top_unmapped
|
||||
dfflibmap -liberty dlatchlibmap_dlatchsr_l.lib top
|
||||
|
||||
clk2fflogic
|
||||
flatten
|
||||
opt_clean -purge
|
||||
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||
hierarchy -top miter
|
||||
# Prove that this is equivalent with the assumption
|
||||
sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
|
||||
# Prove that this is NOT equivalent WITHOUT the assumption
|
||||
sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
|
||||
|
||||
##################################################################
|
||||
|
||||
design -reset
|
||||
read_verilog -sv -icells <<EOT
|
||||
|
||||
module top(input E, D, S, R, output [9:0] Q);
|
||||
|
||||
$_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
||||
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
||||
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
||||
|
||||
assume property (~R || ~S);
|
||||
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
|
||||
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||
|
||||
assign Q[9:5] = ~Q[4:0];
|
||||
|
||||
endmodule
|
||||
|
||||
EOT
|
||||
|
||||
proc
|
||||
opt
|
||||
read_liberty dlatchlibmap_dlatchsr_h.lib
|
||||
|
||||
copy top top_unmapped
|
||||
dfflibmap -liberty dlatchlibmap_dlatchsr_h.lib top
|
||||
|
||||
clk2fflogic
|
||||
flatten
|
||||
opt_clean -purge
|
||||
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||
hierarchy -top miter
|
||||
# Prove that this is equivalent with the assumption
|
||||
sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
|
||||
# Prove that this is NOT equivalent WITHOUT the assumption
|
||||
sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
|
||||
|
||||
##################################################################
|
||||
|
||||
design -reset
|
||||
read_verilog -sv -icells <<EOT
|
||||
|
||||
module top(input E, D, S, R, output [9:0] Q);
|
||||
|
||||
$_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
||||
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
||||
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
||||
|
||||
// no assume when mapping to X
|
||||
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
|
||||
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||
|
|
|
|||
|
|
@ -22,9 +22,10 @@ EOT
|
|||
|
||||
proc
|
||||
opt
|
||||
read_liberty dlatchlibmap_dlatchsr_s.lib
|
||||
|
||||
copy top top_unmapped
|
||||
|
||||
##################################################################
|
||||
|
||||
dfflibmap -liberty dlatchlibmap_dlatchsr_s.lib top
|
||||
|
||||
clk2fflogic
|
||||
|
|
@ -53,6 +54,34 @@ sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
|||
|
||||
delete top miter
|
||||
|
||||
copy top_unmapped top
|
||||
dfflibmap -liberty dlatchlibmap_dlatchsr_l.lib top
|
||||
|
||||
clk2fflogic
|
||||
flatten
|
||||
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||
|
||||
# Prove that this is equivalent
|
||||
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||
|
||||
##################################################################
|
||||
|
||||
delete top miter
|
||||
|
||||
copy top_unmapped top
|
||||
dfflibmap -liberty dlatchlibmap_dlatchsr_h.lib top
|
||||
|
||||
clk2fflogic
|
||||
flatten
|
||||
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||
|
||||
# Prove that this is equivalent
|
||||
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||
|
||||
##################################################################
|
||||
|
||||
delete top miter
|
||||
|
||||
copy top_unmapped top
|
||||
dfflibmap -liberty dlatchlibmap_dlatchsr_mixedpol.lib top
|
||||
|
||||
|
|
@ -76,3 +105,17 @@ miter -equiv -make_assert -flatten top_unmapped top miter
|
|||
|
||||
# Prove that this is equivalent
|
||||
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||
|
||||
##################################################################
|
||||
|
||||
delete top miter
|
||||
|
||||
copy top_unmapped top
|
||||
dfflibmap -liberty dlatchlibmap_dlatchsr_not_data_l.lib top
|
||||
|
||||
clk2fflogic
|
||||
flatten
|
||||
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||
|
||||
# Prove that this is equivalent
|
||||
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||
|
|
|
|||
Loading…
Reference in New Issue