search

tomstorey / discrete-nor-logic-clock

Design files for a clock built out of nothing but discrete transistor NOR logic
https://ornotblog.blogspot.com
1 stars 1 forks source link

Simulate/verify designs - alternative to logic.ly? #4

Open meisl opened 7 years ago

meisl commented 7 years ago

I have optimized the 7-seg decoders following this workflow:

Now my questions are: 1) Are you OK with OpenOffice, and with keeping the spreadsheets in the repo? 2) logic.ly is nice for quickly trying out small things, and has nice visuals. However, to be honest, I don't think it's worth its current price. Particularly it cannot (AFAIK) a) automate the verification b) be used with a textual representation of the design, which, in turn, would enable true working-together on designs (including using the benefits of git) What else can be used?

As for 2) I am envisioning a text file that describes a particular circuit. This text can be written by hand or produced from formulas in a spreadsheet. It can also be interpreted, or evaluated to produce a mapping from input combinations to output combinations. This evaluation would ideally be possible within a spreadsheet.

Well, I've been thinking of (and already working on) writing my own - it's all Booleans anyways, right? You might already have spotted those "µ A -B C -D" labels in my screenshots. My short-list of implementation languages was

Well, I went with the third option because I really want to use it in the spreadsheets. ...And I kind of regret it now. There ought to be a way to use javascript for OpenOffice macros but I just couldn't get it to work, it's (Java) package-hell. The thing is that you really need a parser so you can use mentioned concise lambda-like expression rather than a notation like "NOR(...)"; in addition you need to be able to define intermediate signals (ie. introduce shortcuts/abbreviations). I'm convinced that without that anything beyond trivial becomes unwieldy.

Now, BASIC is really, REALLY bad! But hey, that's kinda in the spirit - "from grounds up"... Additionlly, I seem to have gone in a particularly unfortunate direction with my implementation, ie unsuited for BASIC. I'll try to push it further a little bit more but I might have to start over.

What do you think?

meisl commented 7 years ago

p.s.: to further motivate my point - which is to emphasize the necessity of being able to easily, and safely, work on/experiment with designs - here are some figures of mentioned optimizations: image

p.p.s.: now you know what I meant by "too technical" ;) But that's not to say that this whole issue can't make it into a future blog post, maybe, sometime...

tomstorey commented 7 years ago

Might have to have a guest contributor to the blog. :-D

I havent got around to fully digesting your first comment, started a new job today, so all brain cycle credits used for today. Will try to come back with a response some time this week.

meisl commented 7 years ago

Oh... :D

Re the job: Congratulations!

Re guest contribution: not really sure about that, but definitely taking it as a compliment :D

Re digesting my overly lengthy issue: no worries, I'll be occupied with other stuff until the weekend, too. But the gist of it is rather simple:

tomstorey commented 7 years ago

No problems with storing spreadsheets in the repo. They would be design files after all so i think that would be totally appropriate.

And re making a parser, that would be cool. I'm sure others could find it useful, too. Logicly isn't the best software out there, but it's helping me verify my designs so it has been worth it to me. If there was something better I'd probably use that instead. The desktop version is slightly better because you can save your work and come back to it. Perhaps it'll be a better proposition once everything is available in one hit, you can download the trial and check out all out in one go. Bad timing in that respect right now i guess, given the infancy of the project. :-)

I will also be uploading schematics in future posts. You can't "run" them to observe their behaviour or interact with them, but they are an alternative to logicly I guess. I'll upload those as both EAGLE schematic files and PDF exports for those who don't use EAGLE. If there's sufficient interest I'll look at other formats or software packages too.

Basically, and knowing logicly isn't the answer to everything, it's at least a start getting my designs and theory out there in some way. :)

meisl commented 7 years ago

Ok, so I take it that we're settled on OpenOffice, right?

I'll address verification/logic.ly/EAGLE later. Just now let me express something general. Plz don't be put off if it sounds too harsh at first sight. It is by no means meant as an offense, just a strong believe of mine, formed by bad experience.

Generally: I think it's important to settle on ONE way of how things are done, NOT trying to "please all" by providing a lot of "flavours". What is "just another flavour" vs "a different thing" is of course TBD; eg. providing (pictures of) schematics alongside to what these are derived from is legitimate and even necessary, IMHO. Ideally, however, this one way is easily accessible to as many ppl as possible. "Easily" means two things here: one is about cost: cheap, at best for free. The other is about the effort of "getting it going": at best it'd be no more than a click in your browser. Another thing is consistency. You MUST NOT have MASTER inconsistent! You SHOULD have any other branch consistent at any time! Seriously. So the more variants you introduce - particularly of derived stuff - the more hassle you'll have.

