ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Public Member Functions | List of all members
rrr::Simulator< Ntk > Class Template Reference

#include <rrrSimulator.h>

Public Member Functions

 Simulator ()
 
 Simulator (Parameter const *pPar)
 
void AssignNetwork (Ntk *pNtk_, bool fReuse)
 
bool CheckRedundancy (int id, int idx)
 
bool CheckFeasibility (int id, int fi, bool c)
 
void AddCex (std::vector< VarValue > const &vCex)
 
void ResetSummary ()
 
summary< int > GetStatsSummary () const
 
summary< double > GetTimesSummary () const
 

Detailed Description

template<typename Ntk>
class rrr::Simulator< Ntk >

Definition at line 15 of file rrrSimulator.h.

Constructor & Destructor Documentation

◆ Simulator() [1/2]

template<typename Ntk>
rrr::Simulator< Ntk >::Simulator ( )

Definition at line 662 of file rrrSimulator.h.

662 :
663 pNtk(NULL),
664 nVerbose(0),
665 nWords(0),
666 fGenerated(false),
667 fInitialized(false),
668 target(-1),
669 iPivot(0),
670 fUpdate(false) {
671 ResetSummary();
672 }
Here is the call graph for this function:

◆ Simulator() [2/2]

template<typename Ntk>
rrr::Simulator< Ntk >::Simulator ( Parameter const * pPar)

Definition at line 675 of file rrrSimulator.h.

675 :
676 pNtk(NULL),
677 nVerbose(pPar->nSimulatorVerbose),
678 nWords(pPar->nWords),
679 fGenerated(false),
680 fInitialized(false),
681 target(-1),
682 iPivot(0),
683 fUpdate(false) {
684 care.resize(nWords);
685 tmp.resize(nWords);
686 ResetSummary();
687 }
Here is the call graph for this function:

Member Function Documentation

◆ AddCex()

template<typename Ntk>
void rrr::Simulator< Ntk >::AddCex ( std::vector< VarValue > const & vCex)

Definition at line 786 of file rrrSimulator.h.

