Shulou(Shulou.com)06/01 Report--

Today, I will talk to you about how to operate Keypoint mapping, many people may not know much about it. In order to make you understand better, the editor has summarized the following content for you. I hope you can get something according to this article.

This time, let's talk about a key step in formal verification, mapping. Execute the command "set_system_mode lec" in LEC and the tool will do the mapping operation; if you do not want the tool to do mapping in the switch mode, use the command "set_system_mode lec-nomap" to switch to the lec mode, and then use the command "map_key_points" to do the mapping. If you are not stubborn, please use the first way.

Mapping is the most critical step in formal verification. Whether the mapping algorithm is powerful or not basically determines the pros and cons of a formal verification tool. LEC's mapping algorithm is obviously powerful, and it can complete mapping without relying on the guidance files spit out by any optimization tool. LEC mapping can be divided into three steps:

Identification: after analyzing the design of golden and revised, identify KeyPoint.

Pairing: for each KeyPoint in Golden, determine the corresponding KeyPoint in Revised.

Bind: bind the corresponding KeyPoint together.

Identify

LEC analyzes the Golden and Revised designs to identify KeyPoint and classifies KeyPoint according to PI, PO, BBOX, DLAT, DFF, CUT, Z, E. When parsing the design, LEC will number all the Gate in the design, and each Gate has its own number, commonly known as "Gate-ID". In the subsequent debug, you can directly use this ID to access the corresponding Gate. After mapping, you can use the following command to report the corresponding KeyPoint in the design.

Report_key_point-type DFF DLAT CUT PO-revised

Pairing

Pairing is the most important and complex step in mapping, when LEC acts as an old man, through complex algorithms to find a suitable husband in Revised for every KeyPoint in Golden according to birth, sex, age and personality. When pairing, you also need to remove the redundant KeyPoint in Golden or Revised, such as the optimized constant register, the clock gating logic inserted by the tool, the merged register, and so on. These redundant KeyPoint are doomed single dogs and do not match. So far, the tool is still the driver of the user, and in LEC, the user can use the command "add mapped points" to make a forced match.

Binding

After matching, you need to bind the corresponding KeyPoint one by one. After the binding is completed, the Mapping ends, and LEC will give a summary result.

After the end of Mapping, you can click the button that looks like a book in GUI, open Mapping Manager to check the results of Mapping, successful mapping points will be marked as "Mapped Key Point", no mapping success points, will be divided into three categories: Unreachable, Extra, Not-mapped, for the meaning of each category, please listen to the next decomposition.

In a real project, the mapping process may require multiple iterations or corrections. For example, if the comprehensive tool changes the names of objects in the design beyond the default naming matching rules of LEC, you need to set them with the command "set naming rule" or "add renaming rule" in LEC, or use the command "set mapping method" to adjust the mapping policy. If the synthesis tool optimizes the redundant / constant register, does the register merge, and inserts clock gating cell, the command "set flatten model" is needed to enable the corresponding modeling algorithm. After updating the corresponding settings, you can use the command "map key points" to do further mapping.

After reading the above, do you have any further understanding of how to operate Keypoint mapping? If you want to know more knowledge or related content, please follow the industry information channel, thank you for your support.

Welcome to subscribe "Shulou Technology Information " to get latest news, interesting things and hot topics in the IT industry, and controls the hottest and latest Internet news, technology news and IT industry trends.