tomstorey commented 7 years ago

OpenOffice/LibreOffice is fine, its widely available.

A thought, have you looked at scripts in Google sheets? I believe they are written in more of a JavaScript kind of language. So that would cover the whole "runs in a browser" thing.

Point taken about creating too many variants. It was more of an "if" situation. I wont be going out of my way to create more formats if there isnt sufficient demand to justify it. EAGLE has a free option, but I know there are plenty of people who dont use it, and others that dont want to. So if it was going to be beneficial to a portion of the community then some other format would be looked at - as reproducing some of the schematics from the PDF would be a little time consuming (Im up to 160ish gates on one particular board at the moment).

meisl commented 7 years ago

Google sheet scripts: good idea, will have a look. But I have to say: if we can't put those into the repo, ie only have them in Google's "cloud" then I'd opt against them.

EAGLE: free (feature-limited, not time-limited like logic.ly) and PDF export is a pro. Haven't used it myself, though. And I'm afraid I cannot afford to delve into that right now - at least not without a strong hint that it'd also be useful for verification. However, if you want to make schematics with it - and are willing to make sure they're always in sync with whatever else is there - then fine. Just saying that this keeping-in-sync can very quickly get VERY tedious and error-prone. So better be cautious.

logic.ly: does have its advantages, particularly the free online trial served as an easy entry for myself. But given the time-limitation and no easy export of schematics, it's now not a serious option anymore.

hand-grown NOR-parser: I did push it a bit, and I think I made progress. Don't ask what it took (at least not here)... It's still not presentable but I'm pretty sure to be able to show something that adds value in a spreadsheet in a week's time or so.

meisl commented 7 years ago

Well, maybe a bit of notice is appropriate:

I still can't present something as of now. However, of course - if you like - you can always watch me making ever so small steps on my fork. So: I went for doing a parser/interpreter - functional-style - in OOBasic. Which turned out hard as f**k, ie way harder than I had guessed. But I've committed myself to finishing it nevertheless. And I will. As said, I'm viewing it kinda in the same spirit as building a clock only from mosfets.

As for Google sheet scripts: haven't checked that out yet, and I won't until I have at least a proof-of-concept of the OOBasic stuff. When that happens, however, I definitely will. And if that then turns viable I'm pretty confident to be able to apply some of what I've learned/done by then to it.

Anyhow, all I can really say is plz bear with me; and ask for some patience :)

tomstorey commented 7 years ago

Thats ok, Im not holding you to anything.

I'll be interested to see what you come up with for your own project though, do let me know if you start a blog or anything to cover it, I'll certainly follow along. :-)

meisl commented 7 years ago

Cool, thx :) This whole simulation problem might indeed be worth blogging about,. Interestingly, since I began by writing a parser I started to think about it more and more as a problem of computation, ie. view a circuit as a program. Now, turns out there are really nice correspondences:

So clearly for the third kind, simply "executing the program" won't work, at least as a method of analysis. For this an extra level of abstraction is needed. That is, we have to reason about all possible paths of execution at once, without actually making them explicit. This may sound like impossible on first encounter but it is feasable, and actually done regularly in the semiconductor industry.

I'm not sure how far I will be able to go with this. It is exciting though, so I will pursue it further, and maybe write about my endeavours. I'll definitely cover the first of above pts in OOBasic, but to be honest: a serious verification tool indeed has to cover all three. Let's see...

tomstorey commented 7 years ago

Youre thinking about this at a whole 'nother level to me. Or maybe I'm not thinking about it far enough. 😄

meisl commented 7 years ago

Hmm, so what I said sounded like voodoo? It is not, btw. But maybe I should take that even more as an incentive to write something up? Unfortunately the time I can invest is rather limited. I don't think I'll put up a blog like yours anytime soon; rather start with some .md files in github, and count on a bit of feedback from your side. What'd you think about that?

meisl commented 7 years ago

Hey, I've been able to push it quite a bit. I had put myself as a goal to be able to parse a rather complex language, particularly one including recursive rules with balanced parentheses (ie beyond regular expressions). What I chose was a language of ML-like, or Haskell-like types. Don't worry if you don't really know what that means, just take it as non-trivial.

And I did it!

