{"id":4521,"date":"2010-06-17T01:20:17","date_gmt":"2010-06-17T09:20:17","guid":{"rendered":"http:\/\/www.horace.org\/blog\/?p=4521"},"modified":"2010-06-17T01:20:17","modified_gmt":"2010-06-17T09:20:17","slug":"dac-technical-review-day-3","status":"publish","type":"post","link":"https:\/\/www.horace.org\/blog\/2010\/06\/17\/dac-technical-review-day-3\/","title":{"rendered":"DAC Technical Review (Day 3)"},"content":{"rendered":"<p>In the 3rd day of DAC, I went to the user track presentation on formal verification, checked out the booth of <em>Onespin<\/em>,<em> Jasper, SpringSoft, Tuscany, AMIQ, Starnet, Forte Design System <\/em>and <em>Cypber WorkBench<\/em><\/p>\n<p><strong>User track presentation on formal verification<\/strong><\/p>\n<p>The user track presentation is where users of the EDA present their work on how make the best and creative use of the EDA tools.\u00a0 There are about 40 presentation today and about 10 of them is related to verification.\u00a0 I read their presentation poster and then talk to them to exchange ideas.\u00a0 Here is a few pointers I picked up from the presentation:<\/p>\n<ul>\n<li>Use formal verification tool to aid closing of code coverage.\u00a0 For the line of code is not yet covered, we can write a property statement for that line, feed it to the formal engine and ask it to come up with a input sequence that will trigger the assertion.\u00a0 The formal engine may either generate an input sequence or prove the line is unreachable.<\/li>\n<li>Sun\/Oracle has the idea to run the property in the simulation to keep both formal and simulation in sync.\u00a0 The trick\u00a0 is to have some &#8220;useless&#8221; signals in the DUT to qualify the assertion check to avoid having tons of false-negative when the DUT is an invalid state.<\/li>\n<li>One presentation presents the result that using formal verification early in the development cycle will catch more bugs in FV.\u00a0 Duh!<\/li>\n<li>This is a good one.\u00a0 In formal verification, there are two types of properties, abstract properties that is safe and incomplete, constraint properties that are unsafe and complete.\u00a0 Using which properties type is a trade off between finding counter example or getting a full proof of the design.<\/li>\n<li>Exhaust prove is difficult, it is more practical to limit the proof to some reasonable depth.<\/li>\n<\/ul>\n<p><strong>Onespin<\/strong><\/p>\n<p>This company build formal verification tool.\u00a0 Their basic product is similar to IFV, except it has a better and easier to use GUI that allow users do a lot more interaction and visualization.\u00a0 Their flag ship product is operational formal ABV, instead of defining basic cause-reaction properties in ABV, the tool provides assertion library allow user define operational properties.\u00a0 Then the user will go through an iteration to get a full coverage on the formal space with the aid of the tool.\u00a0 The idea is to generate a set of properties that completely define the RTL.\u00a0 I think the tool will work as it advertise because at the end is human who has to enter the missing properties.\u00a0 However I wonder what&#8217;s the use of getting a complete ABV definition of the RTL.\u00a0 It seems the idea is totally up side down.\u00a0 I guess the idea is instead of auditing the implementation of the RTL code, the auditor should audit the complete properties of the code.<\/p>\n<p>One thing I don&#8217;t like about Onespin is they have way too many products and it&#8217;s really confusing.\u00a0 The flag ship product has all the features and the rest are just crippled version with fancy marketing terms simply to confuse users.\u00a0 For example, the difference between two products is only the ability to load external property files vs the property has to be in the same file of the RTL code.\u00a0 I don&#8217;t really like this kind of marketing ploy simply exist to milk more money from the customer.<\/p>\n<p><strong>Jasper<\/strong><\/p>\n<p>Jasper is THE formal verification tool vendor.\u00a0\u00a0 I spent almost 2 hours (and have my lunch) in their booth walk through all the demo and try out almost all the features in their product.\u00a0 This is the tools of choice in may formal verification presentation in DAC.\u00a0 The tool is much more user friendly and powerful than IFV.\u00a0 IFV seems so primitive compare to Jasper.\u00a0 Jasper also has property libraries for different memory, FIFO model instead of just black-boxing them out.\u00a0 It support tunnel, so the user can steer the formal engine.\u00a0 It comes with a lot more formal engines than IFV and gives very clever ways to get a counter example or a proof.\u00a0 Active design uses the same formal engine but it is for a different application.\u00a0 The idea is if we have poorly documented legacy RTL, the new designer can use active design to generate properties of the RTL and understand exactly what the RTL can and cannot do.\u00a0 Another benefit is when we ask the designer can the RTL do such and such, we no longer have to take their work for it, the designer can generate recipe to prove their design to answer our question.\u00a0 Jasper has an account manager for PMC and she know Bob and Alan.\u00a0 I think we really should try Jasper in Digi and get Bob setup the tool for us.<\/p>\n<p><strong>SpringSoft<\/strong><\/p>\n<p>Springsoft acquired Debussy.\u00a0 Debussy and Verdi does not change much, other than it added support to power-aware design and system verilog.\u00a0 Siloti is an very neat add-on to Debussy for waveform compression. \u00a0 The idea is very neat, in simulation we really only need the input, output and flip flop values in the waveform database.\u00a0 The waveform viewer can calculate the value of the combination signals on the fly.\u00a0 The waveform database is only 25% of the original size.\u00a0 Certitude is a tool to test the testbench.\u00a0 It corrupts the DUT and check whether the testbench fail.\u00a0 If the testbench still pass when there is signal corruption in the DUT, there must be something wrong with the testbench.<\/p>\n<p><strong>Tuscany<\/strong><\/p>\n<p>This company has only 1 product.\u00a0 It is a web interface GUI to display the timing report.\u00a0 I like the GUI, even though I don&#8217;t know much about timing report.\u00a0 I can see it solve the problem of how to keep track of so many timing reports.<\/p>\n<p><strong>AMIQ<\/strong><\/p>\n<p>Another small company with only 1 product.\u00a0 They have a DVT IDE for Specman and SystemVerilog base on Eclipse, the open source Java IDE.\u00a0 The IDE works like Visual Studio, it has editor, data browser, structure tree, keyword auto-complete, quick linting, hooks to launch Specrun, all under the same GUI.\u00a0 It is a lot more user friendly compare to editing e code with vi or Emacs.\u00a0 They are working on the debug interface hooking into the simulation for the next release, it will work like gdb.\u00a0 I highly recommend purchase a few license (1k per seat, but I am sure Bob can negotiate volume discount if we buy more), give it out to the team to evaluate the product.  I think we will see productivity increase with the DVT IDE instantly.<\/p>\n<p><strong>Starnet<\/strong><\/p>\n<p>They are selling a VNC replacement that they claim s much faster then VNC.\u00a0 I know CAD is evaluating some fast VNC-like software right now.\u00a0 Maybe we should get CAD to try out this product as well.\u00a0 We all know how painful is it to view waveform in Banaglore via VNC.<\/p>\n<p><strong>Forte Design System <\/strong>and <strong>Cypber WorkBench<\/strong><\/p>\n<p>Both company sells high level synthesis (HLS) tool, that compile SystemC into RTL code.\u00a0 It looks like HLS is finally here.\u00a0 I don&#8217;t have enough domain knowledge to evaluate the tools.\u00a0 All I can tell is they have a nice GUI and the RTL code generated is not very readable.\u00a0 I asked about is there any limitation on the SystemC code and the efficiency of the generated RTL, I only got the typical marketing answer.\u00a0 Too bad that both tools only work with SystemC, it would be nice if there is HLS for behavioral SystemVerilog.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>In the 3rd day of DAC, I went to the user track presentation on formal verification, checked out the booth of Onespin, Jasper, SpringSoft, Tuscany, AMIQ, Starnet, Forte Design System and Cypber WorkBench User track presentation on formal verification The user track presentation is where users of the EDA present their work on how make &hellip; <a href=\"https:\/\/www.horace.org\/blog\/2010\/06\/17\/dac-technical-review-day-3\/\" class=\"more-link\">Continue reading <span class=\"screen-reader-text\">DAC Technical Review (Day 3)<\/span> <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"lc_iscn_info":[],"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[1],"tags":[],"class_list":["post-4521","post","type-post","status-publish","format-standard","hentry","category-_scribble"],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v27.4 - https:\/\/yoast.com\/product\/yoast-seo-wordpress\/ -->\n<title>DAC Technical Review (Day 3) - \u54f2\u5b50\u6232 Philosophist\u2019s Camp<\/title>\n<meta name=\"description\" content=\"In the 3rd day of DAC, I went to the user track presentation on formal verification, checked out the booth of Onespin, Jasper, SpringSoft, Tuscany, AMIQ,\" \/>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/www.horace.org\/blog\/2010\/06\/17\/dac-technical-review-day-3\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"DAC Technical Review (Day 3) - \u54f2\u5b50\u6232 Philosophist\u2019s Camp\" \/>\n<meta property=\"og:description\" content=\"In the 3rd day of DAC, I went to the user track presentation on formal verification, checked out the booth of Onespin, Jasper, SpringSoft, Tuscany, AMIQ,\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.horace.org\/blog\/2010\/06\/17\/dac-technical-review-day-3\/\" \/>\n<meta property=\"og:site_name\" content=\"\u54f2\u5b50\u6232 Philosophist\u2019s Camp\" \/>\n<meta property=\"article:publisher\" content=\"https:\/\/www.facebook.com\/horace.org\" \/>\n<meta property=\"article:author\" content=\"https:\/\/www.facebook.com\/horace.org\" \/>\n<meta property=\"article:published_time\" content=\"2010-06-17T09:20:17+00:00\" \/>\n<meta name=\"author\" content=\"hevangel\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:creator\" content=\"@horaceorg\" \/>\n<meta name=\"twitter:site\" content=\"@horaceorg\" \/>\n<meta name=\"twitter:label1\" content=\"Written by\" \/>\n\t<meta name=\"twitter:data1\" content=\"hevangel\" \/>\n\t<meta name=\"twitter:label2\" content=\"Est. reading time\" \/>\n\t<meta name=\"twitter:data2\" content=\"6 minutes\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\\\/\\\/schema.org\",\"@graph\":[{\"@type\":\"Article\",\"@id\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/2010\\\/06\\\/17\\\/dac-technical-review-day-3\\\/#article\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/2010\\\/06\\\/17\\\/dac-technical-review-day-3\\\/\"},\"author\":{\"name\":\"hevangel\",\"@id\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/#\\\/schema\\\/person\\\/c8d9e8e7a71d343b4b2c4ef4365cdb4c\"},\"headline\":\"DAC Technical Review (Day 3)\",\"datePublished\":\"2010-06-17T09:20:17+00:00\",\"mainEntityOfPage\":{\"@id\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/2010\\\/06\\\/17\\\/dac-technical-review-day-3\\\/\"},\"wordCount\":1243,\"commentCount\":0,\"publisher\":{\"@id\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/#\\\/schema\\\/person\\\/c8d9e8e7a71d343b4b2c4ef4365cdb4c\"},\"articleSection\":[\"Daily Scribble\"],\"inLanguage\":\"en-CA\",\"potentialAction\":[{\"@type\":\"CommentAction\",\"name\":\"Comment\",\"target\":[\"https:\\\/\\\/www.horace.org\\\/blog\\\/2010\\\/06\\\/17\\\/dac-technical-review-day-3\\\/#respond\"]}]},{\"@type\":\"WebPage\",\"@id\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/2010\\\/06\\\/17\\\/dac-technical-review-day-3\\\/\",\"url\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/2010\\\/06\\\/17\\\/dac-technical-review-day-3\\\/\",\"name\":\"DAC Technical Review (Day 3) - \u54f2\u5b50\u6232 Philosophist\u2019s Camp\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/#website\"},\"datePublished\":\"2010-06-17T09:20:17+00:00\",\"description\":\"In the 3rd day of DAC, I went to the user track presentation on formal verification, checked out the booth of Onespin, Jasper, SpringSoft, Tuscany, AMIQ,\",\"breadcrumb\":{\"@id\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/2010\\\/06\\\/17\\\/dac-technical-review-day-3\\\/#breadcrumb\"},\"inLanguage\":\"en-CA\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\\\/\\\/www.horace.org\\\/blog\\\/2010\\\/06\\\/17\\\/dac-technical-review-day-3\\\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/2010\\\/06\\\/17\\\/dac-technical-review-day-3\\\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"DAC Technical Review (Day 3)\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/#website\",\"url\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/\",\"name\":\"\u54f2\u5b50\u6232 Philosophist\u2019s Camp\",\"description\":\"\u860b\u679c\u65e5\u5831\u4f5c\u8005 - \u9673\u99ac\uff1a\u66f8\u8a55\uff0c\u5f71\u8a55\uff0c\u52d5\u6f2b\uff0c\u65c5\u884c\uff0c\u54f2\u5b78\u7b46\u8a18\",\"publisher\":{\"@id\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/#\\\/schema\\\/person\\\/c8d9e8e7a71d343b4b2c4ef4365cdb4c\"},\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/?s={search_term_string}\"},\"query-input\":{\"@type\":\"PropertyValueSpecification\",\"valueRequired\":true,\"valueName\":\"search_term_string\"}}],\"inLanguage\":\"en-CA\"},{\"@type\":[\"Person\",\"Organization\"],\"@id\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/#\\\/schema\\\/person\\\/c8d9e8e7a71d343b4b2c4ef4365cdb4c\",\"name\":\"hevangel\",\"image\":{\"@type\":\"ImageObject\",\"inLanguage\":\"en-CA\",\"@id\":\"https:\\\/\\\/i0.wp.com\\\/www.horace.org\\\/blog\\\/wp-content\\\/uploads\\\/2021\\\/11\\\/spocky.jpg?fit=1313%2C1259&ssl=1\",\"url\":\"https:\\\/\\\/i0.wp.com\\\/www.horace.org\\\/blog\\\/wp-content\\\/uploads\\\/2021\\\/11\\\/spocky.jpg?fit=1313%2C1259&ssl=1\",\"contentUrl\":\"https:\\\/\\\/i0.wp.com\\\/www.horace.org\\\/blog\\\/wp-content\\\/uploads\\\/2021\\\/11\\\/spocky.jpg?fit=1313%2C1259&ssl=1\",\"width\":1313,\"height\":1259,\"caption\":\"hevangel\"},\"logo\":{\"@id\":\"https:\\\/\\\/i0.wp.com\\\/www.horace.org\\\/blog\\\/wp-content\\\/uploads\\\/2021\\\/11\\\/spocky.jpg?fit=1313%2C1259&ssl=1\"},\"sameAs\":[\"http:\\\/\\\/www.horace.org\",\"https:\\\/\\\/www.facebook.com\\\/horace.org\"],\"url\":\"https:\\\/\\\/www.horace.org\\\/blog\\\/author\\\/hevangel-2\\\/\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"DAC Technical Review (Day 3) - \u54f2\u5b50\u6232 Philosophist\u2019s Camp","description":"In the 3rd day of DAC, I went to the user track presentation on formal verification, checked out the booth of Onespin, Jasper, SpringSoft, Tuscany, AMIQ,","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/www.horace.org\/blog\/2010\/06\/17\/dac-technical-review-day-3\/","og_locale":"en_US","og_type":"article","og_title":"DAC Technical Review (Day 3) - \u54f2\u5b50\u6232 Philosophist\u2019s Camp","og_description":"In the 3rd day of DAC, I went to the user track presentation on formal verification, checked out the booth of Onespin, Jasper, SpringSoft, Tuscany, AMIQ,","og_url":"https:\/\/www.horace.org\/blog\/2010\/06\/17\/dac-technical-review-day-3\/","og_site_name":"\u54f2\u5b50\u6232 Philosophist\u2019s Camp","article_publisher":"https:\/\/www.facebook.com\/horace.org","article_author":"https:\/\/www.facebook.com\/horace.org","article_published_time":"2010-06-17T09:20:17+00:00","author":"hevangel","twitter_card":"summary_large_image","twitter_creator":"@horaceorg","twitter_site":"@horaceorg","twitter_misc":{"Written by":"hevangel","Est. reading time":"6 minutes"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"Article","@id":"https:\/\/www.horace.org\/blog\/2010\/06\/17\/dac-technical-review-day-3\/#article","isPartOf":{"@id":"https:\/\/www.horace.org\/blog\/2010\/06\/17\/dac-technical-review-day-3\/"},"author":{"name":"hevangel","@id":"https:\/\/www.horace.org\/blog\/#\/schema\/person\/c8d9e8e7a71d343b4b2c4ef4365cdb4c"},"headline":"DAC Technical Review (Day 3)","datePublished":"2010-06-17T09:20:17+00:00","mainEntityOfPage":{"@id":"https:\/\/www.horace.org\/blog\/2010\/06\/17\/dac-technical-review-day-3\/"},"wordCount":1243,"commentCount":0,"publisher":{"@id":"https:\/\/www.horace.org\/blog\/#\/schema\/person\/c8d9e8e7a71d343b4b2c4ef4365cdb4c"},"articleSection":["Daily Scribble"],"inLanguage":"en-CA","potentialAction":[{"@type":"CommentAction","name":"Comment","target":["https:\/\/www.horace.org\/blog\/2010\/06\/17\/dac-technical-review-day-3\/#respond"]}]},{"@type":"WebPage","@id":"https:\/\/www.horace.org\/blog\/2010\/06\/17\/dac-technical-review-day-3\/","url":"https:\/\/www.horace.org\/blog\/2010\/06\/17\/dac-technical-review-day-3\/","name":"DAC Technical Review (Day 3) - \u54f2\u5b50\u6232 Philosophist\u2019s Camp","isPartOf":{"@id":"https:\/\/www.horace.org\/blog\/#website"},"datePublished":"2010-06-17T09:20:17+00:00","description":"In the 3rd day of DAC, I went to the user track presentation on formal verification, checked out the booth of Onespin, Jasper, SpringSoft, Tuscany, AMIQ,","breadcrumb":{"@id":"https:\/\/www.horace.org\/blog\/2010\/06\/17\/dac-technical-review-day-3\/#breadcrumb"},"inLanguage":"en-CA","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.horace.org\/blog\/2010\/06\/17\/dac-technical-review-day-3\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/www.horace.org\/blog\/2010\/06\/17\/dac-technical-review-day-3\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.horace.org\/blog\/"},{"@type":"ListItem","position":2,"name":"DAC Technical Review (Day 3)"}]},{"@type":"WebSite","@id":"https:\/\/www.horace.org\/blog\/#website","url":"https:\/\/www.horace.org\/blog\/","name":"\u54f2\u5b50\u6232 Philosophist\u2019s Camp","description":"\u860b\u679c\u65e5\u5831\u4f5c\u8005 - \u9673\u99ac\uff1a\u66f8\u8a55\uff0c\u5f71\u8a55\uff0c\u52d5\u6f2b\uff0c\u65c5\u884c\uff0c\u54f2\u5b78\u7b46\u8a18","publisher":{"@id":"https:\/\/www.horace.org\/blog\/#\/schema\/person\/c8d9e8e7a71d343b4b2c4ef4365cdb4c"},"potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/www.horace.org\/blog\/?s={search_term_string}"},"query-input":{"@type":"PropertyValueSpecification","valueRequired":true,"valueName":"search_term_string"}}],"inLanguage":"en-CA"},{"@type":["Person","Organization"],"@id":"https:\/\/www.horace.org\/blog\/#\/schema\/person\/c8d9e8e7a71d343b4b2c4ef4365cdb4c","name":"hevangel","image":{"@type":"ImageObject","inLanguage":"en-CA","@id":"https:\/\/i0.wp.com\/www.horace.org\/blog\/wp-content\/uploads\/2021\/11\/spocky.jpg?fit=1313%2C1259&ssl=1","url":"https:\/\/i0.wp.com\/www.horace.org\/blog\/wp-content\/uploads\/2021\/11\/spocky.jpg?fit=1313%2C1259&ssl=1","contentUrl":"https:\/\/i0.wp.com\/www.horace.org\/blog\/wp-content\/uploads\/2021\/11\/spocky.jpg?fit=1313%2C1259&ssl=1","width":1313,"height":1259,"caption":"hevangel"},"logo":{"@id":"https:\/\/i0.wp.com\/www.horace.org\/blog\/wp-content\/uploads\/2021\/11\/spocky.jpg?fit=1313%2C1259&ssl=1"},"sameAs":["http:\/\/www.horace.org","https:\/\/www.facebook.com\/horace.org"],"url":"https:\/\/www.horace.org\/blog\/author\/hevangel-2\/"}]}},"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/pwn21-1aV","jetpack_sharing_enabled":true,"jetpack-related-posts":[{"id":4527,"url":"https:\/\/www.horace.org\/blog\/2010\/06\/23\/dac-technical-review-day-45\/","url_meta":{"origin":4521,"position":0},"title":"DAC Technical Review (Day 4,5)","author":"hevangel","date":"June 23, 2010","format":false,"excerpt":"The exhibition floor is over in day 4 and 5. In day 4, I attended user track presentation on verification and a technical session on What input language for HLS. In day 5, I attended a workshop on Software Engineering using Agile Software Development technics User track presentation on verification\u2026","rel":"","context":"In &quot;Daily Scribble&quot;","block_context":{"text":"Daily Scribble","link":"https:\/\/www.horace.org\/blog\/category\/_scribble\/"},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":4512,"url":"https:\/\/www.horace.org\/blog\/2010\/06\/15\/dac-2010-day-1-technical-review\/","url_meta":{"origin":4521,"position":1},"title":"DAC 2010 Technical Report (Day 1)","author":"hevangel","date":"June 15, 2010","format":false,"excerpt":"Today is the report of my first day in DAC. I signed up to a full day technical workshop Choosing Advanced Verification Methodology. After the workshop ended at 3:30p, I managed to checked out a few companies in the exhibition floor Vennsa Technologyies, Agnisys Inc and Veritools Advanced Verification Methodology\u2026","rel":"","context":"In &quot;Daily Scribble&quot;","block_context":{"text":"Daily Scribble","link":"https:\/\/www.horace.org\/blog\/category\/_scribble\/"},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":4515,"url":"https:\/\/www.horace.org\/blog\/2010\/06\/16\/dac-technical-review-day-2\/","url_meta":{"origin":4521,"position":2},"title":"DAC Technical Review (Day 2)","author":"hevangel","date":"June 16, 2010","format":false,"excerpt":"In the 2nd day of DAC, I attended a technology Session Bridging pre-silicon verification and post-silicon validation, a user track presentation on An Open Database for the Open Verification Methodology Synopsys VCS demo and verification luncheon, visited the booth of the following companies: Realintent, Adlec, IBM, Nextop, eVe, ExpertIO Bridging\u2026","rel":"","context":"In &quot;Daily Scribble&quot;","block_context":{"text":"Daily Scribble","link":"https:\/\/www.horace.org\/blog\/category\/_scribble\/"},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":532,"url":"https:\/\/www.horace.org\/blog\/2006\/10\/13\/psl-assertions\/","url_meta":{"origin":4521,"position":3},"title":"PSL assertions","author":"hevangel","date":"October 13, 2006","format":false,"excerpt":"This week I have been spending some time learning PSL assertion at work.? Assertion is a new verification methodology pushing very hard from the EDA venders.? It is a complement to the traditional verification flow, which you have no visibility inside the device.? Assertion allows you put extra checks right\u2026","rel":"","context":"In &quot;Daily Scribble&quot;","block_context":{"text":"Daily Scribble","link":"https:\/\/www.horace.org\/blog\/category\/_scribble\/"},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":4169,"url":"https:\/\/www.horace.org\/blog\/2010\/03\/11\/challenging-misconceptions-about-verification-languages\/","url_meta":{"origin":4521,"position":4},"title":"Challenging Misconceptions About Verification Languages","author":"hevangel","date":"March 11, 2010","format":false,"excerpt":"Looks like Cadence is finally on offensive and pushing Specman strongly over SystemVerilog. As a long time user of Specman, I would like to see Specman wins the HVL war at the end which will make my skill and experience more valuable. By Richard Goering on March 10, 2010 One\u2026","rel":"","context":"In &quot;News Clips&quot;","block_context":{"text":"News Clips","link":"https:\/\/www.horace.org\/blog\/category\/_reference\/_newsclips\/"},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":12152,"url":"https:\/\/www.horace.org\/blog\/2017\/06\/21\/formal-verification-erik-seligman-tom-schubert\/","url_meta":{"origin":4521,"position":5},"title":"Formal Verification &#8211; Erik Seligman, Tom Schubert","author":"hevangel","date":"June 21, 2017","format":false,"excerpt":"\u9019\u7bc7\u4e0d\u662f\u66f8\u8a55\uff0c\u9019\u672c\u66f8\u4ea6\u4e0d\u662f\u4e00\u822c\u81ea\u5b78\u7a0b\u5f0f\u8a2d\u8a08\u7684\u96fb\u8166\u66f8\uff0c\u662f\u4e00\u672c\u6d89\u53ca\u975e\u5e38\u5c08\u9580\u7684\u77e5\u8b58\uff0c\u53ea\u6709\u8a2d\u8a08\u6676\u7247\u624d\u6703\u7528\u5f97\u4e0a\u7684\u6280\u8853\u8ab2\u672c\u3002\u975e\u884c\u5167\u4eba\u5b8c\u5168\u770b\u4e0d\u660e\u767d\uff0c\u9019\u7bc7\u53ea\u662f\u6211\u5b78\u7fd2formal verification(\u5f62\u5f0f\u5316\u9a57\u8b49)\u7684\u5fc3\u5f97\u548c\u7b46\u8a18\uff0c\u6240\u4ee5\u6211\u4ea6\u4e0d\u671f\u671b\u6709\u4ec0\u9ebc\u8b80\u8005\u3002 \u4ec0\u9ebc\u662fFormal Verification\uff1f\u9996\u5148\u8981\u8b1b\u4ec0\u9ebc\u662fdynamic verification\uff0c\u8a2d\u8a08\u6676\u7247\u4e0d\u540c\u5beb\u7a0b\u5f0f\uff0c\u5beb\u7a0b\u5f0f\u6709bug\u5f88\u7c21\u55ae\uff0c\u9664\u932f\u51fapatch\u6c92\u6709\u4ec0\u9ebc\u5927\u4e0d\u4e86\u3002\u6676\u7247\u6709bug\u5c31\u5f88\u5927\u4ef6\u4e8b\uff0c\u56e0\u70ba\u8981\u66f4\u6b63\u554f\u984c\uff0c\u5c31\u8981\u91cd\u65b0tape-out\u591a\u4e00\u6b21\uff0c\u53bb\u505a\u4e00\u500b\u5168\u65b0\u7684mask\u3002\u53ef\u4ee5\u60f3\u50cf\u88fd\u9020\u6676\u7247\u597d\u5370\u9ed1\u81a0\u789f\uff0c\u5148\u8981\u6574\u6709\u4e00\u5f35\u6bcd\u789f\uff0c\u7136\u5f8c\u624d\u53ef\u4ee5\u8986\u5370\uff0cmask\u5c31\u662fsilicon\u7684\u6bcd\u789f\u3002\u50b3\u7d71\u4e0a\u6e2c\u5f0f\u6676\u7247\u8a2d\u4ef6\u4e3b\u529b\u7528simulation\uff08\u5373dynamic verification)\uff0c\u8981\u82b1\u5f88\u591a\u4eba\u529b\u7269\u529b\u5beb\u500btestbench\u51fa\u4f86\uff0c\u7136\u5f8c\u6a21\u7591\u6676\u7247\u6240\u6709\u7684input\u540coutput\u3002\u9019\u662f\u4e00\u500b\u975e\u5e38\u56b4\u683c\u7684\u5de5\u5e8f\uff0c\u56e0\u70ba\u4e00\u500bbug\u4e5f\u4e0d\u53ef\u4ee5\u8d70\u6f0f\u3002\u6676\u7247\u51fa\u4e86\u8857\u4e4b\u5f8c\uff0cfix\u4e00\u500bbug\u7684\u6210\u672c\u662f\u5e7e\u767e\u842c\u7f8e\u5143\u3002\u5bebtestbench\u540c\u5beb\u666e\u901asoftware\u6c92\u6709\u592a\u5927\u5206\u5225\uff0c\u53ea\u4e0d\u904e\u6e2c\u8a66\u786c\u4ef6\u6bd4\u6e2c\u8a66\u8edf\u4ef6\u56b4\u683c\u5f88\u591a\u3002Formal Verification\u5247\u662f\u7528\u53e6\u4e00\u500b\u65b9\u6cd5\u53bb\u6e2c\u8a66\u786c\u4ef6\uff0c\u4e0d\u7528\u5bebcode\uff0c\u5bebformal specification\uff0c\u518d\u7528\u6578\u5b78\u908f\u8f2f\u7406\u8ad6\uff0c\u53bb\u8b49\u660e\u786c\u4ef6\u7684\u8a2d\u4ef6\u5fc5\u5b9a\u7b49\u65bc\u90a3\u500bspecification\u3002\u5b8c\u5168\u4e0d\u540c\u7684\u601d\u8003\u65b9\u6cd5\uff0c\u5b8c\u5168\u4e0d\u540c\u7684\u7528\u9014\u3002Formal Verification\u53ef\u4ee5\u6e2c\u8a66\u51fasimulation\u627e\u4e0d\u51fa\u4f86\u7684bug\uff0c\u59cb\u7d42simulation\u4e26\u4e0d\u662fexhaustive\uff0c\u4e0d\u904eformal\u6709\u5f88\u591a\u9650\u5236\uff0c\u8a2d\u8a08\u4e0d\u80fd\u592a\u5927\u4e0d\u80fd\u592a\u6df1\uff0c\u59cb\u7d42formal proof\u4fc2\u4e00\u500bNP-complete problem\u3002 \u591a\u5e74\u4f86formal\u4e00\u76f4\u53ea\u662f\u5b78\u8853\u7814\u7a76\uff0c\u771f\u6b63\u7684\u5546\u696d\u61c9\u7528\uff0c\u5927\u7d04\u4e94\u516d\u5e74\u524d\u624d\u958b\u59cb\u3002\u65e9\u671f\u7684formal tool\u975e\u5e38\u96e3\u7528\uff0c\u5e38\u5e38\u88ab\u6232\u8aaa\u8981\u535a\u58eb\u624d\u61c2\u7528\uff0c\u5f88\u591adesigner\u807d\u898b\u4fbf\u656c\u800c\u9060\u4e4b\u3002\u76f4\u81f3JasperGold\u7684\u63a8\u51fa\uff0cformal\u624d\u958b\u59cb\u666e\u53ca\u5316\uff0c\u9019\u4e9b\u5e74\u4f86JasperGold\u624b\u57f7\u725b\u8033\uff0c\u4e00\u679d\u7368\u79c0\u5dee\u4e0d\u591a\u7b49\u540c\u65bcformal\u7684\u4ee3\u540d\u8a5e\u3002\u65e9\u5169\u5e74\u6211\u4e5f\u5617\u8a66\u904e\u5b78formal\uff0c\u4e0d\u904e\u7576\u5e74JasperGold\u7684license\u592a\u8cb4\uff0c\u6211\u5011\u7d30\u516c\u53f8\u8cb7\u4e0d\u8d77\uff0c\u53ea\u597d\u7528\u4e86\u4e00\u500b\u5f88\u5dee\u5f88\u96e3\u7528\u7684IFV\uff0c\u7d50\u679c\u5b78\u5e2b\u672a\u6210\u4e0d\u4e86\u4e86\u4e4b\u3002\u53bb\u5e74\u6211\u516c\u53f8\u88ab\u4e00\u500b\u5927\u516c\u53f8\u6536\u8cfc\u4e86\uff0ceconomy of scale\u8b93\u6211\u5011\u6709\u591a\u597d\u591atools\u7528\uff0c\u4eca\u500bproject\u7d42\u65bc\u6709\u6a5f\u6703\u7528\u5230JasperGold\uff0c\u540cIFV\u76f8\u6bd4\u7c21\u76f4\u662f\u5929\u5802\u548c\u5730\u7344\uff0c\u300c\u5de5\u6b32\u5584\u5176\u5584\uff0c\u5fc5\u5148\u5229\u5176\u5668\u300d\uff0c\u5176\u5be6formal\u4e00\u9ede\u4e5f\u4e0d\u96e3\uff0c\u6211\u82b1\u4e86\u5169\u661f\u671f\u4fbf\u6eff\u5e2b\uff0c\u53ef\u4ee5\u5b78\u61c2\u7c21\u55ae\u7684formal specify\uff0c\u53bbproof\u6211\u500bdesign\u4e0d\u6703\u6709dead lock\u3002\u5982\u679c\u8981\u7528simulation\u4f5c\u540c\u6a23\u6e2c\u8a66\uff0c\u56e0\u70ba\u592a\u591acorner cases\uff0c\u662f\u4e00\u4ef6\u975e\u5e38\u75db\u82e6\u7684\u5dee\u4e8b\u3002\u73fe\u5728\u7528formal\u53bb\u505a\uff0c\u5e7e\u884ccode\u5beb\u5b8c\uff0c\u662f\u4e00\u4ef6\u5f88\u597d\u73a9\u7684\u73a9\u610f\u3002 \u6211\u4e00\u76f4\u90fd\u6709follow\u958bformal\u7684paper\u548ctutorial\uff0c\u96d6\u7136\u6c92\u6709\u5be6\u6230\u7d93\u9a57\u4f46formal\u7406\u8ad6\u5927\u81f3\u660e\u767d\uff0c\u7528\u65b0tool\u4e0d\u904e\u662f\u5b78syntax\uff0c\u5f88\u5feb\u4e0a\u624b\u3002\u6211\u516c\u53f8\u7684formal expert\u4ecb\u7d39\u6211\u770b\u9019\u672c\u300aFormal Verification\u300b\u8ab2\u672c\uff0c\u9019\u672c\u66f8\u662f\u4e09\u4f4dIntel\u5de5\u7a0b\u5e2b\u7de8\u5beb\u7684\uff0c\u7531\u6dfa\u5165\u6df1\u8b1b\u89e3\u5f88\u6709\u7cfb\u7d71\u5730\u5982\u4f55\u61c9\u7528formal verification\uff0c\u771f\u6b63\u7684hard-core\u6280\u8853\u542b\u91cf\u4e0d\u591a\uff08\u6280\u8853\u6771\u897f\u53ef\u4ee5\u81ea\u5df2\u770bdocument)\uff0c\u53cd\u800c\u66f4\u50cf\u662f\u904e\u4f86\u4eba\u5206\u4eab\u5fc3\u5f97\u548c\u7d93\u9a57\u3002\u9019\u672c\u66f8\u4e5d\u6210\u662f\u8001\u751f\u5e38\u8ac7\uff0c\u5e73\u6642\u7747tutorial\u7747paper\u90fd\u5b78\u904e\u807d\u904e\uff0c\u4e0d\u904e\u9918\u4e0b\u7684\u4e00\u6210\u975e\u5e38\u6709\u7528\uff0c\u8b93\u6211\u8305\u585e\u9813\u958b\uff0c\u5f88\u591a\u770b\u5df2paper\u4e0d\u660e\u767d\u4eba\u5bb6\u70ba\u4ec0\u9ebc\u4e00\u5b9a\u8981\u9019\u6a23\u505a\u7684\u5730\u65b9\uff0c\u7d93\u4ed6\u4e00\u89e3\u91cb\u5b8c\u5168\u660e\u767d\uff0c\u4e00\u7406\u901a\uff0c\u767e\u7406\u660e\u3002\u9019\u672c\u66f8\u53ef\u4ee5\u8aaa\u662f\u6211formal\u7684\u555f\u8499\u8001\u5e2b\uff0c\u4efb\u4f55\u4e00\u500b\u521d\u5b78formal\u8005\u5fc5\u5b9a\u8981\u770b\u3002\u5e02\u9762\u4e0aformal\u7684textbook\u4e00\u96bb\u624b\u6578\u5f97\u5b8c\uff0c\u56e0\u70baformal\u662f\u592a\u5c08\u9580\u7684\u6280\u8853\uff0c\u8b4e\u60f3\u60f3\u5b78\u5c31\u8981\u4ea4\u5f88\u8cb4\u5b78\u8cbb\u8acbconsultant\u53bb\u6559\uff0c\u4e0d\u904e\u6211\u8a8d\u70ba\u9019\u672c\u66f8\u6bd4consultant\u6559\u5f97\u66f4\u597d\uff0c\u56e0\u70ba\u4f5c\u8005\u6709\u771f\u6b63\u7684\u5be6\u6230\u7d93\u6b77\uff0c\u4e0d\u4f3cconsultant\u822c\u5927\u591a\u7d19\u4e0a\u8ac7\u5175\u3002 \u4ee5\u4e0b\u662f\u6211\u8a8d\u70ba\u66f8\u4e2d\u6709\u7528\u7684formal\u300c\u5fc3\u6cd5\u300d\uff1a cover\u548cassert\u662f\u540c\u4e00\u584a\u93e1\u5b50\u7684\u5169\u9762\u3002\u540c\u4e00\u500bproperty\uff0ccover\u5c31\u662fnot\u5de6\u500bproperty\u7684assert\u7684counter example\u3002assert\u5c31\u4fc2not\u5de6\u500bcover\u65e2unreachable proof Formal engine\u4fc2\u4e00\u500bbreath-first\u5481\u53bb\u884c\u6240\u6709\u7684state space\u3002assume\u540cassert\u5c31\u4fc2cut\u7d30\u500bstate space\uff0ccut\u8d70\u5de6illegal state\uff0c\u5982\u679c\u884c\u5230\u53bbspecification\u679c\u500bstate\uff0c\u54aa\u5c31proof\u5ea6\u56c9\u3002 \u4e00\u958b\u6ce2\u4e0d\u8981\u7acb\u5373\u5bebfull proof\uff0c\u5148\u7531cover\u958b\u59cb\u73a9\u3002\u5514\u7528assume\uff0c\u5269\u4fc2\u5beb\u4f60\u60f3\u7747\u4e5coutput\uff0c\u7747\u4e0bformal engine\u53ef\u4e0d\u53ef\u4ee5back trace\u4f60\u60f3\u8981\u7684input\uff0c\u7136\u5f8c\u518d\u6162\u6162fine-tune\u90a3\u4e9bassume \u7528cover\u6574\u597d\u6652assume\uff0c\u5c31\u53ef\u4ee5\u4e0a\u53bbbug hunting\uff0c\u5c08\u5fc3\u6435assert\u7684counter example\uff0c\u6700\u5f8c\u624d\u6574full proof\u3002\u7528\u4e4b\u524d\u5169\u500bsteps\u7684assume \u5514\u597dload\u592a\u591acode\uff0c\u592a\u591aassert\u540ccover\uff0c\u8981divide and conquer\u3002\u6709\u4e9btricks\u53ef\u4ee5\u7528\uff0c\u5982cutpoint\uff0cabstraction\uff0cfree variable\u7b49\u7b49","rel":"","context":"In &quot;\u66f8\u8a55&quot;","block_context":{"text":"\u66f8\u8a55","link":"https:\/\/www.horace.org\/blog\/category\/_books\/"},"img":{"alt_text":"","src":"https:\/\/i0.wp.com\/www.horace.org\/blog\/wp-content\/uploads\/2017\/06\/images.jpg?fit=624%2C768&ssl=1&resize=350%2C200","width":350,"height":200,"srcset":"https:\/\/i0.wp.com\/www.horace.org\/blog\/wp-content\/uploads\/2017\/06\/images.jpg?fit=624%2C768&ssl=1&resize=350%2C200 1x, https:\/\/i0.wp.com\/www.horace.org\/blog\/wp-content\/uploads\/2017\/06\/images.jpg?fit=624%2C768&ssl=1&resize=525%2C300 1.5x"},"classes":[]}],"jetpack_likes_enabled":false,"amp_enabled":true,"_links":{"self":[{"href":"https:\/\/www.horace.org\/blog\/wp-json\/wp\/v2\/posts\/4521","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.horace.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.horace.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.horace.org\/blog\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.horace.org\/blog\/wp-json\/wp\/v2\/comments?post=4521"}],"version-history":[{"count":1,"href":"https:\/\/www.horace.org\/blog\/wp-json\/wp\/v2\/posts\/4521\/revisions"}],"predecessor-version":[{"id":4522,"href":"https:\/\/www.horace.org\/blog\/wp-json\/wp\/v2\/posts\/4521\/revisions\/4522"}],"wp:attachment":[{"href":"https:\/\/www.horace.org\/blog\/wp-json\/wp\/v2\/media?parent=4521"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.horace.org\/blog\/wp-json\/wp\/v2\/categories?post=4521"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.horace.org\/blog\/wp-json\/wp\/v2\/tags?post=4521"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}