[發(fā)明專利]驗證實例生成方法、裝置、電子設(shè)備及存儲介質(zhì)

在審

• 申請?zhí)枺?/td>: 202111055784.4
• 申請日: 2021-09-09
• 公開（公告）號: CN113850046A
• 公開（公告）日: 2021-12-28
• 發(fā)明（設(shè)計）人: 索健;王正
• 申請（專利權(quán)）人: 愛芯元智半導體（上海）有限公司
• 主分類號: G06F30/398
• 分類號: G06F30/398;G06F111/04
• 代理公司: 北京清亦華知識產(chǎn)權(quán)代理事務(wù)所(普通合伙) 11201
• 代理人: 羅嵐

本申請?zhí)岢鲆环N驗證實例生成方法、裝置、電子設(shè)備及存儲介質(zhì)，其中方法包括：針對驗證環(huán)境中的每個類，配置所述類中的各個變量；針對驗證環(huán)境中的每個實例，對實例需要的已配置的類進行加載處理，并對類中的變量進行約束配置處理；針對實例中的每個約束配置，對約束配置中的各個函數(shù)采用替代函數(shù)庫中對應(yīng)的替代函數(shù)進行替代處理，生成驗證實例。該方法通過對驗證環(huán)境中的實例需要的已配置的類進行約束配置處理，并對約束配置中的函數(shù)采用替代函數(shù)庫中的函數(shù)進行替代，以生成驗證實例。由此，可使生成的驗證實例既滿足復雜約束同時可提高驗證平臺中約束部分的性能，可對后期調(diào)試提供較高的便利性。

技術(shù)領(lǐng)域

本申請涉及計算機技術(shù)領(lǐng)域，尤其涉及一種驗證實例生成方法、裝置、電子設(shè)備及存儲介質(zhì)。

背景技術(shù)

隨著芯片設(shè)計規(guī)模越來越大而復雜，在相關(guān)技術(shù)中，使用隨機約束驗證方法以滿足驗證需求。

但是，在隨機約束驗證方法中，隨著約束(constraints)的尺寸和復雜性的增加，驗證平臺性能也隨之降低，對后期調(diào)試帶來很大不便。

發(fā)明內(nèi)容

本申請旨在至少在一定程度上解決上述技術(shù)中的技術(shù)問題之一。

本申請?zhí)岢鲆环N驗證實例生成方法，以實現(xiàn)對驗證環(huán)境中的實例需要的已配置的類進行約束配置處理，并對約束配置中的函數(shù)采用替代函數(shù)庫中的函數(shù)進行替代，以生成驗證實例，由此，可使生成的驗證實例既滿足復雜約束同時提高驗證平臺中約束部分的性能，可對后期調(diào)試提供較高的便利性。

本申請第一方面實施例提出了一種驗證實例生成方法，包括：針對驗證環(huán)境中的每個類，配置所述類中的各個變量；針對驗證環(huán)境中的每個實例，對所述實例需要的已配置的類進行加載處理，并對所述類中的變量進行約束配置處理；針對所述實例中的每個約束配置，對所述約束配置中的各個函數(shù)采用替代函數(shù)庫中對應(yīng)的替代函數(shù)進行替代處理，生成驗證實例。

本申請實施例的驗證實例生成方法，通過針對驗證環(huán)境中的每個類，配置類中的各個變量；針對驗證環(huán)境中的每個實例，對實例需要的已配置的類進行加載處理，并對類中的變量進行約束配置處理；針對實例中的每個約束配置，對約束配置中的各個函數(shù)采用替代函數(shù)庫中對應(yīng)的替代函數(shù)進行替代處理，生成驗證實例。該方法通過對驗證環(huán)境中的實例需要的已配置的類進行約束配置處理，并對約束配置中的函數(shù)采用替代函數(shù)庫中的函數(shù)進行替代，以生成驗證實例，由此，可使生成的驗證實例既滿足復雜約束同時提高驗證平臺中約束部分的性能，可對后期調(diào)試提供較高的便利性。

可選地，所述針對驗證環(huán)境中的每個類，配置所述類中的各個變量，包括：針對驗證環(huán)境中的每個類，根據(jù)所述類中定義的各個變量以及變量之間關(guān)系，確定所述類中的目標變量，以及所述目標變量對應(yīng)的配置類型；對所述類中的各個所述目標變量按照對應(yīng)的配置類型進行配置。

可選地，所述針對驗證環(huán)境中的每個類，根據(jù)所述類中定義的各個變量以及變量之間關(guān)系，確定所述類中的目標變量，以及所述目標變量對應(yīng)的配置類型，包括：針對驗證環(huán)境中的每個類，針對所述類中的每個變量，判斷所述變量是否滿足預設(shè)配置條件，其中，所述預設(shè)配置條件為所述變量可以根據(jù)所述類中的其他變量計算得到；在所述變量滿足所述預設(shè)配置條件時，確定所述變量為所述目標變量；根據(jù)所述目標變量所定義的參數(shù)的位數(shù)要求，確定所述目標變量對應(yīng)的配置類型。

可選地，所述根據(jù)所述目標變量所定義的參數(shù)的位數(shù)要求，確定所述目標變量對應(yīng)的配置類型，包括：在所述目標變量所定義的參數(shù)的位數(shù)要求為位數(shù)小于等于預設(shè)位數(shù)閾值時，確定所述目標變量對應(yīng)的配置類型為比特類型；在所述目標變量所定義的參數(shù)的位數(shù)要求為位數(shù)大于所述預設(shè)位數(shù)閾值時，確定所述目標變量對應(yīng)的配置類型為整數(shù)類型。

可選地，所述針對驗證環(huán)境中的每個實例，對所述實例需要的已配置的類進行加載處理，并對所述類中的變量進行約束配置處理，包括：針對驗證環(huán)境中的每個實例，對所述實例需要的已配置的類進行加載處理；針對所述實例中加載的每個類，對所述類中的所有變量進行約束配置處理。