[go: up one dir, main page]

CN119397969A - Bus verification method, device, electronic equipment and readable storage medium - Google Patents

Bus verification method, device, electronic equipment and readable storage medium Download PDF

Info

Publication number
CN119397969A
CN119397969A CN202411997230.XA CN202411997230A CN119397969A CN 119397969 A CN119397969 A CN 119397969A CN 202411997230 A CN202411997230 A CN 202411997230A CN 119397969 A CN119397969 A CN 119397969A
Authority
CN
China
Prior art keywords
file
verified
bus
identifiable
node
Prior art date
Legal status (The legal status is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the status listed.)
Granted
Application number
CN202411997230.XA
Other languages
Chinese (zh)
Other versions
CN119397969B (en
Inventor
梁爽
杨华
唐丹
包云岗
Current Assignee (The listed assignees may be inaccurate. Google has not performed a legal analysis and makes no representation or warranty as to the accuracy of the list.)
Beijing Open Source Chip Research Institute
Original Assignee
Beijing Open Source Chip Research Institute
Priority date (The priority date is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the date listed.)
Filing date
Publication date
Application filed by Beijing Open Source Chip Research Institute filed Critical Beijing Open Source Chip Research Institute
Priority to CN202411997230.XA priority Critical patent/CN119397969B/en
Priority claimed from CN202411997230.XA external-priority patent/CN119397969B/en
Publication of CN119397969A publication Critical patent/CN119397969A/en
Application granted granted Critical
Publication of CN119397969B publication Critical patent/CN119397969B/en
Active legal-status Critical Current
Anticipated expiration legal-status Critical

Links

Landscapes

  • Debugging And Monitoring (AREA)

Abstract

The embodiment of the invention provides a bus verification method, a bus verification device, electronic equipment and a readable storage medium. The method comprises the steps of obtaining a sub-file to be verified of a bus to be verified, analyzing characters contained in the sub-file to be verified to convert the sub-file to be verified into an identifiable file identifiable by a target verification tool, and inputting the identifiable file into the target verification tool to obtain a verification result of the bus to be verified. In this way, the sub-files to be verified of the bus to be verified are analyzed into the identifiable files identifiable by the target verification tool, and the bus to be verified can be verified through the target verification tool, so that an automatic bus verification process can be realized through automatic analysis modeling and verification, manual intervention is reduced, and verification efficiency is improved.

Description

Bus verification method, device, electronic equipment and readable storage medium
Technical Field
The present invention relates to the field of computer technologies, and in particular, to a bus verification method, a bus verification device, an electronic device, and a readable storage medium.
Background
With the development of computer technology, the system structure of the integrated chip is more and more complex, including various components such as processor clusters, graphics processors, memory controllers, I/O bridges, PCIe subsystems, etc., and in order to implement shared memory access and cache coherency for each component, an on-chip interconnection bus is generally adopted for implementation, so the performance of the integrated chip is closely related to the bus.
In order to ensure the performance of the integrated chip, the bus adopted by the chip needs to be verified, so how to verify the on-chip interconnection bus becomes a problem to be solved.
Disclosure of Invention
An embodiment of the invention aims to provide a bus verification method, a bus verification device, electronic equipment and a readable storage medium, so as to solve the problem of how to verify a bus. The specific technical scheme is as follows:
In a first aspect of the present invention, there is provided a bus validation method, the method comprising:
obtaining a sub-file to be verified of a bus to be verified;
Mapping characters contained in the subfiles to be verified into binary elements based on a preset mapping rule;
generating an abstract syntax tree based on the binary element, and generating an identifiable file identifiable by a target verification tool based on the abstract syntax tree;
and inputting the identifiable file into the target verification tool to acquire a verification result of the bus to be verified.
In a second aspect of the present invention, there is also provided a bus validation apparatus, the apparatus comprising:
the first acquisition module is used for acquiring a sub-file to be verified of the bus to be verified;
the mapping module is used for mapping the characters contained in the subfiles to be verified into binary elements based on a preset mapping rule;
the generation module is used for generating an abstract syntax tree based on the binary element and generating an identifiable file identifiable by a target verification tool based on the abstract syntax tree;
and the input module is used for inputting the identifiable file into the target verification tool so as to acquire a verification result of the bus to be verified.
In a third aspect of the present invention, there is also provided an electronic device, including a processor, a communication interface, a memory, and a communication bus, where the processor, the communication interface, and the memory complete communication with each other through the communication bus;
a memory for storing a computer program;
and a processor, configured to implement the method according to the first aspect when executing the program stored in the memory.
In a fourth aspect of the invention, there is also provided a computer readable storage medium having instructions stored therein which, when run on a computer, cause the computer to perform the method of the first aspect described above.
In a fifth aspect of the invention there is also provided a computer program product containing instructions which, when run on a computer, cause the computer to perform the method of the first aspect described above.
The bus verification method provided by the embodiment of the invention comprises the steps of obtaining a sub-file to be verified of a bus to be verified, analyzing characters contained in the sub-file to be verified to convert the sub-file to be verified into an identifiable file identifiable by a target verification tool, and inputting the identifiable file into the target verification tool to obtain a verification result of the bus to be verified. In this way, the sub-files to be verified of the bus to be verified are analyzed into the identifiable files identifiable by the target verification tool, and the bus to be verified can be verified through the target verification tool, so that an automatic bus verification process can be realized through automatic analysis modeling and verification, manual intervention is reduced, and verification efficiency is improved.
Drawings
In order to more clearly illustrate the embodiments of the present invention or the technical solutions in the prior art, the drawings used in the description of the embodiments or the prior art will be briefly described below.
FIG. 1 is a flow chart illustrating steps of a bus verification method according to an embodiment of the present invention;
FIG. 2 is a flow chart of a bus verification method according to an embodiment of the invention;
FIG. 3 is a schematic diagram of a bus verification device according to an embodiment of the present invention;
fig. 4 is a schematic diagram of an electronic device according to an embodiment of the present invention.
Detailed Description
The following description of the embodiments of the present invention will be made clearly and fully with reference to the accompanying drawings, in which it is evident that the embodiments described are some, but not all embodiments of the invention. All other embodiments, which can be made by those skilled in the art based on the embodiments of the invention without making any inventive effort, are intended to be within the scope of the invention.
The terms first, second and the like in the description and in the claims, are used for distinguishing between similar elements and not necessarily for describing a particular sequential or chronological order. It is to be understood that the data so used may be interchanged, as appropriate, such that embodiments of the present invention may be implemented in sequences other than those illustrated or described herein, and that the objects identified by "first," "second," etc. are generally of a type, and are not limited to the number of objects, such as the first object may be one or more. Furthermore, the term "and/or" in the specification and claims is used to describe an association relationship of an association object, and means that there may be three relationships, for example, a and/or B, and that there may be three cases where a exists alone, while a and B exist together, and B exists alone. The character "/" generally indicates that the context-dependent object is an "or" relationship. The term "plurality" in embodiments of the present invention means two or more, and other adjectives are similar.
Fig. 1 is a flowchart of a bus verification method according to an embodiment of the present invention, as shown in fig. 1, where the method includes:
step 101, obtaining a sub-file to be verified of a bus to be verified.
Step 102, mapping the characters contained in the subfiles to be verified into binary elements based on a preset mapping rule.
Step 103, generating an abstract syntax tree based on the binary elements, and generating an identifiable file identifiable by a target verification tool based on the abstract syntax tree.
Step 104, inputting the identifiable file into the target verification tool to obtain a verification result of the bus to be verified.
For the steps 101 to 104, the bus to be verified in the embodiment of the present invention may be a bus with verification requirements, and may be a coherence bus interface (Coherent Hub Interface, CHI), where the CHI protocol is a protocol for constructing a high-performance, low-power multiprocessor system. It provides an efficient, low latency method to connect multiple processors, accelerators, memory, and other system components to achieve shared memory access and cache coherency. The bus to be verified can also be MSI, MOESI and other buses, and can be set according to verification requirements, and the embodiment of the invention is not limited to this.
It should be noted that, because the bus is often complex, and includes protocol contents in multiple aspects, only a part of the protocol contents are often needed to be used by a part of the integrated chip, so that verification of the whole content of the bus is not needed. Based on the above, the embodiment of the invention can acquire the subfiles to be verified of the bus to be verified based on the actual scene and the verification requirement. The subfiles to be verified refer to a subset corresponding to a part of functions to be verified in the bus to be verified, and in one case, for a high-performance computing system including a plurality of processor cores, a graphics processor, a memory controller and an I/O bridge, the subfiles to be verified are connected to each other through a CHI bus. In this system, cache consistency is a key for ensuring data consistency and system performance, and the subfiles to be verified may be a subset (CC-Gen architecture model) for implementing cache consistency in the CHI bus, so that the embodiment of the present invention may verify cache consistency of the CHI bus.
Specifically, the bus to be verified can be determined by receiving input information of related personnel, and a sub-file to be verified of the bus to be verified is obtained. The subfiles to be verified can be expressed in a specific domain language, and in the case that the subfiles to be verified are cache consistency subsets, the subfiles to be verified can be expressed in a cache consistency specific domain language, for example, a native language (ProtoGen Language for IMPLEMENTING CACHE Coherence, PCC) for realizing cache consistency or a standard language (Specification Language for IMPLEMENTING CACHE Coherence, SLICC) for realizing cache consistency, and the subfiles to be verified can be understood as a requirement model of the bus to be verified, and the cache consistency function of the bus to be verified can be verified by verifying the requirement model. Specifically, the sub-file to be verified is expressed in a language form in a specific field, so that the sub-file to be verified can be ensured to have verifiability and universality.
The target verification tool refers to an automatic verification tool, and can be an integrated tool environment (Uppaal) for verifying a real-time system, or a Mur phi tool, which can be selected according to actual requirements, and the embodiment of the invention is not limited to this. Specifically, test cases can be quickly generated and executed in the automatic test tool, so that time can be greatly saved, and errors caused by human factors can be reduced to a certain extent. Meanwhile, the automation of the verification process can be realized through the target verification tool, and the automation of the verification process relates to the control and execution of the verification process, including the scheduling, execution, result collection, report output and the like of test cases. By automating the generation and execution of test cases and integrating the continuous integration tool, the efficiency and accuracy of the test can be greatly improved.
Specifically, because different file formats which can be identified by different verification tools may be different, the embodiment of the invention can convert the sub-file to be verified into the identifiable file which can be identified by the target verification tool, so that the identifiable file can be input into the target verification tool for verification, and a verification result of the bus to be verified is obtained. Illustratively, when the target verification tool is Uppaal tools, the identifiable file may be in an extensible markup language (Extensible Markup Language, XML) format, thereby facilitating verification of the bus to be verified by the target verification tool.
Specifically, the source code in the sub-file to be verified is composed of a large number of characters, the character contained in the sub-file to be verified can be analyzed, and the sub-file to be verified is converted into the identifiable file based on the analyzed character meaning. Specifically, the embodiment of the invention can pre-construct the mapping relation based on the format of the sub-file to be verified and the format recognizable by the target verification tool, so that the characters contained in the sub-file to be verified can be mapped into the format recognizable by the target verification tool. Optionally, the embodiment of the invention can pre-construct a lexical analyzer (Lexer) and a Parser (Parser) to parse the sub-files to be verified.
The preset mapping rule may be preset based on the format of the subfile to be verified. Specifically, the characters can be read from the subfiles to be verified one by one to form a character stream. Meanwhile, various binary elements (Token) in the character stream, such as keywords, identifiers, constants, operators, and the like, can be identified by defining a series of rules such as regular expressions. After the identification and classification marks are completed, a Token stream (binary file) is generated, which is an abstract representation of the source code.
Alternatively, the embodiment of the present invention may predefine binary elements to be identified, for example:
Keywords such as if, else, return, which are words predefined by the programming language and having special meaning.
Identifiers, such as variable names and function names, are typically composed of letters, numbers, and underlines.
Constants such as numerical constants, string constants, etc.
Operators such as "+", "-", "/", etc.
Delimiters such as comma ", semicolon", bracket "()", and the like.
Network txreq \ rxreq \ txrsp \ rxrsp \ txdat \ rxdat, etc., and Channel such as req, rsp, snp, dat, etc.
Alternatively, if a sequence of characters that cannot be matched is encountered during the recognition process, an error, such as a grammar error or an illegal character, may be reported.
Wherein the abstract syntax tree (Abstract Syntax Tree, AST) is an abstract representation of the source code syntax structure, which is a tree-like structure, wherein each node represents a syntax structure in the source code, such as an expression, a statement, etc. Furthermore, the embodiment of the invention can generate the abstract syntax tree based on the binary element, thereby facilitating the subsequent further analysis.
In summary, the bus verification method provided by the embodiment of the invention includes the steps of obtaining a sub-file to be verified of a bus to be verified, analyzing characters contained in the sub-file to be verified to convert the sub-file to be verified into an identifiable file identifiable by a target verification tool, and inputting the identifiable file into the target verification tool to obtain a verification result of the bus to be verified. In this way, the sub-files to be verified of the bus to be verified are analyzed into the identifiable files identifiable by the target verification tool, and the bus to be verified can be verified through the target verification tool, so that an automatic bus verification process can be realized through automatic analysis modeling and verification, manual intervention is reduced, and verification efficiency is improved.
Optionally, the above operation of generating the identifiable file identifiable by the target verification tool based on the abstract syntax tree may specifically include:
S21, converting the abstract syntax tree into an executable code file according to node information of each node contained in the abstract syntax tree.
S24, generating an identifiable file identifiable by the target verification tool based on the executable code file.
Specifically, the abstract syntax tree comprises a plurality of nodes, each node represents one syntax structure in the source code, and on the basis, the embodiment of the invention can convert the abstract syntax tree into an executable code file (.m file) according to the node information of each node of the abstract syntax tree.
Further, embodiments of the present invention may generate an identifiable file identifiable by the target verification tool based on the executable code file.
In the embodiment of the invention, the characters contained in the subfiles to be verified are mapped into binary elements based on the preset mapping rules. An abstract syntax tree is generated based on the binary elements. And converting the abstract syntax tree into an executable code file according to node information of each node contained in the abstract syntax tree. Based on the executable code file, an identifiable file identifiable by a target verification tool is generated. In this way, the sub-file to be verified can be converted into the identifiable file, and the accuracy and verifiability of the identifiable file are ensured.
Optionally, the above operation of generating the identifiable file identifiable by the target verification tool based on the executable code file may specifically include:
s31, obtaining a constraint file containing the attribute to be verified.
S32, generating an identifiable file identifiable by the target verification tool based on the constraint file and the executable code file.
The attribute to be verified refers to a constraint rule to be verified, and can be set according to a cache policy implemented by the bus to be verified, for example, deadlock freedom, cache consistency or fairness, etc., which can be obtained based on input information of related personnel, or can be obtained by pre-programming, and can be set according to actual verification requirements, which is not limited by the embodiment of the invention.
Specifically, the constraint file may be written in a specific language of CC-Gen or UPPAAL, where variables such as a cache state and a message type may be defined, and cache policy logic such as a state conversion rule and a condition of sending and receiving a message may be expressed, and further, the constraint file may further include a purpose required for verification, for example, the system may always reach a consistency state.
Further, the constraint file and the executable code file may be integrated, and both may be converted into XML files and input into a pre-written integrator. The integrator may be an integration code written in advance in a high-level programming language (e.g., crawler, python) and used for converting an XML file into a formalized model that can be understood and processed by the CC-Gen to obtain an identifiable file, where the identifiable file includes all states, conversions, synchronization mechanisms, and attributes to be verified.
In this way, in the embodiment of the invention, the constraint file containing the attribute to be verified is obtained. Based on the constraint file and the executable code file, an identifiable file identifiable by a target verification tool is generated. Therefore, constraint rules can be added into the identifiable file according to the actual constraint file, flexibility of bus verification is improved, a complex system behavior model can be abstracted, unnecessary details are removed, and key verification points are highlighted.
Optionally, the above operation of generating the abstract syntax tree based on the binary element may specifically include:
s41, creating a root node.
S42, creating corresponding tree nodes according to the binary elements.
S43, generating an abstract syntax tree based on the root node and each tree node.
The root node refers to a parent node of the abstract syntax tree, which is a parent node of all other nodes. Specifically, the root node and the tree node may be created by a node creation function.
Further, the embodiment of the invention can construct a Parser, and the Parser receives Lexer generated Token streams. These Token are keywords, identifiers, constants, operators, etc. in the source code.
Parser uses recursive descent parsing or similar algorithms to process Token streams. Each function corresponds to a non-terminal in the grammar rules. Parser identifies grammar rules by matching Token and creates corresponding AST nodes (tree nodes). AST is constructed recursively. Each syntax structure is added to the tree to form a hierarchical relationship. For example, a function declaration may have an identifier (function name) and a list of parameters, which are added as child nodes under the function declaration node.
Specifically, the embodiment of the invention can determine basic elements of the AST, such as cache lines, processors, channels, directories and the like, based on the subfiles to be verified. And describes the operation and status of these elements, such as read, write, invalidate, etc. of the cache line. Rules are constructed to define interaction rules between elements, and how write operations affect the cache state of other processors is described by way of state machine descriptions. Generating an AST-converting these rules and operations to an AST using a Parser, each node in an AST representing a particular operation or state in the model.
Thus, in the embodiment of the invention, the root node is created. And creating corresponding tree nodes according to each binary element. An abstract syntax tree is generated based on the root node and each of the tree nodes. Through the operation, the consistency structure AST for expressing the subfiles to be verified can be generated, and the expandability is improved.
Optionally, the operation of converting the abstract syntax tree into the executable code file according to the node information of each node included in the abstract syntax tree may specifically include:
S51, acquiring a concurrency structure, a synchronization structure and a communication structure in the abstract syntax tree according to node information of each node contained in the abstract syntax tree.
And S52, mapping the concurrency structure, the synchronization structure and the communication structure into executable structures respectively.
S52, generating an executable code file based on the executable structure.
Specifically, an Abstract Syntax Tree (AST) may be traversed, with each node in the AST accessed one pass in a particular order (e.g., preface, midrange, successor). This process can result in a structured representation of the source code and can extract key information, providing a basis for subsequent processing. And traversing the abstract syntax tree AST to extract key information of each relation or expression statement in the PCC statement, matching corresponding templates for each relation or expression statement according to the content of the key information to generate concurrency transients, and storing the concurrency transients as an m file to obtain an executable code file. The template may be information input in advance by a relevant person, and may include static protocol jump information, so that a corresponding concurrency transient is set for each relationship or expression statement based on the static protocol jump information.
When traversing an AST, each node is accessed, and the type and attribute of the node are checked. Specific processing logic is executed according to the node type, such as extracting variable names, function calls, control flow statements, etc. The children of the node are recursively traversed, extracting key information, which may include variable declarations, function definitions, control flow statements, expressions, and the like.
In particular, the concurrency structure in the AST may be mapped to a process template of the target verification tool UPPAAL. The synchronization and communication operations are mapped to the channels and synchronization mechanisms of the target verification tool UPPAAL and define system parameters and variables such as buffer status, message type, etc. And further uses the specific language and grammar rules of UPPAAL-CCGen to describe the behavior and attributes of the model.
In the embodiment of the invention, the concurrency structure, the synchronization structure and the communication structure in the abstract syntax tree are obtained according to the node information of each node contained in the abstract syntax tree. And mapping the concurrency structure, the synchronization structure and the communication structure into executable structures respectively. An executable code file is generated based on the executable structure. In this way, an accurate executable code file can be obtained, which is convenient to be subsequently converted into an identifiable file of the target verification tool.
Optionally, the embodiment of the invention specifically may include:
S61, traversing the abstract syntax tree to obtain the node type of each node.
S62, aiming at any node, acquiring node information of the node based on the node type of the node.
Specifically, when traversing an AST, the node type is identified, and corresponding information is extracted according to the type. For each node, its child nodes are examined and information, such as variable declarations, function definitions, control flow statements, expressions, etc., is recursively extracted. While traversing an AST, concurrent computation model (PCC) statements describing concurrent behavior, such as concurrent regions, synchronization operations, etc., may be identified and extracted.
Specifically, the embodiment of the present invention may traverse an AST using Depth-First-Search (DFS) to access each node. For each node it is checked whether it represents a concurrent structure or a synchronous operation. Key attributes of the node are extracted, such as operation type, related variables, channels and the like.
Thus, the node information of each node can be acquired through the nodes of AST so as to avoid omission and ensure the integrity of information acquisition.
Optionally, the bus to be verified is CHI bus, and the target verification tool is UPPAAL.
Alternatively, a verification tool such as a model checker may be used as the target verification tool, but UPPAAL has a certain advantage in terms of real-time system verification.
Further, the UPPAAL can be used for formal verification of the generated identifiable file, so that the cache consistency requirement of the CHI bus is ensured to be met. The verification result output by the UPPAAL can be obtained, and the verification result comprises a verification report about the consistency requirement of the CHI bus cache, including indexes such as correctness and functional completeness of a consistency protocol.
Fig. 2 is a flow chart of a bus verification method according to an embodiment of the present invention, as shown in fig. 2, in which a converter is configured to convert an abstract syntax tree into an executable code file (.m. file), where the converter may include a protocol layer, a network layer, and a link layer. Wherein the editor is used for identifying statement information in the AST. The protocol generator refers to a code model for constructing a property constraint file, and can integrate an executable code file generated by the converter with the property constraint file to obtain an identifiable XML file. The XML file can be input into UPPAAL, and UPPAAL can analyze and verify the XML file through the model solver and the formal verification engine, and output a verification report.
By using domain specific language and UPPAAL, the application of the formalization method is enhanced, and by formalization model and UPPAAL verification, the consistency of the CHI bus is ensured. By constructing a complete automatic verification process, the systematic degree of verification is improved. By the formal verification method, potential design errors and consistency problems can be found in the system design stage, so that the reliability of the system is improved. The automated verification process reduces the need for manual testing, thereby reducing development costs and human resource consumption.
Alternatively, some related art bus validation is performed by manual testing or other formalized methods, which increases the validation coverage by adding testers and test cases, but this increases cost and time. Other formalized methods, such as using a certification assistant (Coq or Isabelle, etc.) to verify system properties, typically require higher expertise and longer development times. If simulation is employed, advanced simulation tools are used to simulate the behavior of the CHI bus, but this may not fully capture all concurrent and real-time behavior.
Alternatively, as the scale of the system increases, the complexity of the model may increase, more efficient algorithms and tools may be required to handle large-scale models, and as the complexity of the model increases, maintaining the readability and maintainability of the model is a challenge, more advanced modeling tools and methods may need to be developed. The embodiment of the invention can further utilize a parallel computing technology to accelerate the verification process of the model by adopting target verification tools such as UPPAAL and the like. The model construction and verification can be assisted by an artificial intelligence assistance method and a machine learning method, so that the automation level is improved. Thereby facilitating handling of larger scale systems. The readability and maintainability of the model are improved.
The method of the invention supports the expandability of the CHI bus, so that the high-efficiency verification flow can be maintained when the system scale is enlarged. The establishment of the formalized model provides convenience for subsequent maintenance and upgrading of the system, so that modification and optimization of the system are easier and more accurate. Because of the improvement of verification efficiency, the system verification can be completed more quickly, and the period from design to marketing of the product is shortened.
Fig. 3 is a schematic structural diagram of a bus verification device according to an embodiment of the present invention, and as shown in fig. 3, the device 20 may include:
a first obtaining module 201, configured to obtain a subfile to be verified of a bus to be verified;
the mapping module 202 is configured to map the characters contained in the subfiles to be verified into binary elements based on a preset mapping rule;
a generating module 203, configured to generate an abstract syntax tree based on the binary element, and generate an identifiable file identifiable by a target verification tool based on the abstract syntax tree;
and the input module 204 is configured to input the identifiable file into the target verification tool to obtain a verification result of the bus to be verified.
Optionally, the generating module 203 includes:
the conversion sub-module is used for converting the abstract syntax tree into an executable code file according to the node information of each node contained in the abstract syntax tree;
and the first generation sub-module is used for generating an identifiable file identifiable by the target verification tool based on the executable code file.
Optionally, the first generating sub-module is specifically configured to:
Acquiring a constraint file containing attributes to be verified;
Based on the constraint file and the executable code file, an identifiable file identifiable by a target verification tool is generated.
Optionally, the generating module further includes:
The first creation sub-module is used for creating a root node;
a second creating sub-module, configured to create a corresponding tree node according to each binary element;
and the tree generation sub-module is used for generating an abstract syntax tree based on the root node and each tree node.
Optionally, the conversion sub-module is specifically configured to:
Acquiring a concurrency structure, a synchronization structure and a communication structure in the abstract syntax tree according to node information of each node contained in the abstract syntax tree;
Mapping the concurrency structure, the synchronization structure, and the communication structure to executable structures based on templates of the target verification tool, respectively;
an executable code file is generated based on the executable structure.
Optionally, the apparatus further comprises:
the traversing module is used for traversing the abstract syntax tree to obtain the node type of each node;
The acquisition module is used for acquiring the node information of any node based on the node type of the node.
Optionally, the bus to be verified is CHI bus, and the target verification tool is UPPAAL.
In summary, the bus verification device provided by the embodiment of the invention obtains the sub-file to be verified of the bus to be verified, analyzes the characters contained in the sub-file to be verified to convert the sub-file to be verified into the identifiable file identifiable by the target verification tool, and inputs the identifiable file into the target verification tool to obtain the verification result of the bus to be verified. In this way, the sub-files to be verified of the bus to be verified are analyzed into the identifiable files identifiable by the target verification tool, and the bus to be verified can be verified through the target verification tool, so that an automatic bus verification process can be realized through automatic analysis modeling and verification, manual intervention is reduced, and verification efficiency is improved.
For the device embodiments, since they are substantially similar to the method embodiments, the description is relatively simple, and reference is made to the description of the method embodiments for relevant points.
In this specification, each embodiment is described in a progressive manner, and each embodiment is mainly described by differences from other embodiments, and identical and similar parts between the embodiments are all enough to be referred to each other.
The specific manner in which the respective modules perform the operations in the bus verification apparatus in the above-described embodiment has been described in detail in the embodiment concerning the method, and will not be described in detail here.
The embodiment of the invention also provides electronic equipment, which comprises a processor and a memory for storing instructions executable by the processor, wherein the processor is configured to execute the bus verification method.
Referring to fig. 4, a schematic structural diagram of an electronic device according to an embodiment of the present invention is shown. As shown in fig. 4, the electronic device includes a processor, a memory, a communication interface, and a communication bus, where the processor, the memory, and the communication interface complete communication with each other through the communication bus, and the memory is configured to store at least one executable instruction, where the executable instruction causes the processor to execute the bus verification method of the foregoing embodiment.
It should be noted that, the electronic device in the embodiment of the present application includes a mobile electronic device and a non-mobile electronic device.
The Processor may be a CPU (Central Processing Unit ), general purpose Processor, DSP (DIGITAL SIGNAL Processor ), ASIC (Application SPECIFIC INTEGRATED Circuit), FPGA (Field Programmble GATE ARRAY, field programmable gate array) or other editable device, transistor logic device, hardware component, or any combination thereof. The processor may also be a combination that performs the function of a computation, e.g., a combination comprising one or more microprocessors, a combination of a DSP and a microprocessor, etc.
The communication bus may include a path to transfer information between the memory and the communication interface. The communication bus may be a PCI (PERIPHERAL COMPONENT INTERCONNECT, peripheral component interconnect standard) bus or an EISA (Extended Industry Standard Architecture ) bus, or the like. The communication bus may be classified into an address bus, a data bus, a control bus, and the like. For ease of illustration, only one line is shown in fig. 3, but not only one bus or one type of bus.
The memory may be a ROM (Read Only memory) or other type of static storage device that can store static information and instructions, a RAM (Random Access memory) or other type of dynamic storage device that can store information and instructions, an EEPROM (ELECTRICALLY ERASABLE PROGRAMMABLE READ ONLY, electrically erasable programmable Read Only memory), a CD-ROM (Compact Disa Read Only, compact disc Read Only), a magnetic tape, a floppy disk, an optical data storage device, and the like.
Embodiments of the present invention also provide a non-transitory computer-readable storage medium that, when executed by a processor of an electronic device (server or terminal), enables the processor to perform the bus validation method shown in fig. 1.
Embodiments of the present invention also provide a computer program product containing instructions that, when run on a computer, cause the computer to perform the bus validation method shown in fig. 1.
The embodiment of the application also provides a chip, which comprises a processor and a communication interface, wherein the communication interface is coupled with the processor, and the processor is used for running programs or instructions to realize the processes of the embodiment of the bus verification method, and can achieve the same technical effects, so that repetition is avoided, and the description is omitted here.
It should be understood that the chips referred to in the embodiments of the present application may also be referred to as system-on-chip chips, chip systems, or system-on-chip chips, etc.
In this specification, each embodiment is described in a progressive manner, and each embodiment is mainly described by differences from other embodiments, and identical and similar parts between the embodiments are all enough to be referred to each other.
It will be apparent to those skilled in the art that embodiments of the present invention may be provided as a method, apparatus, or computer program product. Accordingly, embodiments of the present invention may be implemented, in whole or in part, in software, hardware, firmware, or any combination thereof. When implemented in software, may be implemented in whole or in part in the form of a computer program product. The computer program product includes one or more computer instructions. When loaded and executed on a computer, produces a flow or function in accordance with embodiments of the present invention, in whole or in part. The computer may be a general purpose computer, a special purpose computer, a computer network, or other programmable apparatus. The computer instructions may be stored in or transmitted from one computer-readable storage medium to another, for example, by wired (e.g., coaxial cable, optical fiber, digital Subscriber Line (DSL)), or wireless (e.g., infrared, wireless, microwave, etc.). The computer readable storage medium may be any available medium that can be accessed by a computer or a data storage device such as a server, data center, etc. that contains an integration of one or more available media. The usable medium may be a magnetic medium (e.g., floppy disk, hard disk, tape), an optical medium (e.g., DVD), or a semiconductor medium (e.g., solid state disk Solid STATE DISK (SSD)), etc.
Embodiments of the present invention are described with reference to flowchart illustrations and/or block diagrams of methods, terminal devices (systems), and computer program products according to embodiments of the invention. It will be understood that each flow and/or block of the flowchart illustrations and/or block diagrams, and combinations of flows and/or blocks in the flowchart illustrations and/or block diagrams, can be implemented by computer program instructions. These computer program instructions may be provided to a processor of a general purpose computer, special purpose computer, embedded processor, or other programmable data processing terminal device to produce a machine, such that the instructions, which execute via the processor of the computer or other programmable data processing terminal device, create means for implementing the functions specified in the flowchart flow or flows and/or block diagram block or blocks.
These computer program instructions may also be stored in a computer-readable memory that can direct a computer or other programmable data processing apparatus to function in a particular manner, such that the instructions stored in the computer-readable memory produce an article of manufacture including instruction means which implement the function specified in the flowchart flow or flows and/or block diagram block or blocks.
These computer program instructions may also be loaded onto a computer or other programmable data processing apparatus to cause a series of operational steps to be performed on the computer or other programmable apparatus to produce a computer implemented process such that the instructions which execute on the computer or other programmable apparatus provide steps for implementing the functions specified in the flowchart flow or flows and/or block diagram block or blocks.
While preferred embodiments of the present invention have been described, additional variations and modifications in those embodiments may occur to those skilled in the art once they learn of the basic inventive concepts. It is therefore intended that the following claims be interpreted as including the preferred embodiment and all such alterations and modifications as fall within the scope of the embodiments of the invention.
In this specification, each embodiment is described in a related manner, and identical and similar parts of each embodiment are all referred to each other, and each embodiment mainly describes differences from other embodiments. In particular, for system embodiments, since they are substantially similar to method embodiments, the description is relatively simple, as relevant to see a section of the description of method embodiments.
It should be noted that, in the embodiment of the present application, the related processes of obtaining various data are all performed under the premise of conforming to the corresponding data protection rule policy of the country of the location and obtaining the authorization given by the owner of the corresponding device.
Finally, it is further noted that relational terms such as first and second, and the like are used solely to distinguish one entity or action from another entity or action without necessarily requiring or implying any actual such relationship or order between such entities or actions. Moreover, the terms "comprises," "comprising," or any other variation thereof, are intended to cover a non-exclusive inclusion, such that a process, method, article, or terminal that comprises a list of elements does not include only those elements but may include other elements not expressly listed or inherent to such process, method, article, or terminal. Without further limitation, an element defined by the phrase "comprising one does not exclude the presence of other like elements in a process, method, article or terminal device comprising the element.
The foregoing describes the principles and embodiments of the present invention in detail using specific examples to facilitate understanding of the method and core ideas thereof, and the present invention is not to be construed as limited to the specific embodiments and the application scope of the invention as long as the method, the apparatus, the electronic device and the readable storage medium are modified by those skilled in the art according to the ideas of the present invention.

Claims (10)

1. A bus validation method, the method comprising:
obtaining a sub-file to be verified of a bus to be verified;
Mapping characters contained in the subfiles to be verified into binary elements based on a preset mapping rule;
generating an abstract syntax tree based on the binary element, and generating an identifiable file identifiable by a target verification tool based on the abstract syntax tree;
and inputting the identifiable file into the target verification tool to acquire a verification result of the bus to be verified.
2. The method of claim 1, wherein generating an identifiable file identifiable by a target verification tool based on the abstract syntax tree comprises:
converting the abstract syntax tree into an executable code file according to node information of each node contained in the abstract syntax tree;
based on the executable code file, an identifiable file identifiable by a target verification tool is generated.
3. The method of claim 2, wherein the generating an identifiable file identifiable by a target verification tool based on the executable code file comprises:
Acquiring a constraint file containing attributes to be verified;
Based on the constraint file and the executable code file, an identifiable file identifiable by a target verification tool is generated.
4. The method of claim 1, wherein the generating an abstract syntax tree based on the binary elements comprises:
Creating a root node;
Creating corresponding tree nodes according to the binary elements;
an abstract syntax tree is generated based on the root node and each of the tree nodes.
5. The method according to claim 2, wherein the converting the abstract syntax tree into an executable code file according to node information of each node included in the abstract syntax tree comprises:
Acquiring a concurrency structure, a synchronization structure and a communication structure in the abstract syntax tree according to node information of each node contained in the abstract syntax tree;
mapping the concurrency structure, the synchronization structure and the communication structure into executable structures respectively;
an executable code file is generated based on the executable structure.
6. The method according to claim 2, wherein the method further comprises:
Traversing the abstract syntax tree to obtain node types of all nodes;
and aiming at any node, acquiring node information of the node based on the node type of the node.
7. The method of any of claims 1-6, wherein the bus to be authenticated is a CHI bus and the target authentication tool is UPPAAL.
8. A bus validation apparatus, the apparatus comprising:
the first acquisition module is used for acquiring a sub-file to be verified of the bus to be verified;
the mapping module is used for mapping the characters contained in the subfiles to be verified into binary elements based on a preset mapping rule;
the generation module is used for generating an abstract syntax tree based on the binary element and generating an identifiable file identifiable by a target verification tool based on the abstract syntax tree;
and the input module is used for inputting the identifiable file into the target verification tool so as to acquire a verification result of the bus to be verified.
9. The electronic equipment is characterized by comprising a processor, a communication interface, a memory and a communication bus, wherein the processor, the communication interface and the memory are communicated with each other through the communication bus;
a memory for storing a computer program;
a processor for implementing the method of any of claims 1-7 when executing a program stored on a memory.
10. A computer readable storage medium, on which a computer program is stored, characterized in that the program, when being executed by a processor, implements the method according to any of claims 1-7.
CN202411997230.XA 2024-12-31 Bus verification method, device, electronic device and readable storage medium Active CN119397969B (en)

Priority Applications (1)

Application Number Priority Date Filing Date Title
CN202411997230.XA CN119397969B (en) 2024-12-31 Bus verification method, device, electronic device and readable storage medium

Applications Claiming Priority (1)

Application Number Priority Date Filing Date Title
CN202411997230.XA CN119397969B (en) 2024-12-31 Bus verification method, device, electronic device and readable storage medium

Publications (2)

Publication Number Publication Date
CN119397969A true CN119397969A (en) 2025-02-07
CN119397969B CN119397969B (en) 2025-04-18

Family

ID=

Citations (9)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
CN101017458A (en) * 2007-03-02 2007-08-15 北京邮电大学 Software safety code analyzer based on static analysis of source code and testing method therefor
CN103140838A (en) * 2010-10-27 2013-06-05 株式会社日立制作所 Method of converting source code and source code conversion program
CN108376221A (en) * 2018-02-27 2018-08-07 哈尔滨工业大学 A software system security verification and evaluation method based on AADL model extension
CN109976712A (en) * 2019-03-12 2019-07-05 中山大学 One kind doing formalization verification method to network physical system requirements based on UPPAAL-SMC
CN112416337A (en) * 2020-11-11 2021-02-26 北京京航计算通讯研究所 Software architecture development system for aerospace embedded system
CN112506489A (en) * 2020-11-30 2021-03-16 广州市智能软件产业研究院 Cross-platform method, computer and storage medium for security protocol modeling end and verification end
CN113726821A (en) * 2021-11-02 2021-11-30 华东交通大学 Verification method and system for security protocol formalization
US20230252161A1 (en) * 2020-02-10 2023-08-10 Telefonaktiebolaget Lm Ericsson (Publ) Methods of evaluating source code using numeric array representations of source code elements
CN118277253A (en) * 2024-03-25 2024-07-02 中国工商银行股份有限公司 Program verification method, program verification device, program verification equipment, program verification medium and program verification product

Patent Citations (10)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
CN101017458A (en) * 2007-03-02 2007-08-15 北京邮电大学 Software safety code analyzer based on static analysis of source code and testing method therefor
CN103140838A (en) * 2010-10-27 2013-06-05 株式会社日立制作所 Method of converting source code and source code conversion program
US20130263092A1 (en) * 2010-10-27 2013-10-03 Hitachi,Ltd. Method of converting source code and source code conversion program
CN108376221A (en) * 2018-02-27 2018-08-07 哈尔滨工业大学 A software system security verification and evaluation method based on AADL model extension
CN109976712A (en) * 2019-03-12 2019-07-05 中山大学 One kind doing formalization verification method to network physical system requirements based on UPPAAL-SMC
US20230252161A1 (en) * 2020-02-10 2023-08-10 Telefonaktiebolaget Lm Ericsson (Publ) Methods of evaluating source code using numeric array representations of source code elements
CN112416337A (en) * 2020-11-11 2021-02-26 北京京航计算通讯研究所 Software architecture development system for aerospace embedded system
CN112506489A (en) * 2020-11-30 2021-03-16 广州市智能软件产业研究院 Cross-platform method, computer and storage medium for security protocol modeling end and verification end
CN113726821A (en) * 2021-11-02 2021-11-30 华东交通大学 Verification method and system for security protocol formalization
CN118277253A (en) * 2024-03-25 2024-07-02 中国工商银行股份有限公司 Program verification method, program verification device, program verification equipment, program verification medium and program verification product

Non-Patent Citations (1)

* Cited by examiner, † Cited by third party
Title
常天佑;魏强;耿洋洋;: "基于状态转换的PLC程序模型构建方法", 计算机应用, no. 12, 10 December 2017 (2017-12-10), pages 3574 - 3580 *

Similar Documents

Publication Publication Date Title
JP2022062060A (en) Tools and methods for real-time dataflow programming languages
US20130125098A1 (en) Transformation of Computer Programs
CN106294148B (en) C programmer software verification method and device based on escape character transition system
CN106951305A (en) It is a kind of based on method of the model conversion by QVT R language generation midCore scripts
Chen et al. Hopper: Interpretative fuzzing for libraries
Lukács et al. Formal modeling and verification of the functionality of electronic urban railway control systems through a case study
Mross et al. Transformation of GRAFCET into GAL for verification purposes based on a detailed meta-model
US11593076B2 (en) Method for merging architecture data
CN119397969B (en) Bus verification method, device, electronic device and readable storage medium
CN118503110A (en) A method for identifying and repairing source code defects
CN119397969A (en) Bus verification method, device, electronic equipment and readable storage medium
CN114281314B (en) Method, system and medium for converting JPSL to PPTL property specification
CN115408289A (en) A Method of Automatically Generating Test Cases Oriented to SCADE Model
Jiang et al. Safety-assured formal model-driven design of the multifunction vehicle bus controller
US11650802B2 (en) Idiomatic source code generation
CN115904480A (en) Code reconstruction method and device, electronic equipment and storage medium
Zhang An Approach for Extracting UML Diagram from Object-Oriented Program Based on J2X
Germino et al. An XSLT-based proposal to ease embedded critical systems tools implementation, verification, validation, testing, and certification efforts
CN114817124A (en) Inter-multi-core microcontroller mapping method, device and computer-readable storage medium
Ballenghien et al. Event-B as DSL in Isabelle and HOL Experiences from a Prototype
Yue et al. Trap: trace runtime analysis of properties
Lin et al. OntCheck: An Ontology‐Driven Static Correctness Checking Tool for Component‐Based Models
CN118940720A (en) A programming language conversion method, device, equipment and storage medium
CN118733050A (en) A2L file processing method, electronic device and storage medium
CN119046127A (en) Method, device, equipment and storage medium for formal verification based on SCADE model

Legal Events

Date Code Title Description
PB01 Publication
PB01 Publication
SE01 Entry into force of request for substantive examination
SE01 Entry into force of request for substantive examination
GR01 Patent grant