786 {
787 if(nVerbose) {
788 std::cout << "cex: ";
789 for(VarValue c: vCex) {
790 std::cout << GetVarValueChar(c);
791 }
792 std::cout << std::endl;
793 }
794 // record care pi indices
795 assert(int_size(vCex) == pNtk->GetNumPis());
796 std::vector<int> vCarePiIdxs;
797 for(int idx = 0; idx < pNtk->GetNumPis(); idx++) {
798 switch(vCex[idx]) {
799 case TRUE:
800 vCarePiIdxs.push_back(idx);
801 break;
802 case FALSE:
803 vCarePiIdxs.push_back(idx);
804 break;
805 default:
806 break;
807 }
808 }
809 assert(!vCarePiIdxs.empty());
810 // find compatible word
811 int iWord = 0;
812 std::vector<word> vCompatibleBits(1);
813 itr it = vCompatibleBits.begin();
814 for(; iWord < nWords; iWord++) {
815 Fill(1, it);
816 for(int idx: vCarePiIdxs) {
817 int id = pNtk->GetPi(idx);
818 bool c;
819 if(vCex[idx] == TRUE) {
820 c = false;
821 } else {
822 assert(vCex[idx] == FALSE);
823 c = true;
824 }
825 itr x = vValues.begin() + id * nWords + iWord;
826 itr y = vAssignedStimuli.begin() + idx * nWords + iWord;
827 And(1, tmp.begin(), x, y, !c, false);
828 And(1, it, it, tmp.begin(), false, true);
829 if(IsZero(1, it)) {
830 break;
831 }
832 }
833 if(!IsZero(1, it)) {
834 break;
835 }
836 }
837 // find compatible bit
838 int iBit;
839 if(iWord < nWords) {
840 assert(!IsZero(1, it));
841 iBit = 0;
842 while(!((*it >> iBit) & 1)) {
843 iBit++;
844 }
845 if(nVerbose) {
846 std::cout << "fusing into stimulus word " << iWord << " bit " << iBit << std::endl;
847 }
848 vPackedCount[iWord * 64 + iBit]++;
849 } else {
850 // no bits are compatible, so reset at pivot
851 iWord = iPivot / 64;
852 iBit = iPivot % 64;
853 if(nVerbose) {
854 std::cout << "resetting stimulus word " << iWord << " bit " << iBit << std::endl;
855 }
856 if(vPackedCount[iWord * 64 + iBit]) {
857 // this can be zero only when stats has been reset
858 vPackedCountEvicted.push_back(vPackedCount[iWord * 64 + iBit]);
859 }
860 vPackedCount[iWord * 64 + iBit] = 1;
861 word mask = 1ull << iBit;
862 for(int idx = 0; idx < pNtk->GetNumPis(); idx++) {
863 vAssignedStimuli[idx * nWords + iWord] &= ~mask;
864 }
865 iPivot++;
866 if(iPivot == 64 * nWords) {
867 iPivot = 0;
868 }
869 }
870 // update stimulus
871 for(int idx: vCarePiIdxs) {
872 int id = pNtk->GetPi(idx);
873 word mask = 1ull << iBit;
874 if(vCex[idx] == TRUE) {
875 vValues[id * nWords + iWord] |= mask;
876 } else {
877 assert(vCex[idx] == FALSE);
878 vValues[id * nWords + iWord] &= ~mask;
879 }
880 vAssignedStimuli[idx * nWords + iWord] |= mask;
881 if(nVerbose) {
882 std::cout << "node " << std::setw(3) << id << ": ";
883 Print(1, vValues.begin() + id * nWords + iWord);
884 std::cout << std::endl;
885 std::cout << "asgn " << std::setw(3) << id << ": ";
886 Print(1, vAssignedStimuli.begin() + idx * nWords + iWord);
887 std::cout << std::endl;
888 }
889 }
890 // simulate
891 SimulateOneWord(iWord);
892 // recompute care with new stimulus
893 time_point timeStart = GetCurrentTime();
894 if(target != -1 && !pNtk->IsPoDriver(target)) {
895 if(nVerbose) {
896 std::cout << "recomputing careset of " << target << std::endl;
897 }
898 vValues2.resize(vValues.size());
899 pNtk->ForEachPi([&](int id) {
900 vValues2[id * nWords + iWord] = vValues[id * nWords + iWord];
901 });
902 pNtk->ForEachInt([&](int id) {
903 vValues2[id * nWords + iWord] = vValues[id * nWords + iWord];
904 });
905 pNtk->ForEachTfo(target, false, [&](int id) {
906 SimulateOneWordNode(vValues2, id, iWord, target);
907 if(nVerbose) {
908 std::cout << "node " << std::setw(3) << id << ": ";
909 Print(1, vValues2.begin() + id * nWords + iWord);
910 std::cout << std::endl;
911 }
912 });
913 Clear(1, care.begin() + iWord);
914 pNtk->ForEachPoDriver([&](int fi) {
915 assert(fi != target);
916 care[iWord] = care[iWord] | (vValues[fi * nWords + iWord] ^ vValues2[fi * nWords + iWord]);
917 });
918 if(nVerbose) {
919 std::cout << "care " << std::setw(3) << target << ": ";
920 Print(1, care.begin() + iWord);
921 std::cout << std::endl;
922 }
923 }
924 durationCare += Duration(timeStart, GetCurrentTime());
925 nCex++;
926 }
assert
#define assert(ex)
Definition util_old.h:213

◆ AssignNetwork()

template<typename Ntk>
void rrr::Simulator< Ntk >::AssignNetwork ( Ntk * pNtk_,
bool fReuse )

Definition at line 690 of file rrrSimulator.h.

690 {
691 if(!fReuse) {
692 fGenerated = false;
693 }
694 fInitialized = false;
695 target = -1;
696 fUpdate = false;
697 sUpdates.clear();
698 pNtk = pNtk_;
699 pNtk->AddCallback(std::bind(&Simulator<Ntk>::ActionCallback, this, std::placeholders::_1));
700 }

◆ CheckFeasibility()

template<typename Ntk>
bool rrr::Simulator< Ntk >::CheckFeasibility ( int id,
int fi,
bool c )

Definition at line 747 of file rrrSimulator.h.