Having gone so far, I think I should definitely write about it. But right now I just want to give you a short glimpse. Don't worry, only (comparatively) simple things for starters, not the whole types language.

Let's start with parsing binary digits. That is: read a "0" or a "1" character from an input string and output a 0/1 integer if there is a "0" or "1" - or report an error otherwise. Of course I wrote a toString function that turns a parser into a string so you can see what you've built. Here's what comes out if you write =TParser_toString("pBinDigit") into a cell of the spreadsheet:

BinDigit_1 where
BinDigit_1 ::= (str '0') >>= \_.return 0
             | (str '1') >>= \_.return 1

This is the actual output of the toString function unedited, with all the nice indentation and such! Now, what does it say? First of all, you might recognize an EBNF-like notation: the ::= declares a rule and the | marks a choice between alternatives. The alternatives themselves consume a "0" or a "1", and if that succeeded pass it on (that is what the >>= does). The character passed on is then actually ignored, and a fixed constant, 0 or 1 - but now as an integer - is returned. The overall outcome is either 0, 1, or failure to parse.

Ok, easy enough to do decimal digits 0..9: TParser_toString("pDecDigit") yields

DecDigit_1 where
DecDigit_1 ::= BinDigit_2
             | (str '2') >>= \_.return 2
             | (str '3') >>= \_.return 3
             | (str '4') >>= \_.return 4
             | (str '5') >>= \_.return 5
             | (str '6') >>= \_.return 6
             | (str '7') >>= \_.return 7
             | (str '8') >>= \_.return 8
             | (str '9') >>= \_.return 9
BinDigit_2 ::= (str '0') >>= \_.return 0
             | (str '1') >>= \_.return 1

As you can see I have re-used pBinDigit, rather than repeating it. Again, this is the actual output. It did the reference to BinDigit_2 and the explicit restating of it automatically!

Now we're ready for some serious business: even though still a regular language, let's go for parsing hexadecimal literals - of the form "0xDeAdBeEf0123" - into integers. This is more than just collecting the digits (0..9, A..F or a..f this time), rather we need to interpret a whole sequence of them as a written-down number in base 16, with the most significant digit to the left. There are more concise (and more efficient) ways of getting the digits than the above patterns, and I've combined one of those ways with successively building up the resulting integer value. The following example contains a lot more to say about, but for now I'll just show it off: =TParser_toString("pHexLit") yields

HexLit_1 where
HexLit_1 ::= (do  _ <- (str '0x')
                 a0 <- HexNum_2
              return a0
             )
HexNum_2 ::= (do a0 <- HexDigit_3+
              return ((foldl1 \a0.add ((mul 16) a0)) a0)
             )
HexDigit_3 ::= item >>= (ite (inRange 48 57) 
                             \a0.pReturn ((add -48) a0) 
                             (ite (inRange 65 70) 
                                  \a0.pReturn ((add -55) a0)
                                  (ite (inRange 97 102)
                                       \a0.pReturn ((add -87) a0)
                                       (fstArg fail)
                             )    )
                        ) ° asc

Isn't that amzaing? Well, the BASIC code for building such a parser is of course not nearly as pretty. However, with a bit of squinting, it is still recognizable. Here's the BASIC code for the HexNum rule, to give just one example:

Function pHexNum()
    Static result As Object
    If isNull(result) Then
        result = fixIndirection(pInd("HexNum"), _
            pSeq(Array( _
                    pMany1(pHexDigit) _
                ), foldl1(compose(add, mul(16))) _
            ) _
        )
    End If
    pHexNum = result
End Function

Especially noteworthy is the expression foldl1(compose(add, mul(16))). This is partial function application together with function composition - all valid BASIC! Well, there's of course a bit of additionally machinery behind the scenes to make this work...

p.s: in the HexLit example I did edit the HexDigit rule, the actual toString fn basically puts all on one line.

tomstorey commented 7 years ago

I think this is going beyond my understanding lol.

A more detailed write up might help to make it more clear. :)

meisl commented 7 years ago

Sure, and sorry. The above isn't really an explanation. I'm going to write one, but I need to get clear about what to put in, as well as what to leave out.

So the goal is to write expressions (or formulas in spreadsheet-talk) that describe our circuits, and have them evaluated/analyzed/tested. I would like to discuss with you how those expression should look like, and what we want their expressive power to be. For this we will need so-called grammars in EBNF, Extended Backus-Naur Form and so-called regular expressions. Then I have added to this is my own invention of a LISP, or ML or Haskell-like syntax, but I think I should not bother you with that too much. For example the >>= ("bind") operator is a bit hard to get used to, but I know how to do without it entirely.

