{"id":92,"date":"2015-11-24T15:55:48","date_gmt":"2015-11-24T15:55:48","guid":{"rendered":"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/?p=92"},"modified":"2016-07-11T15:56:12","modified_gmt":"2016-07-11T14:56:12","slug":"concepts-iii-initial-states","status":"publish","type":"post","link":"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/2015\/11\/24\/concepts-iii-initial-states\/","title":{"rendered":"Concepts III: Initial States"},"content":{"rendered":"<p><span style=\"text-decoration: underline\">Initial States<br \/>\n<\/span><\/p>\n<p>Now we have introduced a couple of simple gates, <a href=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/2015\/09\/30\/designing-asynchronous-logic-gates-using-behavioural-concepts-i-a-buffer-2\/\">a buffer<\/a> and <a href=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/2015\/10\/21\/concepts-ii-an-inverter\/\">an inverter<\/a>, we should now discuss an important part of Signal Transition Graphs, and their implementation using Concepts. These are <em>initial states. \u00a0<\/em><\/p>\n<p>Initial states are used in Signal Transition Graphs to show what state a signal is in, high or low, when the system being designed starts. This is important as STGs require initial states for simulation, verification and synthesis.<\/p>\n<p>In the previous posts, we have assumed that all signals involved in the STGs are initially set to 0, and this has been indicated by placing a <em>token <\/em>in the places which are before each signals <strong>+\u00a0<\/strong>transition (as above), but this assumption cannot be applied to every STG.<\/p>\n<p><span style=\"text-decoration: underline\">Example &#8211; A Handshake<\/span><\/p>\n<p>So now let&#8217;s use a previous example, a Handshake, and discuss what we can do to ensure there are initial states in an STG produced using concepts.<\/p>\n<p>The concept used to describe a\u00a0handshake is as follows:<\/p>\n<p><strong>handshake(a,b) = buffer(a,b)\u00a0\u22c4 inverter(b,a)<\/strong><\/p>\n<p>This concept captures the interactions of signals\u00a0<strong>a<\/strong> and\u00a0<strong>b<\/strong>, using previously defined <strong>buffer<\/strong> and <strong>inverter<\/strong> concepts, but this does not explain the state of these signals when the handshake starts.<\/p>\n<p>Initial state concepts can be defined similarly to other concepts, and thus can be composed with other concepts as normal. For this example, let&#8217;s say the two signals involved in handshake are both initially 0.<\/p>\n<p><strong>initialState = initialise(a,0)\u00a0\u22c4 initialise(b,0)<\/strong><\/p>\n<p>There is some syntax to discuss here:<\/p>\n<p>initialise(a,0) &#8211; This is used to express an initial state.\u00a0The state of the signal, a, will be initially set to 0.<\/p>\n<p>The concept, <strong>initialState,<\/strong> implies that the initial state of signals\u00a0<strong>a\u00a0<\/strong>and\u00a0<strong>b\u00a0<\/strong>will be 0, so the first transition of each can be <strong>+<\/strong>, from low to high.<\/p>\n<p>Now we can include this concept with the handshake concept:<\/p>\n<p><strong>system = handshake(a,b)\u00a0\u22c4 initialState<\/strong><\/p>\n<p>Passing this concept into the algorithm will produce the same STG as in the previous post:<\/p>\n<p><a href=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/bufferAndInverter00.png\"><img loading=\"lazy\" decoding=\"async\" class=\"aligncenter wp-image-103 size-large\" src=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/bufferAndInverter00-1024x423.png\" alt=\"bufferAndInverter00\" width=\"474\" height=\"196\" srcset=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/bufferAndInverter00-1024x423.png 1024w, https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/bufferAndInverter00-300x124.png 300w, https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/bufferAndInverter00.png 1400w\" sizes=\"auto, (max-width: 474px) 100vw, 474px\" \/><\/a><\/p>\n<p>And this can be resynthesized to produce the same handshake STG:<\/p>\n<p><a href=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/handshake00.png\"><img loading=\"lazy\" decoding=\"async\" class=\"aligncenter wp-image-104 size-medium\" src=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/handshake00-298x300.png\" alt=\"handshake00\" width=\"298\" height=\"300\" srcset=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/handshake00-298x300.png 298w, https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/handshake00-150x150.png 150w, https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/handshake00.png 303w\" sizes=\"auto, (max-width: 298px) 100vw, 298px\" \/><\/a><\/p>\n<p>However, what if the initial states are not both 0? For this, let&#8217;s redefine the initial state concept and compose this with a handshake concept:<\/p>\n<p><strong>initialState = initial(a,0)\u00a0\u22c4 initial(b,1)<br \/>\nsystem = handshake(a,b)\u00a0\u22c4 initialState<\/strong><\/p>\n<p>Now,\u00a0<strong>a<\/strong>\u00a0should initially be 0, and\u00a0<strong>b<\/strong> should initialy be 1. The STG produced from these concepts is:<\/p>\n<p><a href=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/BufferAndInverter01.png\"><img loading=\"lazy\" decoding=\"async\" class=\"alignnone wp-image-93 size-large\" src=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/BufferAndInverter01-1024x423.png\" alt=\"BufferAndInverter01\" width=\"474\" height=\"196\" srcset=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/BufferAndInverter01-1024x423.png 1024w, https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/BufferAndInverter01-300x124.png 300w, https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/BufferAndInverter01.png 1400w\" sizes=\"auto, (max-width: 474px) 100vw, 474px\" \/><\/a>This is the same as the previous version, but the tokens have shifted. After resynthesis, the STG is as follows:<a href=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/BufferAndInvertorRe01.png\"><img loading=\"lazy\" decoding=\"async\" class=\"aligncenter wp-image-94 size-medium\" src=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/BufferAndInvertorRe01-300x297.png\" alt=\"BufferAndInvertorRe01\" width=\"300\" height=\"297\" srcset=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/BufferAndInvertorRe01-300x297.png 300w, https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/BufferAndInvertorRe01-150x150.png 150w, https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/BufferAndInvertorRe01.png 800w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/a>Again, very similar to the previous post-resynthesis STG. But in this case, we can see that\u00a0<strong>b-<\/strong> is the first transition, instead of\u00a0<strong>a+<\/strong>.<\/p>\n<p><span style=\"text-decoration: underline\">No initial state concepts<\/span><\/p>\n<p>So, what if a set of concepts doesn&#8217;t contain any initial state concepts. In this case, the STG produced may still be a correct implementation of the system, but a user may wish to do some testing with options for initial states open.<\/p>\n<p>When this occurs, the algorithm has the option of adding some extra transitions to allow a user some options. So, for example, let&#8217;s define a handshake, but no initial states:<\/p>\n<p><strong>system = handshake(a,b)<\/strong><\/p>\n<p>In this case, we make no assumptions of initial states, but how does this affect the STG produced?<\/p>\n<p><a href=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/BufferInverterNoInit.png\"><img loading=\"lazy\" decoding=\"async\" class=\"alignnone wp-image-97 size-large\" src=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/BufferInverterNoInit-1024x628.png\" alt=\"BufferInverterNoInit\" width=\"474\" height=\"291\" srcset=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/BufferInverterNoInit-1024x628.png 1024w, https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/BufferInverterNoInit-300x184.png 300w, https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/files\/2015\/11\/BufferInverterNoInit.png 1400w\" sizes=\"auto, (max-width: 474px) 100vw, 474px\" \/><\/a><\/p>\n<p>The STG produced is very similar to the previous STG, the concepts used to describe which features initial states. In this case however, the places <strong>a_0<\/strong>, <strong>a_1<\/strong>, <strong>b_0<\/strong> and <strong>b_1 <\/strong>are all free from tokens. In order to select an initial state, the algorithm adds in an extra place and two extra transitions per signal, in order to allow\u00a0 a choice of each signal&#8217;s initial state.<\/p>\n<p>Using this example, when a user starts the simulation, the first transitions to be enabled will be the transitions either high or low from the initial state selections, allowing the user to select <strong>a- <\/strong>to set this signal to 0 initially, or <strong>a+ <\/strong>to set it to 1 initially, and this is the same as with signal <strong>b<\/strong>.<\/p>\n<p>After this choice is made, the initial state selection will no longer be usable until the simulation is started again. The user can test how the system runs using these initial states, and then\u00a0restart to test another combination of initial states. After the initial states have been selected, the user can either change this STG, removing the initial state selections and adding tokens into the correct place, or they can add the initial states to the list of concepts, and re-compose these for a new STG.<\/p>\n<blockquote><p><strong>DISCLAIMER<\/strong> &#8211;\u00a0An STG featuring initial state selection is not a correct STG, it violates properties of STGs which are necessary in order to be used with tools which perform useful functions like synthesis, for example.\u00a0Currently, this method of testing for initial states should be used only for simulation, to test how differing initial states can affect a system. Any future developments are made on how to include a choice \u00a0of initial state in a correct STG, a follow-up post will be made.<\/p><\/blockquote>\n<p><span style=\"text-decoration: underline\">Finally<\/span><\/p>\n<p>In this and the previous two posts, we have covered the basics of concepts, and the design process of various simple gates.\u00a0 Now we can move onto discussing some more complicated designs, and how we can use pre-existing concepts, and define new ones.<\/p>\n<p>The next blog post will be Concepts IV: A C-element. This will be the first in a set of posts describing some standard logic gates, and from this we will work up to some more complex examples, using\u00a0some of the previously described gates.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Initial States Now we have introduced a couple of simple gates, a buffer and an inverter, we should now discuss an important part of Signal Transition Graphs, and their implementation using Concepts. These are initial states. \u00a0 Initial states are used in Signal Transition Graphs to show what state a signal is in, high or &hellip; <a href=\"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/2015\/11\/24\/concepts-iii-initial-states\/\" class=\"more-link\">Continue reading <span class=\"screen-reader-text\">Concepts III: Initial States<\/span> <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":6010,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[3,5,2,7],"tags":[],"class_list":["post-92","post","type-post","status-publish","format-standard","hentry","category-asynchronous","category-buffer","category-concepts","category-inverter"],"_links":{"self":[{"href":"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/wp-json\/wp\/v2\/posts\/92","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/wp-json\/wp\/v2\/users\/6010"}],"replies":[{"embeddable":true,"href":"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/wp-json\/wp\/v2\/comments?post=92"}],"version-history":[{"count":10,"href":"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/wp-json\/wp\/v2\/posts\/92\/revisions"}],"predecessor-version":[{"id":102,"href":"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/wp-json\/wp\/v2\/posts\/92\/revisions\/102"}],"wp:attachment":[{"href":"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/wp-json\/wp\/v2\/media?parent=92"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/wp-json\/wp\/v2\/categories?post=92"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blogs.ncl.ac.uk\/jrbeaumont\/wp-json\/wp\/v2\/tags?post=92"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}