mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-03-23 04:49:15 +00:00
Code Activity

Merge 12b443e71c into 5fd39ff3e1

Browse source
This commit is contained in:
Emil J 2026-03-20 20:16:12 +13:00 • committed by GitHub
commit 6c6699be46
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
13 changed files with 452 additions and 68 deletions
Download patch file Download diff file Expand all files Collapse all files

8
docs/source/cell/gate_reg_ff.rst
View file

@ -154,6 +154,10 @@ to the following Verilog code template, where ``RST_EDGE`` is ``posedge`` if
``RST_LVL`` if ``1``, ``negedge`` otherwise, and ``SET_EDGE`` is ``posedge`` if
``SET_LVL`` if ``1``, ``negedge`` otherwise.
When both set and reset are active, the state and output is undefined. The Verilog
code model does not correspond to this due to limitations
of synthesizable Verilog.
.. code-block:: verilog
:force:
@ -187,6 +191,10 @@ types relate to the following Verilog code template, where ``RST_EDGE`` is
``posedge`` if ``RST_LVL`` if ``1``, ``negedge`` otherwise, and ``SET_EDGE`` is
``posedge`` if ``SET_LVL`` if ``1``, ``negedge`` otherwise.
When both set and reset are active, the state and output is undefined. The Verilog
code model does not correspond to this due to limitations
of synthesizable Verilog.
.. code-block:: verilog
:force:

1
docs/source/cell/word_reg.rst
View file

@ -78,6 +78,7 @@ D-type flip-flops with asynchronous set and reset are represented by `$dffsr`
cells. As the `$dff` cells they have ``CLK``, ``D`` and ``Q`` ports. In addition
they also have multi-bit ``SET`` and ``CLR`` input ports and the corresponding
polarity parameters, like `$sr` cells.
When both set and reset are active, the state and output is undefined.
D-type flip-flops with enable are represented by `$dffe`, `$adffe`, `$aldffe`,
`$dffsre`, `$sdffe`, and `$sdffce` cells, which are enhanced variants of `$dff`,

97
frontends/liberty/liberty.cc
View file

