Article(id=1241719222749942559, tenantId=1146029695717560320, journalId=1146032081894723586, issueId=1241719216169079576, articleNumber=null, orderNo=3, doi=10.3981/j.issn.2097-0781.2023.01.002, pmid=null, cstr=null, oa=null, hot=null, price=null, onlineType=0, articleFormat=0, articleType=null, articleTypeStr=research-article, receivedDate=1672416000000, receivedDateStr=2022-12-31, revisedDate=1675008000000, revisedDateStr=2023-01-30, acceptedDate=null, acceptedDateStr=null, onlineDate=1679587200000, onlineDateStr=2023-03-24, pubDate=1679241600000, pubDateStr=2023-03-20, doiRegisterDate=null, doiRegisterDateStr=null, onlineIssueDate=1679587200000, onlineIssueDateStr=2023-03-24, onlineJustAcceptDate=null, onlineJustAcceptDateStr=null, onlineFirstDate=null, onlineFirstDateStr=null, sourceXml=null, magXml=null, createTime=1773978532727, creator=sys-migrate, updateTime=1773978532727, updator=sys-migrate, issue=Issue{id=1241719216169079576, tenantId=1146029695717560320, journalId=1146032081894723586, year='2023', volume='2', issue='1', pageStart='5', pageEnd='143', issueExtLink='null', onlineDate='null', pubDate='null', beforeIssueId=null, nextIssueId=null, price=null, status=1, issueComplete=1, articleOrder=1, issueType=-1, specialIssue=1, createTime=1773978531159, creator=sys-migrate, updateTime=1774001248771, updator=13041195026, preIssue=null, nextIssue=null, ext={EN=IssueExt(id=1241814500781916967, tenantId=1146029695717560320, journalId=1146032081894723586, issueId=1241719216169079576, language=EN, specialIssueTitle=Science and Technology Foresight, coverIllustrator=null, specialIssueEditor=null, specialIssueAbout=null), CN=IssueExt(id=1241814500781916968, tenantId=1146029695717560320, journalId=1146032081894723586, issueId=1241719216169079576, language=CN, specialIssueTitle=形式化方法与复杂计算系统可信保障, coverIllustrator=null, specialIssueEditor=null, specialIssueAbout=null)}, issueFiles=null}, startPage=23, endPage=32, ext={EN=ArticleExt(id=1241719228898800381, articleId=1241719222749942559, tenantId=1146029695717560320, journalId=1146032081894723586, language=EN, title=Formal Verification of Circuit Design, columnId=1149656489310208610, journalTitle=Science and Technology Foresight, columnName=Review and Commentary, runingTitle=null, highlight=null, articleAbstract=

The verification of circuit design is to check its correctness and safety, which is vital in the circuit design process and occupies almost half of the cost and time. Formal verification is one of the important ways to guarantee the correctness and safety of software and hardware systems of computers and has been applied to circuit design verification. The electronic design automation (EDA) software from three global EDA giants, i.e., Cadence, Synopsis, and Siemens, all includes mature formal verification tools for circuit design. This paper summarizes the current status of the formal verification of circuit design, analyzes its challenges, discusses its perspectives and trends, and proposes suggestions on its development in China.

, correspAuthors=Zhilin WU, authorNote=null, correspAuthorsNote=, copyrightStatement=null, copyrightOwner=null, extLink=null, articleAbsUrl=null, sourceXml=null, magXml=null, pdfUrl=null, pdf=null, pdfFileSize=null, pdfExtLink=null, richHtmlUrl=null, mobilePdfUrl=null, reviewReport=null, pdfFirstPage=null, abstractGraph=null, abstractGraphContent=null, abstractVideo=null, citation=null, cebUrl=null, magXmlContent=null, mapNumber=null, authorCompany=null, fund=null, authors=null, authorsList=Bohua ZHAN, Zhilin WU), CN=ArticleExt(id=1241719228772971258, articleId=1241719222749942559, tenantId=1146029695717560320, journalId=1146032081894723586, language=CN, title=芯片设计形式验证, columnId=1148708266483446458, journalTitle=前瞻科技, columnName=综述与述评, runingTitle=null, highlight=null, articleAbstract=

芯片设计验证是对芯片设计是否正确与安全进行检查，在芯片设计流程中具有非常重要的地位，占其将近1/2的成本和时间。形式验证是保证计算机软硬件系统正确性与安全性的非常重要的手段，已经成功用于芯片设计验证。全世界三大电子设计自动化（EDA）软件厂商Cadence、Synopsis、Siemens的EDA软件均包含成熟的芯片设计形式验证工具。文章总结了芯片设计形式验证发展现状，分析了面临的挑战，展望了发展趋势，并对其在中国的发展提出建议。

, correspAuthors=吴志林, authorNote=null, correspAuthorsNote=, copyrightStatement=null, copyrightOwner=null, extLink=null, articleAbsUrl=null, sourceXml=etsd3Ud3mCy5QC3AXV6mOA==, magXml=vDBoJtaHBMYXtHWdMYwDgA==, pdfUrl=null, pdf=f/H3iYBd3nTKV+/GZqCHDQ==, pdfFileSize=2157986, pdfExtLink=null, richHtmlUrl=null, mobilePdfUrl=null, reviewReport=null, pdfFirstPage=null, abstractGraph=null, abstractGraphContent=null, abstractVideo=null, citation=null, cebUrl=null, magXmlContent=RwLPigP5CTmwJjszKqUjuw==, mapNumber=null, authorCompany=null, fund=null, authors=, authorsList=詹博华, 吴志林)}, authors=[Author(id=1241719233952936768, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, orderNo=0, firstName=null, middleName=null, lastName=null, nameCn=null, orcid=null, stid=null, country=null, authorPic=null, dead=0, email=bzhan@ios.ac.cn, emailSecond=null, emailThird=null, correspondingAuthor=0, authorType=1, ext={EN=AuthorExt(id=1241719234024239938, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, authorId=1241719233952936768, language=EN, stringName=Bohua ZHAN, firstName=Bohua, middleName=null, lastName=ZHAN, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=null, address=null, bio=null, bioImg=null, bioContent=null, aboutCorrespAuthor=null), CN=AuthorExt(id=1241719234103931715, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, authorId=1241719233952936768, language=CN, stringName=詹博华, firstName=null, middleName=null, lastName=null, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=null, address=null, bio={"img":"3IUc1qq5uTmbMUG0d0MFjg==","content":"

詹博华，副研究员。中国计算机学会形式化方法专业委员会执行委员。主要研究方向为交互式定理证明、嵌入式系统的建模和验证。在形式化方法领域的主要会议和期刊发表论文30余篇。电子信箱：bzhan@ios.ac.cn。

"}, bioImg=3IUc1qq5uTmbMUG0d0MFjg==, bioContent=

詹博华，副研究员。中国计算机学会形式化方法专业委员会执行委员。主要研究方向为交互式定理证明、嵌入式系统的建模和验证。在形式化方法领域的主要会议和期刊发表论文30余篇。电子信箱：bzhan@ios.ac.cn。

, aboutCorrespAuthor=null)}, companyList=null), Author(id=1241719234162651974, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, orderNo=1, firstName=null, middleName=null, lastName=null, nameCn=null, orcid=null, stid=null, country=null, authorPic=null, dead=0, email=wuzl@ios.ac.cn, emailSecond=null, emailThird=null, correspondingAuthor=1, authorType=1, ext={EN=AuthorExt(id=1241719234250732360, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, authorId=1241719234162651974, language=EN, stringName=Zhilin WU, firstName=Zhilin, middleName=null, lastName=WU, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=^†, address=null, bio=null, bioImg=null, bioContent=null, aboutCorrespAuthor=null), CN=AuthorExt(id=1241719234322035530, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, authorId=1241719234162651974, language=CN, stringName=吴志林, firstName=null, middleName=null, lastName=null, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=^†, address=null, bio={"img":"WNRIF6oYa2u4v3WWqOvpLQ==","content":"

吴志林，研究员，博士研究生导师。中国计算机学会形式化方法专业委员会副秘书长。主要研究方向为计算逻辑、自动机理论、计算机软硬件系统的形式验证。先后承担国家重点研发计划、中国科学院A类战略性先导科技专项、中央军委装备发展部预研领域基金、国家自然科学基金等项目10余项。获CCF-IEEE CS青年科学家奖。发表论文40余篇。电子信箱：wuzl@ios.ac.cn。

"}, bioImg=WNRIF6oYa2u4v3WWqOvpLQ==, bioContent=

吴志林，研究员，博士研究生导师。中国计算机学会形式化方法专业委员会副秘书长。主要研究方向为计算逻辑、自动机理论、计算机软硬件系统的形式验证。先后承担国家重点研发计划、中国科学院A类战略性先导科技专项、中央军委装备发展部预研领域基金、国家自然科学基金等项目10余项。获CCF-IEEE CS青年科学家奖。发表论文40余篇。电子信箱：wuzl@ios.ac.cn。

, aboutCorrespAuthor=null)}, companyList=null)], keywords=[Keyword(id=1241719234410115916, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, language=EN, orderNo=1, keyword=circuit design), Keyword(id=1241719234481419086, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, language=EN, orderNo=2, keyword=correctness and safety), Keyword(id=1241719234565305168, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, language=EN, orderNo=3, keyword=electronic design automation), Keyword(id=1241719234628219730, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, language=EN, orderNo=4, keyword=equivalence checking), Keyword(id=1241719234699522900, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, language=EN, orderNo=5, keyword=assertion-based formal verification), Keyword(id=1241719234770826070, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, language=EN, orderNo=6, keyword=satisfiability problem (SAT) solving), Keyword(id=1241719234858906455, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, language=EN, orderNo=7, keyword=model checking), Keyword(id=1241719234917626712, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, language=CN, orderNo=1, keyword=芯片设计), Keyword(id=1241719234976346970, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, language=CN, orderNo=2, keyword=正确性与安全性), Keyword(id=1241719235043455836, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, language=CN, orderNo=3, keyword=电子设计自动化), Keyword(id=1241719235114759006, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, language=CN, orderNo=4, keyword=等价性验证), Keyword(id=1241719235198645088, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, language=CN, orderNo=5, keyword=基于断言的形式验证), Keyword(id=1241719235265753954, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, language=CN, orderNo=6, keyword=命题逻辑可满足性（SAT）求解), Keyword(id=1241719235328668516, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, language=CN, orderNo=7, keyword=模型检测)], refs=[Reference(id=1241719235517412201, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=1986, volume=35, issue=8, pageStart=677, pageEnd=691, url=null, language=null, rfNumber=[1], rfOrder=0, authorNames=Bryant R E, journalName=IEEE Transaction on Computers, refType=null, unstructuredReference=Bryant R E. Graph-based algorithms for Boolean function manipulation[J]. IEEE Transaction on Computers, 1986, 35(8): 677-691., articleTitle=Graph-based algorithms for Boolean function manipulation, refAbstract=null), Reference(id=1241719235584521067, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2022, volume=null, issue=null, pageStart=null, pageEnd=null, url=ftp://vlsi.colorado.edu/pub/, language=null, rfNumber=[2], rfOrder=1, authorNames=Somenzi F, journalName=CUDD: CU decision diagram package release 2.5.0, refType=null, unstructuredReference=Somenzi F. CUDD: CU decision diagram package release 2.5.0[EB/OL]. [2022-12-20]. ftp://vlsi.colorado.edu/pub/., articleTitle=null, refAbstract=null), Reference(id=1241719235664212845, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2022, volume=null, issue=null, pageStart=null, pageEnd=null, url=http://buddy.sourceforge.net, language=null, rfNumber=[3], rfOrder=2, authorNames=Lind-Nielsen J, journalName=BuDDy—A binary decision diagram package, refType=null, unstructuredReference=Lind-Nielsen J. BuDDy—A binary decision diagram package[EB/OL]. [2022-12-20]. http://buddy.sourceforge.net., articleTitle=null, refAbstract=null), Reference(id=1241719235748098927, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=1971, volume=null, issue=null, pageStart=151, pageEnd=158, url=null, language=null, rfNumber=[4], rfOrder=3, authorNames=Cook S A, journalName=Proceedings of the Third Annual ACM Symposium on Theory of Computing, refType=null, unstructuredReference=Cook S A. The complexity of theorem-proving procedures[C]// Proceedings of the Third Annual ACM Symposium on Theory of Computing. New York: ACM Press, 1971: 151-158., articleTitle=The complexity of theorem-proving procedures, refAbstract=null), Reference(id=1241719235811013489, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=10.1145/368273.368557, pmid=null, pmcid=null, year=1962, volume=5, issue=7, pageStart=394, pageEnd=397, url=https://dl.acm.org/doi/10.1145/368273.368557, language=null, rfNumber=[5], rfOrder=4, authorNames=Davis M, Logemann G, Loveland D, journalName=Communications of the ACM, refType=null, unstructuredReference=Davis M, Logemann G, Loveland D. A machine program for theorem proving[J]. Communications of the ACM, 1962, 5(7): 394-397., articleTitle=A machine program for theorem proving, refAbstract=The programming of a proof procedure is discussed in connection with trial runs and possible improvements.), Reference(id=1241719235882316659, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=10.1109/12.769433, pmid=null, pmcid=null, year=1999, volume=48, issue=5, pageStart=506, pageEnd=521, url=http://ieeexplore.ieee.org/document/769433/, language=null, rfNumber=[6], rfOrder=5, authorNames=Marques-Silva J P, Sakallah K A, journalName=IEEE Transactions on Computers, refType=null, unstructuredReference=Marques-Silva J P, Sakallah K A. Grasp: A search algorithm for propositional satisfiability[J]. IEEE Transactions on Computers, 1999, 48(5): 506-521., articleTitle=Grasp: A search algorithm for propositional satisfiability, refAbstract=null), Reference(id=1241719235941036917, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=10.1145/5397.5399, pmid=null, pmcid=null, year=1986, volume=8, issue=2, pageStart=244, pageEnd=263, url=https://dl.acm.org/doi/10.1145/5397.5399, language=null, rfNumber=[7], rfOrder=6, authorNames=Clarke E M, Emerson E A, Sistla A P, journalName=ACM Transactions on Programming Languages and Systems, refType=null, unstructuredReference=Clarke E M, Emerson E A, Sistla A P. Automatic verification of finite-state concurrent systems using temporal logic specifications[J]. ACM Transactions on Programming Languages and Systems, 1986, 8(2): 244-263., articleTitle=Automatic verification of finite-state concurrent systems using temporal logic specifications, refAbstract=We give an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a (propositional, branching-time) temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global state graph for the concurrent system. We also show how this approach can be adapted to handle fairness. We argue that our technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems. Experimental results show that state machines with several hundred states can be checked in a matter of seconds.), Reference(id=1241719236016534391, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=1982, volume=null, issue=null, pageStart=337, pageEnd=351, url=null, language=null, rfNumber=[8], rfOrder=7, authorNames=Queille J P, Sifakis J, journalName=Proceedings of the International Symposium on Programming. Berlin, refType=null, unstructuredReference=Queille J P, Sifakis J. Specification and verification of concurrent systems in CESAR[C]// Proceedings of the International Symposium on Programming. Berlin, Heidelberg: Springer, 1982: 337-351., articleTitle=Specification and verification of concurrent systems in CESAR, refAbstract=null), Reference(id=1241719236092031865, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=null, volume=null, issue=null, pageStart=332, pageEnd=344, url=null, language=null, rfNumber=[9], rfOrder=8, authorNames=Vardi M Y, Wolper P, journalName=Proceedings of the Logic in Computer Science (LICS). Piscataway:IEEE Press, 1986, refType=null, unstructuredReference=Vardi M Y, Wolper P. An automata-theoretic approach to automatic program verification (preliminary report)[C]// Proceedings of the Logic in Computer Science (LICS). Piscataway:IEEE Press, 1986: 332-344., articleTitle=An automata-theoretic approach to automatic program verification (preliminary report), refAbstract=null), Reference(id=1241719236163335035, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=1993, volume=null, issue=null, pageStart=409, pageEnd=423, url=null, language=null, rfNumber=[10], rfOrder=9, authorNames=Peled D, journalName=Courcoubetis C. Proceedings of the 5th International Conference on Computer Aided Verification. Berlin, refType=null, unstructuredReference=Peled D. All from one, one for all: On model checking using representatives[C]// Courcoubetis C. Proceedings of the 5th International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 1993: 409-423., articleTitle=All from one, one for all: On model checking using representatives, refAbstract=null), Reference(id=1241719237669090173, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=10.1016/0890-5401(92)90017-A, pmid=null, pmcid=null, year=1992, volume=98, issue=2, pageStart=142, pageEnd=170, url=https://linkinghub.elsevier.com/retrieve/pii/089054019290017A, language=null, rfNumber=[11], rfOrder=10, authorNames=Burch J R, Clarke E M, McMillan K L, journalName=Information and Computation, refType=null, unstructuredReference=Burch J R, Clarke E M, McMillan K L, et al. Symbolic model checking: 1020 states and beyond[J]. Information and Computation, 1992, 98(2): 142-170., articleTitle=Symbolic model checking: 1020 states and beyond, refAbstract=null), Reference(id=1241719237744587647, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=1993, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[12], rfOrder=11, authorNames=McMillan K L, journalName=Symbolic model checking, refType=null, unstructuredReference=McMillan K L. Symbolic model checking[M]. Boston: Kluwer Academic Publishers, 1993., articleTitle=null, refAbstract=null), Reference(id=1241719237820085122, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=1999, volume=null, issue=null, pageStart=193, pageEnd=207, url=null, language=null, rfNumber=[13], rfOrder=12, authorNames=Biere A, Cimatti A, Clarke E, journalName=Cleavelond W R.Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, refType=null, unstructuredReference=Biere A, Cimatti A, Clarke E, et al. Symbolic model checking without BDDs[C]// Cleavelond W R.Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer, 1999: 193-207., articleTitle=Symbolic model checking without BDDs, refAbstract=null), Reference(id=1241719237912359811, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2000, volume=null, issue=null, pageStart=108, pageEnd=125, url=null, language=null, rfNumber=[14], rfOrder=13, authorNames=Sheeran M, Singh S, Stålmarck G, journalName=Hunt W A, Jr Johnson S D.Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design. Berlin, refType=null, unstructuredReference=Sheeran M, Singh S, Stålmarck G. Checking safety properties using induction and a SAT-solver[C]// Hunt W A, Jr Johnson S D.Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design. Berlin, Heidelberg: Springer, 2000: 108-125., articleTitle=Checking safety properties using induction and a SAT-solver, refAbstract=null), Reference(id=1241719237987857285, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2003, volume=null, issue=null, pageStart=1, pageEnd=13, url=null, language=null, rfNumber=[15], rfOrder=14, authorNames=McMillan K L, journalName=Hunt W A, Jr.Somenzi F.Proceedings of the 15th International Conference on Computer Aided Verification, refType=null, unstructuredReference=McMillan K L. Interpolation and SAT-based model checking[C]// Hunt W A, Jr.Somenzi F.Proceedings of the 15th International Conference on Computer Aided Verification. Cham: Springer, 2003: 1-13., articleTitle=Interpolation and SAT-based model checking, refAbstract=null), Reference(id=1241719238080131975, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2011, volume=null, issue=null, pageStart=70, pageEnd=87, url=null, language=null, rfNumber=[16], rfOrder=15, authorNames=Bradley A R, journalName=Jhala R, Schmidt D.Proceedings of the 12th International Conference on Verification Model Checking and Abstract Interpretation. Berlin, refType=null, unstructuredReference=Bradley A R. SAT-based model checking without unrolling[C]// Jhala R, Schmidt D.Proceedings of the 12th International Conference on Verification Model Checking and Abstract Interpretation. Berlin, Heidelberg: Springer, 2011, 70-87., articleTitle=SAT-based model checking without unrolling, refAbstract=null), Reference(id=1241719238155629449, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2011, volume=null, issue=null, pageStart=125, pageEnd=134, url=null, language=null, rfNumber=[17], rfOrder=16, authorNames=Eén N, Mishchenko A, Brayton R, journalName=Proceedings of the International Conference on Formal Methods in Computer-Aided Design, refType=null, unstructuredReference=Eén N, Mishchenko A, Brayton R. Efficient implementation of property directed reachability[C]// Proceedings of the International Conference on Formal Methods in Computer-Aided Design. Piscataway: IEEE Press, 2011: 125-134., articleTitle=Efficient implementation of property directed reachability, refAbstract=null), Reference(id=1241719238210155403, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2002, volume=null, issue=null, pageStart=33, pageEnd=51, url=null, language=null, rfNumber=[18], rfOrder=17, authorNames=Chauhan P, Clarke E M, Kukula J H, journalName=Aagaard M D, O’Leary J W.Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design. Berlin, refType=null, unstructuredReference=Chauhan P, Clarke E M, Kukula J H, et al. Automated abstraction refinement for model checking large state spaces using SAT-based conflict analysis[C]// Aagaard M D, O’Leary J W.Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design. Berlin, Heidelberg: Springer, 2002: 33-51., articleTitle=Automated abstraction refinement for model checking large state spaces using SAT-based conflict analysis, refAbstract=null), Reference(id=1241719238277264269, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=1997, volume=null, issue=null, pageStart=72, pageEnd=83, url=null, language=null, rfNumber=[19], rfOrder=18, authorNames=Graf S, Saidi H, journalName=Grumberg O. Proceedings of the 9th International Conference on Computer Aided Verification, refType=null, unstructuredReference=Graf S, Saidi H. Construction of abstract state graphs with PVS[C]// Grumberg O. Proceedings of the 9th International Conference on Computer Aided Verification. Cham: Springer, 1997: 72-83., articleTitle=Construction of abstract state graphs with PVS, refAbstract=null), Reference(id=1241719238344373135, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=10.1145/876638.876643, pmid=null, pmcid=null, year=2003, volume=50, issue=5, pageStart=752, pageEnd=794, url=https://dl.acm.org/doi/10.1145/876638.876643, language=null, rfNumber=[20], rfOrder=19, authorNames=Clarke E M, Grumberg O, Jha S, journalName=Journal of the ACM, refType=null, unstructuredReference=Clarke E M, Grumberg O, Jha S, et al. Counterexample-guided abstraction refinement for symbolic model checking[J]. Journal of the ACM, 2003, 50(5): 752-794., articleTitle=Counterexample-guided abstraction refinement for symbolic model checking, refAbstract=The state explosion problem remains a major hurdle in applying symbolic model checking to large hardware designs. State space abstraction, having been essential for verifying designs of industrial complexity, is typically a manual process, requiring considerable creativity and insight.In this article, we present an automatic iterative abstraction-refinement methodology that extends symbolic model checking. In our method, the initial abstract model is generated by an automatic analysis of the control structures in the program to be verified. Abstract models may admit erroneous (or \"spurious\") counterexamples. We devise new symbolic techniques that analyze such counterexamples and refine the abstract model correspondingly. We describe aSMV, a prototype implementation of our methodology in NuSMV. Practical experiments including a large Fujitsu IP core design with about 500 latches and 10000 lines of SMV code confirm the effectiveness of our approach.), Reference(id=1241719238407287697, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=10.1016/S0167-6423(99)00030-1, pmid=null, pmcid=null, year=2000, volume=37, issue=1/3, pageStart=279, pageEnd=309, url=https://linkinghub.elsevier.com/retrieve/pii/S0167642399000301, language=null, rfNumber=[21], rfOrder=20, authorNames=McMillan K L, journalName=Science of Computer Programming, refType=null, unstructuredReference=McMillan K L. A methodology for hardware verification using compositional model checking[J]. Science of Computer Programming, 2000, 37(1/3): 279-309., articleTitle=A methodology for hardware verification using compositional model checking, refAbstract=null), Reference(id=1241719238482785171, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2001, volume=null, issue=null, pageStart=179, pageEnd=195, url=null, language=null, rfNumber=[22], rfOrder=21, authorNames=McMillan K L, journalName=Margaria T, Melham T.Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods. Berlin, refType=null, unstructuredReference=McMillan K L. Parameterized verification of the FLASH cache coherence protocol by compositional model checking[C]// Margaria T, Melham T.Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods. Berlin, Heidelberg: Springer, 2001: 179-195., articleTitle=Parameterized verification of the FLASH cache coherence protocol by compositional model checking, refAbstract=null), Reference(id=1241719238545699733, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=null, volume=null, issue=null, pageStart=397, pageEnd=402, url=null, language=null, rfNumber=[23], rfOrder=22, authorNames=Beatty D L, Bryant R E, Seger C J, journalName=Proceedings of the 28th ACM/IEEE Design Automation Conference (DAC). New York:ACM Press, 1991, refType=null, unstructuredReference=Beatty D L, Bryant R E, Seger C J. Formal hardware verification by symbolic ternary trajectory evaluation[C]// Proceedings of the 28th ACM/IEEE Design Automation Conference (DAC). New York:ACM Press, 1991: 397-402., articleTitle=Formal hardware verification by symbolic ternary trajectory evaluation, refAbstract=null), Reference(id=1241719238612808599, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=1999, volume=null, issue=null, pageStart=323, pageEnd=340, url=null, language=null, rfNumber=[24], rfOrder=23, authorNames=Aagaard M, Jones R B, Seger C J H, DowekG, HirschowitzA, journalName=Bertot Y, refType=null, unstructuredReference=Aagaard M, Jones R B, Seger C J H. Lifted-FL: A pragmatic implementation of combined model checking and theorem proving[C]// Bertot Y, DowekG, HirschowitzA, et al. Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics (TPHOLs). Berlin, Heidelberg: Springer, 1999: 323-340., articleTitle=Lifted-FL: A pragmatic implementation of combined model checking and theorem proving, refAbstract=null), Reference(id=1241719238679917465, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2009, volume=null, issue=null, pageStart=414, pageEnd=429, url=null, language=null, rfNumber=[25], rfOrder=24, authorNames=Kaivola R, Ghughal R, Narasimhan N, journalName=Bouajjani A, Maler O. Proceedings of the 21st International Conference on Computer Aided Verification, refType=null, unstructuredReference=Kaivola R, Ghughal R, Narasimhan N, et al. Replacing testing with formal verification in Intel Core^TM i7 processor execution engine validation[C]// Bouajjani A, Maler O. Proceedings of the 21st International Conference on Computer Aided Verification. Cham: Springer, 2009: 414-429., articleTitle=Replacing testing with formal verification in Intel Core^TM i7 processor execution engine validation, refAbstract=null), Reference(id=1241719238738637723, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2022, volume=null, issue=null, pageStart=null, pageEnd=null, url=http://www.deepchip.com/items/0558-05.html, language=null, rfNumber=[26], rfOrder=25, authorNames=Hogan J, journalName=Cadence, Mentor, OneSpin, Real Intent, Synopsys formal, refType=null, unstructuredReference=Hogan J. Cadence, Mentor, OneSpin, Real Intent, Synopsys formal[EB/OL]. [2022-12-20]. http://www.deepchip.com/items/0558-05.html., articleTitle=null, refAbstract=null), Reference(id=1241719238797357981, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2010, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[27], rfOrder=26, authorNames=IEEE Standard, journalName=Piscataway, refType=null, unstructuredReference=IEEE Standard 1850-2010. Property specification language (PSL)[S]. Piscataway: IEEE Press, 2010., articleTitle=null, refAbstract=null), Reference(id=1241719238860272543, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=1800, volume=null, issue=null, pageStart=null, pageEnd=2009, url=null, language=null, rfNumber=[28], rfOrder=27, authorNames=IEEE Standard, journalName=Piscataway, refType=null, unstructuredReference=IEEE Standard 1800-2009. SystemVerilog—Unified hardware design, specification, and verification language[S]. Piscataway: IEEE Press, 2009., articleTitle=null, refAbstract=null), Reference(id=1241719238939964321, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=10.1109/43.748158, pmid=null, pmcid=null, year=1999, volume=18, issue=3, pageStart=282, pageEnd=292, url=http://ieeexplore.ieee.org/document/748158/, language=null, rfNumber=[29], rfOrder=28, authorNames=Lin C C, Chen K C, Marek-Sadowska M, journalName=IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, refType=null, unstructuredReference=Lin C C, Chen K C, Marek-Sadowska M. Logic synthesis for engineering change[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1999, 18(3): 282-292., articleTitle=Logic synthesis for engineering change, refAbstract=null), Reference(id=1241719239011267491, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2020, volume=null, issue=null, pageStart=413, pageEnd=422, url=null, language=null, rfNumber=[30], rfOrder=29, authorNames=Goel A, Sakallah K A, journalName=Biere A, Parker D.Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, refType=null, unstructuredReference=Goel A, Sakallah K A. AVR: Abstractly Verifying Reachability[C]// Biere A, Parker D.Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer, 2020: 413-422., articleTitle=AVR: Abstractly Verifying Reachability, refAbstract=null), Reference(id=1241719239090959269, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2021, volume=null, issue=null, pageStart=461, pageEnd=474, url=null, language=null, rfNumber=[31], rfOrder=30, authorNames=Mann M, Irfan A, Lonsing F, journalName=Silva A, Leino K R M.Proceedings of the 33rd International Conference on Computer Aided Verification, refType=null, unstructuredReference=Mann M, Irfan A, Lonsing F, et al. Pono: A flexible and extensible SMT-based model checker[C]// Silva A, Leino K R M.Proceedings of the 33rd International Conference on Computer Aided Verification. Cham: Springer, 2021: 461-474., articleTitle=Pono: A flexible and extensible SMT-based model checker, refAbstract=null), Reference(id=1241719239158068135, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2014, volume=null, issue=null, pageStart=260, pageEnd=276, url=null, language=null, rfNumber=[32], rfOrder=31, authorNames=Vizel Y, Gurfinkel A, journalName=Biere A, Bloem R.Proceedings of the the 26th International Conference on Computer Aided Verification, refType=null, unstructuredReference=Vizel Y, Gurfinkel A. Interpolating property directed reachability[C]// Biere A, Bloem R.Proceedings of the the 26th International Conference on Computer Aided Verification. Cham: Springer, 2014: 260-276., articleTitle=Interpolating property directed reachability, refAbstract=null), Reference(id=1241719239229371305, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2014, volume=null, issue=null, pageStart=849, pageEnd=865, url=null, language=null, rfNumber=[33], rfOrder=32, authorNames=Lee S, Sakallah K A, journalName=Proceedings of Computer Aided Verification, Lecture Notes in Computer Science, refType=null, unstructuredReference=Lee S, Sakallah K A. Unbounded scalable verification based on approximate property-directed reachability and datapath abstraction[C]// Proceedings of Computer Aided Verification, Lecture Notes in Computer Science. Cham: Springer, 2014: 849-865., articleTitle=Unbounded scalable verification based on approximate property-directed reachability and datapath abstraction, refAbstract=null), Reference(id=1241719239292285867, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2013, volume=null, issue=null, pageStart=791, pageEnd=796, url=null, language=null, rfNumber=[34], rfOrder=33, authorNames=Welp T, Kuehlmann A, journalName=Proceedings of Design, Automation & Test in Europe Conference (DATE). San Jose, refType=null, unstructuredReference=Welp T, Kuehlmann A. QF_BV model checking with property directed reachability[C]// Proceedings of Design, Automation & Test in Europe Conference (DATE). San Jose, CA: EDA Consortium, 2013: 791-796., articleTitle=QF_BV model checking with property directed reachability, refAbstract=null), Reference(id=1241719239359394733, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2019, volume=null, issue=null, pageStart=166, pageEnd=185, url=null, language=null, rfNumber=[35], rfOrder=34, authorNames=Goel A, Sakallah K A, journalName=Bodger J M, Rozier K Y.Proceedings of the 11th International Symposium on NASA Formal Methods, refType=null, unstructuredReference=Goel A, Sakallah K A. Model checking of Verilog RTL using IC3 with syntax-guided abstraction[C]// Bodger J M, Rozier K Y.Proceedings of the 11th International Symposium on NASA Formal Methods. Cham: Springer Nature Switzerland AG, 2019: 166-185., articleTitle=Model checking of Verilog RTL using IC3 with syntax-guided abstraction, refAbstract=null), Reference(id=1241719239413920687, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2021, volume=null, issue=null, pageStart=325, pageEnd=349, url=null, language=null, rfNumber=[36], rfOrder=35, authorNames=Zhang H, Gupta A, Malik S, journalName=Beyer D, Zufferey D.Proceedings of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation, refType=null, unstructuredReference=Zhang H, Gupta A, Malik S. Syntax-guided synthesis for lemma generation in hardware model checking[C]// Beyer D, Zufferey D.Proceedings of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation. Cham: Springer, 2021: 325-349., articleTitle=Syntax-guided synthesis for lemma generation in hardware model checking, refAbstract=null), Reference(id=1241719239489418161, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2020, volume=null, issue=null, pageStart=373, pageEnd=389, url=null, language=null, rfNumber=[37], rfOrder=36, authorNames=Luo C, Hoos H H, Cai S, PreussM, DeutzA, journalName=Bäck T, refType=null, unstructuredReference=Luo C, Hoos H H, Cai S. PbO-CCSAT: Boosting local search for satisfiability using programming by optimisation[C]// Bäck T, PreussM, DeutzA, et al.Proceedigns of the 16th International Conference on Parallel Problem Solving from Nature—PPSN XVI. Cham: Springer, 2020: 373-389., articleTitle=PbO-CCSAT: Boosting local search for satisfiability using programming by optimisation, refAbstract=null), Reference(id=1241719239552332723, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=10.1613/jair.2490, pmid=null, pmcid=null, year=2008, volume=32, issue=null, pageStart=565, pageEnd=606, url=https://jair.org/index.php/jair/article/view/10556, language=null, rfNumber=[38], rfOrder=37, authorNames=Xu L, Hutter F, Hoos H H, journalName=Journal of Artificial Intelligence Research, refType=null, unstructuredReference=Xu L, Hutter F, Hoos H H, et al. SATzilla: Portfolio-based algorithm selection for SAT[J]. Journal of Artificial Intelligence Research, 2008, 32: 565-606., articleTitle=SATzilla: Portfolio-based algorithm selection for SAT, refAbstract=It has been widely observed that there is no single \"dominant\" SAT solver; instead, different solvers perform best on different instances. Rather than following the traditional approach of choosing the best solver for a given class of instances, we advocate making this decision online on a per-instance basis. Building on previous work, we describe SATzilla, an automated approach for constructing per-instance algorithm portfolios for SAT that use so-called empirical hardness models to choose among their constituent solvers. This approach takes as input a distribution of problem instances and a set of component solvers, and constructs a portfolio optimizing a given objective function (such as mean runtime, percent of instances solved, or score in a competition). The excellent performance of SATzilla was independently verified in the 2007 SAT Competition, where our SATzilla07 solvers won three gold, one silver and one bronze medal. In this article, we go well beyond SATzilla07 by making the portfolio construction scalable and completely automated, and improving it by integrating local search solvers as candidate solvers, by predicting performance score instead of runtime, and by using hierarchical hardness models that take into account different types of SAT instances. We demonstrate the effectiveness of these new techniques in extensive experimental results on data sets including instances from the most recent SAT competition.), Reference(id=1241719239619441589, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=null, volume=null, issue=null, pageStart=707, pageEnd=721, url=null, language=null, rfNumber=[39], rfOrder=38, authorNames=Zhu H, Magill S, Jagannathan S, journalName=Proceedings of ACM-SIGPLAN Symposium on Programming Language Design and Implementation (PLDI). New York:ACM Press, 2018, refType=null, unstructuredReference=Zhu H, Magill S, Jagannathan S. A data-driven CHC solver[C]// Proceedings of ACM-SIGPLAN Symposium on Programming Language Design and Implementation (PLDI). New York:ACM Press, 2018: 707-721., articleTitle=A data-driven CHC solver, refAbstract=null), Reference(id=1241719239699133367, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2020, volume=null, issue=null, pageStart=151, pageEnd=164, url=null, language=null, rfNumber=[40], rfOrder=39, authorNames=Si X, Naik Aa, Dai H, journalName=Lahiri S K, Wang C.Proceedings of the 32nd International Conference on Computer Aided Verification, refType=null, unstructuredReference=Si X, Naik Aa, Dai H, et al. Code2Inv: A deep learning framework for program verification[C]// Lahiri S K, Wang C.Proceedings of the 32nd International Conference on Computer Aided Verification. Cham: Springer, 2020: 151-164., articleTitle=Code2Inv: A deep learning framework for program verification, refAbstract=null), Reference(id=1241719239770436537, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2012, volume=null, issue=null, pageStart=1216, pageEnd=1225, url=null, language=null, rfNumber=[41], rfOrder=40, authorNames=Bachrach J, Vo H, Richards B C, journalName=Proceedings of Design Automation Conference 2012, refType=null, unstructuredReference=Bachrach J, Vo H, Richards B C, et al. Chisel: Constructing hardware in a scala embedded language[C]// Proceedings of Design Automation Conference 2012. Piscataway: IEEE Press, 2012: 1216-1225., articleTitle=Chisel: Constructing hardware in a scala embedded language, refAbstract=null), Reference(id=1241719239850128315, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2022, volume=null, issue=null, pageStart=null, pageEnd=null, url=https://circt.llvm.org/, language=null, rfNumber=[42], rfOrder=41, authorNames=null, journalName=CIRCT, refType=null, unstructuredReference=CIRCT[EB/OL]. [2022-12-20]. https://circt.llvm.org/., articleTitle=null, refAbstract=null), Reference(id=1241719239913042877, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, doi=null, pmid=null, pmcid=null, year=2016, volume=null, issue=null, pageStart=393, pageEnd=405, url=null, language=null, rfNumber=[43], rfOrder=42, authorNames=Liu S, Du Z, Tao J, journalName=Proceedings of the 2016 ACM/IEEE 43rd Annual International Symposium on Computer Architecture, refType=null, unstructuredReference=Liu S, Du Z, Tao J, et al. Cambricon: An instruction set architecture for neural networks[C]// Proceedings of the 2016 ACM/IEEE 43rd Annual International Symposium on Computer Architecture. Piscataway: IEEE Press, 2016: 393-405., articleTitle=Cambricon: An instruction set architecture for neural networks, refAbstract=null)], funds=[Fund(id=1241719235433526119, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, awardId=2021ZD0113300, language=CN, fundingSource=国家重点研发计划(2021ZD0113300), fundOrder=null, country=null)], companyList=[AuthorCompany(id=1241719233873244988, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, xref=null, ext=[AuthorCompanyExt(id=1241719233881633597, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, companyId=1241719233873244988, language=EN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China), AuthorCompanyExt(id=1241719233894216510, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719222749942559, companyId=1241719233873244988, language=CN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=中国科学院软件研究所计算机科学国家重点实验室，北京 100190)])], figs=null, attaches=null, journal=Journal(id=1129340393107079197, delFlag=0, nameCn=前瞻科技, nameEn=Science and Technology Foresight, nameHistory1=null, nameHistory2=null, issn=2097-0781, eissn=, cn=10-1786/N, coden=null, periodic=2, language=CN, oaType=null, ccby=null, superviseOffice=null, ownerOffice=null, pubOffice=null, editorOffice=null, officeType=null, aims=null, clcCode=null, officeProv=null, officeCity=null, officeAddr=null, officeZip=null, officeEmail=null, officePhone=null, editDirector=null, officeDirector=null, officeDirectorPhone=null, officeStaffNum=null, officeEmpNum=null, coverPicUrl=ti95jJIJzXaf02YNe1UF2A==, journalPrice=null, startedYear=null, abbrevIsoEn=Sci Technol Fore, journalRemark=null, publicationField=null, createdTime=null, updatedTime=1757931223825, createdBy=null, updatedBy=15831073675, firstLetterCn=S, firstLetterEn=S, subjectCode=Natural Sciences, subjectName=自然科学, subjectCodeEn=Natural Sciences, subjectNameEn=null, picCn=ti95jJIJzXaf02YNe1UF2A==, picEn=cuGsq8KPhoqtfsQROuZvoQ==, jcr=null, cjcr=null, exts=[JournalExt(id=1174411930946125939, language=CN, name=前瞻科技, nameHistory1=null, nameHistory2=null, managedBy=, sponsoredBy=, publishedBy=, editorOffice=, officeProv=null, officeCity=null, officeAddr=, officeZip=, editDirector=null, officeDirector=null, officePhone=null, coverPicUrl=null, journalRemark=, submitArticleUrl=null, websiteUrl=http://www.qianzhankeji.cn/CN/2097-0781/home.shtml, createdTime=1757931223856, updatedTime=1757931223856, createdBy=15831073675, updatedBy=15831073675, submissionGuidelinesUrl=http://www.qianzhankeji.cn/CN/column/column7.shtml, submissionAuthorUrl=https://qzkjauthor.cast.org.cn/webm/, submissionEditorUrl=https://qzkjeditor.cast.org.cn/webm/, submissionReviewUrl=https://qzkjauthor.cast.org.cn/webm/, submissionCeEditorUrl=https://qzkjeditor.cast.org.cn/webm/, submissionAeEditorUrl=https://qzkjeditor.cast.org.cn/webm/, option={"copyright":""}), JournalExt(id=1174411931076149364, language=EN, name=Science and Technology Foresight, nameHistory1=null, nameHistory2=null, managedBy=, sponsoredBy=, publishedBy=, editorOffice=, officeProv=null, officeCity=null, officeAddr=, officeZip=, editDirector=null, officeDirector=null, officePhone=null, coverPicUrl=null, journalRemark=, submitArticleUrl=null, websiteUrl=http://www.qianzhankeji.cn/EN/2097-0781/home.shtml, createdTime=1757931223887, updatedTime=1757931223887, createdBy=15831073675, updatedBy=15831073675, submissionGuidelinesUrl=http://www.qianzhankeji.cn/EN/column/column7.shtml, submissionAuthorUrl=https://qzkjauthor.manuscriptcloud.com/login, submissionEditorUrl=https://qzkjeditor.manuscriptcloud.com/login, submissionReviewUrl=https://qzkjauthor.manuscriptcloud.com/login, submissionCeEditorUrl=https://qzkjeditor.manuscriptcloud.com/login, submissionAeEditorUrl=https://qzkjeditor.manuscriptcloud.com/login, option={"copyright":""})], databaseList=null, tenantJournalId=1146032081894723586, websiteList=[Website(id=1148243202353652128, webName=null, webTitle=null, webDomain=null, webCopyrigh=null, webIpcNo=null, seoTitle=null, seoKeywords=null, seoDescription=null, tenantJournalId=null, journalId=1146032081894723586, journalNameCn=null, journalNameEn=null, grayFlag=null, tenantId=1146029695717560320, platformId=null, journalGroupId=null, journalGroupNameCn=null, journalGroupNameEn=null, type=1, domain=https://castjournals.cast.org.cn/joweb/qzkj/CN, language=CN, createTime=1751692112768, createBy=18614031015, updateTime=1753516254852, updateBy=18614031015, name=《前瞻科技》中文站点, tplId=1146099689490845704, title=前瞻科技, delFlag=0, indexPage=/home, props=[WebsiteProps(id=1148618977242275853, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=articleTextType, value=kx, createTime=1751781704483, updateTime=1751781704483, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977217110026, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=banner, value=null, createTime=1751781704477, updateTime=1751781704477, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977204527113, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=logo, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic?fileId=skpCN5mVIzgEJbdUXu8/8A==, createTime=1751781704474, updateTime=1751781704474, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977233887244, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=picServerUrl, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic, createTime=1751781704481, updateTime=1751781704481, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977225498635, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=staticResourcePath, value=https://castjournals.cast.org.cn/joweb/cast_kjdb_cn_619/, createTime=1751781704479, updateTime=1751781704479, creator=18614031015, updator=18614031015)]), Website(id=1155894377965830154, webName=null, webTitle=null, webDomain=null, webCopyrigh=null, webIpcNo=null, seoTitle=null, seoKeywords=null, seoDescription=null, tenantJournalId=null, journalId=1146032081894723586, journalNameCn=null, journalNameEn=null, grayFlag=null, tenantId=1146029695717560320, platformId=null, journalGroupId=null, journalGroupNameCn=null, journalGroupNameEn=null, type=1, domain=https://castjournals.cast.org.cn/joweb/qzkj/EN, language=EN, createTime=1753516295187, createBy=18614031015, updateTime=1753516295187, updateBy=18614031015, name=《前瞻科技》英文站点, tplId=1146101810881728533, title=Science and Technology Foresight, delFlag=0, indexPage=/home, props=[WebsiteProps(id=1155894740970233959, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=articleTextType, value=kx, createTime=1753516381733, updateTime=1753516381733, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740953456740, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=banner, value=null, createTime=1753516381729, updateTime=1753516381729, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740945068131, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=logo, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic?fileId=skpCN5mVIzgEJbdUXu8/8A==, createTime=1753516381727, updateTime=1753516381727, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740966039654, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=picServerUrl, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic, createTime=1753516381732, updateTime=1753516381732, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740961845349, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=staticResourcePath, value=https://castjournals.cast.org.cn/joweb/cast_kjdb_cn_619/, createTime=1753516381731, updateTime=1753516381731, creator=18614031015, updator=18614031015)])], journalTitle=前瞻科技, weixinUrl=null, journalUrl=null, iacademicId=null, status=0, seqNo=null, journalTitleEn=Science and Technology Foresight, journalPhotoCn=ti95jJIJzXaf02YNe1UF2A==, journalPhotoEn=cuGsq8KPhoqtfsQROuZvoQ==, journalFirstLetter=S, journalRecommend=null, journalNew=null, journalCollection=null, jcrJf=null, cjcrJf=null, jcrJfStr=null, cjcrJfStr=null, submissionFirstDecision=null, sciSubjectClassification=null, casSubjectClassification=null, citeScore=null, totalCitationFrequency=null, icpCode=null, psCode=null, advertisingLicenseCode=null, copyrightInformation=null, country=null, option=, provinceCode=null, provinceName=null, collectFlag=false), detailUrlCn=https://castjournals.cast.org.cn/joweb/qzkj/CN/10.3981/j.issn.2097-0781.2023.01.002, detailUrlEn=https://castjournals.cast.org.cn/joweb/qzkj/EN/10.3981/j.issn.2097-0781.2023.01.002, pdfUrlCn=https://castjournals.cast.org.cn/joweb/qzkj/CN/PDF/10.3981/j.issn.2097-0781.2023.01.002, pdfUrlEn=https://castjournals.cast.org.cn/joweb/qzkj/EN/PDF/10.3981/j.issn.2097-0781.2023.01.002, aliStartDate=null, aliEndDate=null, collectionFlag=false, citedCount=null, citedUrl=null, reference=null)