747 {
748 if(!fInitialized) {
749 Initialize();
750 }
751 ComputeCare(id);
752 switch(pNtk->GetNodeType(id)) {
753 case AND: {
754 itr x = vValues.end();
755 bool cx = false;
756 pNtk->ForEachFanin(id, [&](int fi, bool c) {
757 if(x == vValues.end()) {
758 x = vValues.begin() + fi * nWords;
759 cx = c;
760 } else {
761 And(nWords, tmp.begin(), x, vValues.begin() + fi * nWords, cx, c);
762 x = tmp.begin();
763 cx = false;
764 }
765 });
766 if(x == vValues.end()) {
767 x = care.begin();
768 } else {
769 And(nWords, tmp.begin(), x, care.begin(), cx, false);
770 x = tmp.begin();
771 }
772 And(nWords, tmp.begin(), x, vValues.begin() + fi * nWords, false, !c);
773 return IsZero(nWords, tmp.begin());
774 }
775 default:
776 assert(0);
777 }
778 return false;
779 }

◆ CheckRedundancy()

template<typename Ntk>
bool rrr::Simulator< Ntk >::CheckRedundancy ( int id,
int idx )

Definition at line 707 of file rrrSimulator.h.

707 {
708 if(!fInitialized) {
709 Initialize();
710 }
711 ComputeCare(id);
712 switch(pNtk->GetNodeType(id)) {
713 case AND: {
714 itr x = vValues.end();
715 bool cx = false;
716 pNtk->ForEachFaninIdx(id, [&](int idx2, int fi, bool c) {
717 if(idx == idx2) {
718 return;
719 }
720 if(x == vValues.end()) {
721 x = vValues.begin() + fi * nWords;
722 cx = c;
723 } else {
724 And(nWords, tmp.begin(), x, vValues.begin() + fi * nWords, cx, c);
725 x = tmp.begin();
726 cx = false;
727 }
728 });
729 if(x == vValues.end()) {
730 x = care.begin();
731 } else {
732 And(nWords, tmp.begin(), x, care.begin(), cx, false);
733 x = tmp.begin();
734 }
735 int fi = pNtk->GetFanin(id, idx);
736 bool c = pNtk->GetCompl(id, idx);
737 And(nWords, tmp.begin(), x, vValues.begin() + fi * nWords, false, !c);
738 return IsZero(nWords, tmp.begin());
739 }
740 default:
741 assert(0);
742 }
743 return false;
744 }

◆ GetStatsSummary()

template<typename Ntk>
summary< int > rrr::Simulator< Ntk >::GetStatsSummary ( ) const

Definition at line 948 of file rrrSimulator.h.

948 {
949 summary<int> v;
950 v.emplace_back("sim cex", nCex);
951 if(!fKeepStimula) {
952 v.emplace_back("sim discarded cex", nDiscarded);
953 }
954 int nPackedCount = vPackedCountEvicted.size() - nPackedCountOld;
955 for(int count: vPackedCount) {
956 if(count) {
957 nPackedCount++;
958 }
959 }
960 v.emplace_back("sim packed pattern", nPackedCount);
961 v.emplace_back("sim evicted pattern", vPackedCountEvicted.size());
962 return v;
963 };

◆ GetTimesSummary()

template<typename Ntk>
summary< double > rrr::Simulator< Ntk >::GetTimesSummary ( ) const

Definition at line 966 of file rrrSimulator.h.

966 {
967 summary<double> v;
968 v.emplace_back("sim simulation", durationSimulation);
969 v.emplace_back("sim care computation", durationCare);
970 return v;
971 };

◆ ResetSummary()

template<typename Ntk>
void rrr::Simulator< Ntk >::ResetSummary ( )

Definition at line 933 of file rrrSimulator.h.

933 {
934 nCex = 0;
935 nDiscarded = 0;
936 nPackedCountOld = 0;
937 for(int count: vPackedCount) {
938 if(count) {
939 nPackedCountOld++;
940 }
941 }
942 vPackedCountEvicted.clear();
943 durationSimulation = 0;
944 durationCare = 0;
945 };
Here is the caller graph for this function:
The documentation for this class was generated from the following file: