From 1602a0386419495993f25667c7c6e5fb55010592 Mon Sep 17 00:00:00 2001
From: Claire Xenia Wolf <claire@clairexen.net>
Date: Fri, 8 Oct 2021 16:21:25 +0200
Subject: [PATCH] Add support for $aldff flip-flops to verific importer

Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
---
 frontends/verific/verific.cc | 55 +++++++++++++++++++++++++++++++++++-
 frontends/verific/verific.h  |  1 +
 2 files changed, 55 insertions(+), 1 deletion(-)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 231003753..cbbae7417 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -410,6 +410,20 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
 		return true;
 	}
 
+	if (inst->Type() == PRIM_DFF)
+	{
+		VerificClocking clocking(this, inst->GetClock());
+		log_assert(clocking.disable_sig == State::S0);
+		log_assert(clocking.body_net == nullptr);
+
+		if (inst->GetAsyncVal()->IsGnd())
+			clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+		else
+			clocking.addAldff(inst_name, net_map_at(inst->GetAsyncCond()), net_map_at(inst->GetAsyncVal()),
+					net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+		return true;
+	}
+
 	return false;
 }
 
@@ -792,6 +806,34 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
 		return true;
 	}
 
+	if (inst->Type() == OPER_WIDE_DFF)
+	{
+		VerificClocking clocking(this, inst->GetClock());
+		log_assert(clocking.disable_sig == State::S0);
+		log_assert(clocking.body_net == nullptr);
+
+		RTLIL::SigSpec sig_d = IN;
+		RTLIL::SigSpec sig_q = OUT;
+		RTLIL::SigSpec sig_adata = IN1;
+		RTLIL::SigSpec sig_acond = IN2;
+
+		if (sig_acond.is_fully_const() && !sig_acond.as_bool()) {
+			cell = clocking.addDff(inst_name, sig_d, sig_q);
+			import_attributes(cell->attributes, inst);
+		} else {
+			int offset = 0, width = 0;
+			for (offset = 0; offset < GetSize(sig_acond); offset += width) {
+				for (width = 1; offset+width < GetSize(sig_acond); width++)
+					if (sig_acond[offset] != sig_acond[offset+width]) break;
+				cell = clocking.addAldff(inst_name, sig_acond[offset], sig_adata.extract(offset, width),
+						sig_d.extract(offset, width), sig_q.extract(offset, width));
+				import_attributes(cell->attributes, inst);
+			}
+		}
+
+		return true;
+	}
+
 	#undef IN
 	#undef IN1
 	#undef IN2
@@ -1806,6 +1848,17 @@ Cell *VerificClocking::addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::Si
 	return module->addDffsr(name, clock_sig, sig_set, sig_clr, sig_d, sig_q, posedge);
 }
 
+Cell *VerificClocking::addAldff(IdString name, RTLIL::SigSpec sig_aload, RTLIL::SigSpec sig_adata, SigSpec sig_d, SigSpec sig_q)
+{
+	log_assert(gclk == false);
+	log_assert(disable_sig == State::S0);
+
+	if (enable_sig != State::S1)
+		sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
+
+	return module->addAldff(name, clock_sig, sig_aload, sig_d, sig_q, sig_adata, posedge);
+}
+
 // ==================================================================
 
 struct VerificExtNets
@@ -2313,7 +2366,7 @@ struct VerificPass : public Pass {
 			RuntimeFlags::SetVar("db_preserve_user_nets", 1);
 			RuntimeFlags::SetVar("db_allow_external_nets", 1);
 			RuntimeFlags::SetVar("db_infer_wide_operators", 1);
-			RuntimeFlags::SetVar("db_infer_set_reset_registers",1);
+			RuntimeFlags::SetVar("db_infer_set_reset_registers", 1);
 
 			RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
 			RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index f79d8042a..9d5beb787 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -50,6 +50,7 @@ struct VerificClocking {
 	RTLIL::Cell *addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value = Const());
 	RTLIL::Cell *addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value);
 	RTLIL::Cell *addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q);
+	RTLIL::Cell *addAldff(IdString name, RTLIL::SigSpec sig_aload, RTLIL::SigSpec sig_adata, SigSpec sig_d, SigSpec sig_q);
 
 	bool property_matches_sequence(const VerificClocking &seq) const {
 		if (clock_net != seq.clock_net)
-- 
2.30.2