[CEC][SimGen][LUT mapping] Adding option to consider an already mappe…

…d circuit before executing SimGen
Carmine50 · Dec 21, 2024 · 8a1c28b · 8a1c28b
1 parent f407156
commit 8a1c28b
Showing 1 changed file with 16 additions and 7 deletions.
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
@@ -4304,13 +4304,22 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){
 
     Cec4_Man_t * pManSim;  
     int i, k, iFan;
-
-
-    // apply technology mapping
-    If_Par_t IfPars, * pIfPars = &IfPars;
-    Gia_ManSetIfParsDefault( pIfPars );
-    pIfPars->nLutSize = 6;
-    Gia_Man_t * pMapped = Gia_ManPerformMapping( p, pIfPars );
+    Gia_Man_t * pMapped;
+
+    if (!Gia_ManHasMapping(p)){
+      // apply technology mapping if not already done
+      If_Par_t IfPars, * pIfPars = &IfPars;
+      Gia_ManSetIfParsDefault( pIfPars );
+      pIfPars->nLutSize = 6;
+      pMapped = Gia_ManPerformMapping( p, pIfPars );
+      if(pPars->fVerbose)
+        printf("Performing LUT-mapping\n");
+    } else {
+      pMapped = Gia_ManDup( p );
+      Gia_ManDupMapping( pMapped, p );
+      if(pPars->fVerbose)
+        printf("Using already mapped network\n");
+    }
     pManSim = Cec4_ManCreate( pMapped, pPars->pCECPars );
 
     Cec_DeriveSOPs( pMapped );