Replies: 6 comments 16 replies
-
Both of these things seem doable! I suspect the first issue is caused by old Yosys. If you're on Ubuntu/Linux, the yosys in the repositories is always way out of date. On mac, the homebrew version is more up to date. I would generally recommend building from source. Please update yosys and see what happens. I can make the yosys binary configurable in the script pretty easily, too, if you want to keep multiple versions of yosys around. RE: state names: this will take a bit more work on my side, because yeah, for some reason, yosys seemingly regressed in the way it handles state names. The state names are still in there, but they're defined at the end and not the beginning if I recall correctly. But I think I should be able to get that working. Array types should be doable! The thing that would really help me w/r/t array types is if you'd send me a btor file (you can just attach it here) as a test case. I've just never run into them. |
Beta Was this translation helpful? Give feedback.
-
Thanks Gus! Updating Yosys fixed that issue. I'll attach a btor file with an array sort soon! |
Beta Was this translation helpful? Give feedback.
-
Hey Gus, Here's a btor test case with array sorts.
If you're curious, it comes from the following verilog code I wrote which implements a tiny one-instruction set computer called a TOGA machine. Let me know if there's any way I can help out! Happy to contribute.
|
Beta Was this translation helpful? Give feedback.
-
This is awesome, Gus. After adding a couple missing operators like |
Beta Was this translation helpful? Give feedback.
-
Hey Gus, I've got another noob-ish question about using signals. (Sorry if this is necroposting.) I'm playing with the TOGA example I included here. When I run the
This seems reasonable, but I see that a lot of the state such as In some of the generated state code I see this relevant warning: |
Beta Was this translation helpful? Give feedback.
-
hey Zach, sorry, I have had a crazy week (and it won't stop til the weekend
is done). I want to unblock you on this ASAP, I'm hoping I get to do it on
my flights this weekend, but it may not be until next week!!
…On Sun, Jan 8, 2023, 5:24 PM zsisco ***@***.***> wrote:
Not sure if this is helpful, but I also wrote a "reference" implementation
in Racket directly, using the signal construct:
(define (toga-ref clk instruction)
(let* ([merged-state (merge-state (list clk instruction))]
[old-clk (if (hash-has-key? merged-state 'clk)
(hash-ref merged-state 'clk)
(bv 0 1))]
[current-clk (signal-value clk)]
[clock-ticked (rising-edge old-clk current-clk)]
[old-pc (if (hash-has-key? merged-state 'pc)
(hash-ref merged-state 'pc)
(bv 0 4))]
[a-addr (extract 3 0 (signal-value instruction))]
[b-addr (extract 7 4 (signal-value instruction))]
[a-bit (vector-ref-bv (hash-ref merged-state 'dm) a-addr)]
[a-toggle (bvnot a-bit)]
[target (if (bvzero? a-toggle) (bvadd1 old-pc) b-addr)]
[new-pc (if clock-ticked
target
old-pc)]
[write-dm (if clock-ticked
(begin
(vector-set!-bv
(hash-ref merged-state 'dm)
a-addr
a-toggle)
(hash-ref merged-state 'dm))
(hash-ref merged-state 'dm))]
[out-next-pc (signal target
(hash 'clk current-clk
'pc new-pc
'dm write-dm))])
out-next-pc))
(define (rising-edge old current)
(and (bvzero? old) (not (bvzero? current))))
A quick test with concrete values makes me think this is correct, but I
haven't yet been able to verify it against TOGA semantics expressed as
bitvector formula. Something like this:
(define (toga-semantics state inst pc dm)
(let* ([a (extract 3 0 inst)]
[b (extract 7 4 inst)]
[a-bit (vector-ref-bv dm a)]
[a! (bvnot a-bit)])
(begin
;; if data at a is 0 after toggling,
;; update pc to pc + 1
;; else if it is 1
;; update pc to b
(assert (bveq (hash-ref state 'pc)
(if (bvzero? a!) (bvadd1 pc) b)))
;; dm[a] is updated to ~dm[a]
(assert (bveq (vector-ref-bv (hash-ref state 'dm) a)
a!)))))
—
Reply to this email directly, view it on GitHub
<#138 (reply in thread)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAJFZANN5TGMWRJH2HS3IE3WRNSGDANCNFSM6AAAAAAQOSUI44>
.
You are receiving this because you commented.Message ID:
***@***.***>
|
Beta Was this translation helpful? Give feedback.
-
I've been playing with the scripts in
/bin
for converting Verilog->BTOR->Racket and had some questions with the BTOR format. (Aside: I really appreciate the effort you put into making those scripts!! 🙏)I noticed when I emit BTOR from Yosys,
state
expressions have 2 arguments: one for sort and one for state id. For example:state 3 pc
However, when I look at
/racket/btor.rkt
and the examples in the repo, I only see the one argument for the sort. Like this:where I would have expected something like this:
Because of this difference, I got stuck on the BTOR->Racket step because the match would fail. I couldn't find much documentation on the BTOR format online... I wonder if I'm using an old/different version of Yosys (using v0.9)?
One of the reasons I'm curious about this is because I'm trying to use the Verilog->Racket scripts on a small single-stage RISC-V processor: NERV. It would actually be quite beneficial to know, for instance, that a particular state element has id
pc
to be able to track the values of different components in the microarchitecture.This point brings to mind another question about array sorts. Designs like the RISC-V processor I'm looking at have a register file, which in BTOR turns into an array sort like this:
Has there been any discussion on supporting array sorts? It seems like these could be supported by creating vectors of signals addressed by something like
vector-ref-bv
. I understand if these haven't come up yet because of the particular benchmarks you're focusing on don't use them, but was just curious and wanted to start a discussion around this area. Thanks!Beta Was this translation helpful? Give feedback.
All reactions