So my questions for you are:

Again, I will try my best to avoid any theory, and even leave out the parts of the formalisms that aren't actually used.

meisl commented 7 years ago

Well, to make things more concrete I started writing Formal-languages.md. It's unfinished, just want to get things started.

Tried to make it understandable with no prerequisites whatsoever, and focus on motivating every concept introduced. The downside of this approach, however, is that it tends to make it rather lengthy. But that of course very much depends on the reader's expectations...

So I'd like you to have a look and am hoping for some feedback. Particularly on the style. Should I be more concise, not quite as wordy? Or maybe there are already points where I'm making too big a step?

tomstorey commented 7 years ago

I like the style, short, but not too short - just to the point.

I guess its early days, so Im still trying to figure out exactly how it applies to the designs so far, but I guess youre still building up to that. :)

meisl commented 7 years ago

Thanks, Tom! That does help me a lot. And yes, I am building up. So I'll continue like this and let you know once I got more.

meisl commented 7 years ago

Hey there! I've added quite big an example of an actually useful grammar - effectively doubling the overall size! I am hoping that it gives a bit of a hint where all this is going (although I'm still not quite there). Also, due to your commenting "short, but not too short", this time I did NOT try as hard as before to keep things short. It'd be really great if you could tell me whether or not I went overboard in this regard.

In the p.s. below I've added an "executive summary", just so you can see what to expect before actually reading it. Also: you might want to look at the diff rather than the whole document, so you don't have to search for what's new. Simply click here.

Hint: once there, click on "Display the rich diff", like so:

display-the-rich-diff

What I've planned next is to write a working parser for mentioned example, so one can experiment with it by putting formulas into spreadsheet cells.

p.s.: Summary of changes:

tomstorey commented 7 years ago

Not sure what your background is, but that is starting to border on rocket surgery to me.

A demo to play with might be better, I tend to think I work more practically than theoretically. :-D

meisl commented 7 years ago

"rocket surgery" :-O At least you don't call it "voodoo"...

But first: in the meantime I have pretty much completed it, by adding associativity, multiplicity & char classes, and for the grand finale of this part: a grammar of grammars. See here for those changes. You might also want to try out https://stackedit.io/editor for reading: just replace the default document by copying/pasting the raw .md source. It has very nice rendering, plus auto-generated table of contents.

Then: thanks for the feedback. I'm sorry if it's kinda overwhelming. I really tried my best to require no pre-requisites. Similarly, I'm trying to omit as much - particularly related theory - as I can. Ok, there are one or two proofs in the text that could go into footnotes. Otherwise you'd have to tell me at which point (roughly) things are getting "blurry" for you. I still hope though to have sparked some interest. It's really only beginnings. There's a lot more exciting stuff...

Right now I am working on making the examples "playable". I'm thinking of (you) putting sample text into cells of prepared "tutorial" sheets, and see some output in other cells. That of course is quite a bit more limited than eg. writing your own BASIC, using the macros already there. Which of course you're always free to try as well ;-)

tomstorey commented 7 years ago

This might be a case of needing to read it a couple more times. Ive just been over it again and its making a bit more sense.

There is quite a lot to take in, and its a brand new concept to me, so I need to put in some time to really understand it before I can (hopefully) give some meaningful feedback.

meisl commented 7 years ago

It is indeed quite dense, thank you for taking the time. There's an updated version where I polished a few things plus made one correction. It's about the relation of a grammar to its rules. My apologies should this have confused you (rightly so, in case).

incorrect:

Actually, both grammars and rules are nothing but definitions: of languages (sets) and parts of languages (subsets of languages), respectively.

correct:

Actually, both grammars and rules are nothing but definitions. A grammar is a definition of a language (set). And so is each rule from that grammar, where the set defined by the rule contains only words (character sequences) that are sub-words (parts of other sequences) of words defined by the whole grammar.

Note that this is different from set-inclusion: the language defined by the grammar is NOT (necessarily) the union of the languages defined by the rules. Rather it's a relation between words in respective languages, and that is the relation of sequence ("grammar-word") to sub-sequence ("rule-word").

p.s.: One more thing: I'm taking your feedback as "a bit too dense". So eg I inserted an extra section to introduce "nonterminals", rather than just one sentence; like that.