@ -20,6 +20,7 @@
#include "passes/techmap/libparse.h"
#include "kernel/register.h"
#include "kernel/log.h"
#include <array>
YOSYS_NAMESPACE_BEGIN
@ -210,7 +211,10 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node)
auto [iq_sig, iqn_sig] = find_latch_ff_wires(module, node);
RTLIL::SigSpec clk_sig, data_sig, clear_sig, preset_sig;
bool clk_polarity = true, clear_polarity = true, preset_polarity = true;
const std::string name = RTLIL::unescape_id(module->name);
std::optional<char> clear_preset_var1;
std::optional<char> clear_preset_var2;
for (auto child : node->children) {
if (child->id == "clocked_on")
clk_sig = parse_func_expr(module, child->value.c_str());
@ -220,10 +224,18 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node)
clear_sig = parse_func_expr(module, child->value.c_str());
if (child->id == "preset")
preset_sig = parse_func_expr(module, child->value.c_str());
for (auto& [id, var] : {pair{"clear_preset_var1", &clear_preset_var1}, {"clear_preset_var2", &clear_preset_var2}})
if (child->id == id) {
if (child->value.size() != 1)
log_error("Unexpected length of clear_preset_var* value %s in FF cell %s\n", child->value, name);
*var = child->value[0];
}
}
if (clk_sig.size() == 0 || data_sig.size() == 0)
log_error("FF cell %s has no next_state and/or clocked_on attribute.\n", RTLIL::unescape_id(module->name));
log_error("FF cell %s has no next_state and/or clocked_on attribute.\n", name);
for (bool rerun_invert_rollback = true; rerun_invert_rollback;)
{
@ -248,36 +260,64 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node)
}
}
RTLIL::Cell *cell = module->addCell(NEW_ID, ID($_NOT_));
cell->setPort(ID::A, iq_sig);
cell->setPort(ID::Y, iqn_sig);
for (auto& [out_sig, cp_var, neg] : {tuple{iq_sig, clear_preset_var1, false}, {iqn_sig, clear_preset_var2, true}}) {
SigSpec q_sig = out_sig;
if (neg) {
q_sig = module->addWire(NEW_ID, out_sig.as_wire());
module->addNotGate(NEW_ID, q_sig, out_sig);
}
cell = module->addCell(NEW_ID, "");
cell->setPort(ID::D, data_sig);
cell->setPort(ID::Q, iq_sig);
cell->setPort(ID::C, clk_sig);
RTLIL::Cell* cell = module->addCell(NEW_ID, "");
cell->setPort(ID::D, data_sig);
cell->setPort(ID::Q, q_sig);
cell->setPort(ID::C, clk_sig);
if (clear_sig.size() == 0 && preset_sig.size() == 0) {
cell->type = stringf("$_DFF_%c_", clk_polarity ? 'P' : 'N');
if (clear_sig.size() == 0 && preset_sig.size() == 0) {
cell->type = stringf("$_DFF_%c_", clk_polarity ? 'P' : 'N');
}
if (clear_sig.size() == 1 && preset_sig.size() == 0) {
cell->type = stringf("$_DFF_%c%c0_", clk_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N');
cell->setPort(ID::R, clear_sig);
}
if (clear_sig.size() == 0 && preset_sig.size() == 1) {
cell->type = stringf("$_DFF_%c%c1_", clk_polarity ? 'P' : 'N', preset_polarity ? 'P' : 'N');
cell->setPort(ID::R, preset_sig);
}
if (clear_sig.size() == 1 && preset_sig.size() == 1) {
cell->type = stringf("$_DFFSR_%c%c%c_", clk_polarity ? 'P' : 'N', preset_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N');
SigBit s_sig = preset_sig;
SigBit r_sig = clear_sig;
if (cp_var && *cp_var != 'X') {
// Either set or reset dominates
bool set_dominates;
if (*cp_var == 'L') {
set_dominates = neg;
} else if (*cp_var == 'H') {
set_dominates = !neg;
} else {
log_error("FF cell %s has unsupported clear&preset behavior \'%c\'.\n", name, *cp_var);
}
log_debug("cell %s variable %d cp_var %c set dominates? %d\n", name, (int)neg + 1, *cp_var, set_dominates);
// S&R priority is well-defined now
if (set_dominates) {
r_sig = module->AndnotGate(NEW_ID, r_sig, s_sig);
} else {
s_sig = module->AndnotGate(NEW_ID, s_sig, r_sig);
}
} else {
log_debug("cell %s variable %d undef c&p behavior\n", name, (int)neg + 1);
}
cell->setPort(ID::S, s_sig);
cell->setPort(ID::R, r_sig);
}
log_assert(!cell->type.empty());
}
if (clear_sig.size() == 1 && preset_sig.size() == 0) {
cell->type = stringf("$_DFF_%c%c0_", clk_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N');
cell->setPort(ID::R, clear_sig);
}
if (clear_sig.size() == 0 && preset_sig.size() == 1) {
cell->type = stringf("$_DFF_%c%c1_", clk_polarity ? 'P' : 'N', preset_polarity ? 'P' : 'N');
cell->setPort(ID::R, preset_sig);
}
if (clear_sig.size() == 1 && preset_sig.size() == 1) {
cell->type = stringf("$_DFFSR_%c%c%c_", clk_polarity ? 'P' : 'N', preset_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N');
cell->setPort(ID::S, preset_sig);
cell->setPort(ID::R, clear_sig);
}
log_assert(!cell->type.empty());
}
static bool create_latch(RTLIL::Module *module, const LibertyAst *node, bool flag_ignore_miss_data_latch)
@ -797,3 +837,4 @@ skip_cell:;
YOSYS_NAMESPACE_END

27
passes/sat/async2sync.cc
View file

@ -157,6 +157,7 @@ struct Async2syncPass : public Pass {
SigSpec sig_set = ff.sig_set;
SigSpec sig_clr = ff.sig_clr;
SigSpec sig_clr_inv = ff.sig_clr;
if (!ff.pol_set) {
if (!ff.is_fine)
@ -166,24 +167,42 @@ struct Async2syncPass : public Pass {
}
if (ff.pol_clr) {
if (!ff.is_fine)
sig_clr_inv = module->Not(NEW_ID, sig_clr);
else
sig_clr_inv = module->NotGate(NEW_ID, sig_clr);
} else {
if (!ff.is_fine)
sig_clr = module->Not(NEW_ID, sig_clr);
else
sig_clr = module->NotGate(NEW_ID, sig_clr);
}
// At this point, sig_set and sig_clr are now unconditionally
// active-high, and sig_clr_inv is inverted sig_clr
SigSpec set_and_clr;
if (!ff.is_fine)
set_and_clr = module->And(NEW_ID, sig_set, sig_clr);
else
set_and_clr = module->AndGate(NEW_ID, sig_set, sig_clr);
if (!ff.is_fine) {
SigSpec tmp = module->Or(NEW_ID, ff.sig_d, sig_set);
module->addAnd(NEW_ID, tmp, sig_clr, new_d);
tmp = module->And(NEW_ID, tmp, sig_clr_inv);
module->addBwmux(NEW_ID, tmp, Const(State::Sx, ff.width), set_and_clr, new_d);
tmp = module->Or(NEW_ID, new_q, sig_set);
module->addAnd(NEW_ID, tmp, sig_clr, ff.sig_q);
tmp = module->And(NEW_ID, tmp, sig_clr_inv);
module->addBwmux(NEW_ID, tmp, Const(State::Sx, ff.width), set_and_clr, ff.sig_q);
} else {
SigSpec tmp = module->OrGate(NEW_ID, ff.sig_d, sig_set);
module->addAndGate(NEW_ID, tmp, sig_clr, new_d);
tmp = module->AndGate(NEW_ID, tmp, sig_clr_inv);
module->addMuxGate(NEW_ID, tmp, State::Sx, set_and_clr, new_d);
tmp = module->OrGate(NEW_ID, new_q, sig_set);
module->addAndGate(NEW_ID, tmp, sig_clr, ff.sig_q);
tmp = module->AndGate(NEW_ID, tmp, sig_clr_inv);
module->addMuxGate(NEW_ID, tmp, State::Sx, set_and_clr, ff.sig_q);
}
ff.sig_d = new_d;

12
passes/sat/clk2fflogic.cc
View file

@ -123,10 +123,14 @@ struct Clk2fflogicPass : public Pass {
return module->Mux(NEW_ID, a, b, s);
}
SigSpec bitwise_sr(Module *module, SigSpec a, SigSpec s, SigSpec r, bool is_fine) {
if (is_fine)
return module->AndGate(NEW_ID, module->OrGate(NEW_ID, a, s), module->NotGate(NEW_ID, r));
else
return module->And(NEW_ID, module->Or(NEW_ID, a, s), module->Not(NEW_ID, r));
if (is_fine) {
return module->MuxGate(NEW_ID, module->AndGate(NEW_ID, module->OrGate(NEW_ID, a, s), module->NotGate(NEW_ID, r)), RTLIL::State::Sx, module->AndGate(NEW_ID, s, r));
} else {
std::vector<SigBit> y;
for (int i = 0; i < a.size(); i++)
y.push_back(module->MuxGate(NEW_ID, module->AndGate(NEW_ID, module->OrGate(NEW_ID, a[i], s[i]), module->NotGate(NEW_ID, r[i])), RTLIL::State::Sx, module->AndGate(NEW_ID, s[i], r[i])));
return y;
}
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{

24
techlibs/common/simcells.v
View file

@ -1613,6 +1613,7 @@ endmodule
//-
//- Truth table: C S R D | Q
//- ---------+---
//- - 0 0 - | x
//- - - 0 - | 0
//- - 0 - - | 1
//- \ - - d | d
@ -1641,6 +1642,7 @@ endmodule
//-
//- Truth table: C S R D | Q
//- ---------+---
//- - 0 1 - | x
//- - - 1 - | 0
//- - 0 - - | 1
//- \ - - d | d
@ -1669,6 +1671,7 @@ endmodule
//-
//- Truth table: C S R D | Q
//- ---------+---
//- - 1 0 - | x
//- - - 0 - | 0
//- - 1 - - | 1
//- \ - - d | d
@ -1697,6 +1700,7 @@ endmodule
//-
//- Truth table: C S R D | Q
//- ---------+---
//- - 1 1 - | x
//- - - 1 - | 0
//- - 1 - - | 1
//- \ - - d | d
@ -1725,6 +1729,7 @@ endmodule
//-
//- Truth table: C S R D | Q
//- ---------+---
//- - 0 0 - | x
//- - - 0 - | 0
//- - 0 - - | 1
//- / - - d | d
@ -1753,6 +1758,7 @@ endmodule
//-
//- Truth table: C S R D | Q
//- ---------+---
//- - 0 1 - | x
//- - - 1 - | 0
//- - 0 - - | 1
//- / - - d | d
@ -1781,6 +1787,7 @@ endmodule
//-
//- Truth table: C S R D | Q
//- ---------+---
//- - 1 0 - | x
//- - - 0 - | 0
//- - 1 - - | 1
//- / - - d | d
@ -1809,6 +1816,7 @@ endmodule
//-
//- Truth table: C S R D | Q
//- ---------+---
//- - 1 1 - | x
//- - - 1 - | 0
//- - 1 - - | 1
//- / - - d | d
@ -1837,6 +1845,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 0 0 - - | x
//- - - 0 - - | 0
//- - 0 - - - | 1
//- \ - - 0 d | d
@ -1865,6 +1874,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 0 0 - - | x
//- - - 0 - - | 0
//- - 0 - - - | 1
//- \ - - 1 d | d
@ -1893,6 +1903,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 0 1 - - | x
//- - - 1 - - | 0
//- - 0 - - - | 1
//- \ - - 0 d | d
@ -1921,6 +1932,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 0 1 - - | x
//- - - 1 - - | 0
//- - 0 - - - | 1
//- \ - - 1 d | d
@ -1949,6 +1961,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 1 0 - - | x
//- - - 0 - - | 0
//- - 1 - - - | 1
//- \ - - 0 d | d
@ -1977,6 +1990,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 1 0 - - | x
//- - - 0 - - | 0
//- - 1 - - - | 1
//- \ - - 1 d | d
@ -2005,6 +2019,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 1 1 - - | x
//- - - 1 - - | 0
//- - 1 - - - | 1
//- \ - - 0 d | d
@ -2033,6 +2048,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 1 1 - - | x
//- - - 1 - - | 0
//- - 1 - - - | 1
//- \ - - 1 d | d
@ -2061,6 +2077,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 0 0 - - | x
//- - - 0 - - | 0
//- - 0 - - - | 1
//- / - - 0 d | d
@ -2089,6 +2106,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 0 0 - - | x
//- - - 0 - - | 0
//- - 0 - - - | 1
//- / - - 1 d | d
@ -2117,6 +2135,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 0 1 - - | x
//- - - 1 - - | 0
//- - 0 - - - | 1
//- / - - 0 d | d
@ -2145,6 +2164,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 0 1 - - | x
//- - - 1 - - | 0
//- - 0 - - - | 1
//- / - - 1 d | d
@ -2173,6 +2193,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 1 0 - - | x
//- - - 0 - - | 0
//- - 1 - - - | 1
//- / - - 0 d | d
@ -2201,6 +2222,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 1 0 - - | x
//- - - 0 - - | 0
//- - 1 - - - | 1
//- / - - 1 d | d
@ -2229,6 +2251,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 1 1 - - | x
//- - - 1 - - | 0
//- - 1 - - - | 1
//- / - - 0 d | d
@ -2257,6 +2280,7 @@ endmodule
//-
//- Truth table: C S R E D | Q
//- -----------+---
//- - 1 1 - - | x
//- - - 1 - - | 0
//- - 1 - - - | 1
//- / - - 1 d | d

4
tests/techmap/dfflibmap.ys
View file

@ -64,8 +64,8 @@ select -assert-count 1 t:dffe
select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i
design -load orig
dfflibmap -prepare -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr.lib
dfflibmap -map-only -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr.lib
dfflibmap -prepare -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib
dfflibmap -map-only -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib
clean
select -assert-count 5 t:$_NOT_

0
tests/techmap/dfflibmap_dffr_not_next.lib → tests/techmap/dfflibmap_dffsr_not_next_l.lib
View file

6
tests/techmap/dfflibmap_dffsr.lib → tests/techmap/dfflibmap_dffsr_r.lib
View file

@ -7,8 +7,8 @@ library(test) {
clear : "CLEAR";
preset : "PRESET";
clear_preset_var1 : L;
clear_preset_var2 : L;
}
clear_preset_var2 : H;
}
pin(D) {
direction : input;
}
@ -28,6 +28,6 @@ library(test) {
pin(QN) {
direction: output;
function : "IQN";
}
}
}
}

33
tests/techmap/dfflibmap_dffsr_s.lib Normal file
View file

@ -0,0 +1,33 @@
library(test) {
cell (dffsr) {
area : 6;
ff("IQ", "IQN") {
next_state : "D";
clocked_on : "CLK";
clear : "CLEAR";
preset : "PRESET";
clear_preset_var1 : H;
clear_preset_var2 : L;
}
pin(D) {
direction : input;
}
pin(CLK) {
direction : input;
}
pin(CLEAR) {
direction : input;
}
pin(PRESET) {
direction : input;
}
pin(Q) {
direction: output;
function : "IQ";
}
pin(QN) {
direction: output;
function : "IQN";
}
}
}

33
tests/techmap/dfflibmap_dffsr_x.lib Normal file
View file

@ -0,0 +1,33 @@
library(test) {
cell (dffsr) {
area : 6;
ff("IQ", "IQN") {
next_state : "D";
clocked_on : "CLK";
clear : "CLEAR";
preset : "PRESET";
clear_preset_var1 : X;
clear_preset_var2 : X;
}
pin(D) {
direction : input;
}
pin(CLK) {
direction : input;
}
pin(CLEAR) {
direction : input;
}
pin(PRESET) {
direction : input;
}
pin(Q) {
direction: output;
function : "IQ";
}
pin(QN) {
direction: output;
function : "IQN";
}
}
}

175
tests/techmap/dfflibmap_formal.ys
View file

@ -8,13 +8,132 @@ $_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
// Formal checking of directly instantiated DFFSR doesn't work at the moment
// likely due to an equiv_induct assume bug #5196
assume property (~R || ~S);
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
// // Workaround for DFFSR bug #5194
// assume property (~R || ~S);
// $_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
// $_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
assign Q[11:6] = ~Q[5:0];
endmodule
EOT
proc
opt
read_liberty dfflibmap_dffsr_s.lib
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffsr_s.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 C, D, E, S, R, output [11:0] Q);
$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
assume property (~R || ~S);
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
assign Q[11:6] = ~Q[5:0];
endmodule
EOT
proc
opt
read_liberty dfflibmap_dffsr_r.lib
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffsr_r.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 C, D, E, S, R, output [11:0] Q);
$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
// no assume when mapping to X
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
assign Q[11:6] = ~Q[5:0];
endmodule
EOT
proc
opt
read_liberty dfflibmap_dffsr_x.lib
opt
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffsr_x.lib top
clk2fflogic
flatten
opt_clean -purge
miter -equiv -make_assert -flatten top_unmapped top miter
hierarchy -top miter
# Prove that this is equivalent
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
##################################################################
design -reset
read_verilog -sv -icells <<EOT
module top(input C, D, E, S, R, output [11:0] Q);
$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
// Formal checking of directly instantiated DFFSR doesn't work at the moment
// likely due to an equiv_induct -set-assumes assume bug #5196
// no assume when mapping to unset clear_preset_var
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
@ -32,12 +151,14 @@ read_liberty dfflibmap_dffsr_not_next.lib
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib top
async2sync
clk2fflogic
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_status -assert equiv
miter -equiv -make_assert -flatten top_unmapped top miter
hierarchy -top miter
# Prove that this is equivalent
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
##################################################################
@ -50,13 +171,9 @@ $_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
// Formal checking of directly instantiated DFFSR doesn't work at the moment
// likely due to an equiv_induct assume bug #5196
// // Workaround for DFFSR bug #5194
// assume property (~R || ~S);
// $_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
// $_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
assume property (~R || ~S);
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
@ -68,17 +185,21 @@ EOT
proc
opt
read_liberty dfflibmap_dffr_not_next.lib
read_liberty dfflibmap_dffsr_not_next_l.lib
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffr_not_next.lib top
dfflibmap -liberty dfflibmap_dffsr_not_next_l.lib top
async2sync
clk2fflogic
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_status -assert equiv
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
##################################################################
@ -108,11 +229,11 @@ copy top top_unmapped
simplemap top
dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib top
async2sync
clk2fflogic
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_induct -set-assumes equiv
equiv_status -assert equiv
##################################################################
@ -139,9 +260,9 @@ copy top top_unmapped
simplemap top
dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dff_not_next.lib top
async2sync
clk2fflogic
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_induct -set-assumes equiv
equiv_status -assert equiv

100
tests/techmap/dfflibmap_proc_formal.ys Normal file
View file

@ -0,0 +1,100 @@
##################################################################
read_verilog -sv -icells <<EOT
module top(input C, D, E, S, R, output [7:0] Q);
always @( posedge C, posedge S, posedge R)
if (R)
Q[0] <= 0;
else if (S)
Q[0] <= 1;
else
Q[0] <= D;
always @( posedge C, posedge S, posedge R)
if (S)
Q[1] <= 1;
else if (R)
Q[1] <= 0;
else
Q[1] <= D;
always @( posedge C, posedge S, posedge R)
if (R)
Q[2] <= 0;
else if (S)
Q[2] <= 1;
else if (E)
Q[2] <= D;
always @( posedge C, posedge S, posedge R)
if (S)
Q[3] <= 1;
else if (R)
Q[3] <= 0;
else if (E)
Q[3] <= D;
assign Q[7:4] = ~Q[3:0];
endmodule
EOT
proc
opt
read_liberty dfflibmap_dffsr_s.lib
copy top top_unmapped
dfflibmap -liberty dfflibmap_dffsr_s.lib top
clk2fflogic
flatten
opt_clean -purge
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 dfflibmap_dffsr_r.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 dfflibmap_dffsr_mixedpol.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 dfflibmap_dffsr_not_next.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