BTOR format: state and array sorts

[zsisco]

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:

[`("state" ,sort-id-str)

where I would have expected something like this:

[`("state" ,sort-id-str ,state-id-str)

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:

3 sort bitvec 32
10 sort bitvec 5
11 sort array 10 3
12 state 11 regfile

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!

[gussmith23]

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.

[zsisco]

Thanks Gus! Updating Yosys fixed that issue.

I'll attach a btor file with an array sort soon!

[zsisco]

Hey Gus,

Here's a btor test case with array sorts.

; BTOR description generated by Yosys 0.21+10 (git sha1 558018522, clang 14.0.0 -fPIC -Os) for module toga.
1 sort bitvec 1
2 input 1 clk ; toga.v:1.19-1.22
3 input 1 reset ; toga.v:1.30-1.35
4 sort bitvec 4
5 state 4
6 state 4
7 const 1 1
8 state 1
9 init 1 8 7
10 sort bitvec 2
11 concat 10 2 8
12 const 10 10
13 eq 1 11 12
14 ite 4 13 6 5
15 output 14 pc ; toga.v:1.50-1.52
16 sort bitvec 8
17 sort array 4 16
18 state 17 pm
19 read 16 18 14
20 slice 4 19 3 0
21 uext 4 20 0 a_addr ; toga.v:25.11-25.17
22 sort array 4 1
23 state 22 dm
24 state 4
25 state 1
26 const 1 0
27 state 1
28 state 1
29 init 1 28 7
30 concat 10 2 28
31 eq 1 30 12
32 ite 1 31 27 26
33 read 1 23 24
34 not 1 32
35 and 1 33 34
36 and 1 25 32
37 or 1 36 35
38 write 22 23 24 37
39 redor 1 32
40 ite 22 39 38 23
41 read 1 40 20
42 next 22 23 40
43 not 1 41
44 uext 1 43 0 a_toggle ; toga.v:27.6-27.14
45 slice 4 19 7 4
46 uext 4 45 0 b_addr ; toga.v:26.11-26.17
47 uext 16 19 0 instruction ; toga.v:24.11-24.22
48 next 4 5 14
49 uext 4 7 3
50 add 4 14 49
51 ite 4 41 50 45
52 const 4 0000
53 ite 4 3 52 51
54 next 4 6 53
55 next 1 8 2
56 next 4 24 20
57 next 1 25 43
58 next 1 27 7
59 next 1 28 2
60 next 17 18 18 pm ; toga.v:20.10-20.12
; end of yosys output

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.

module toga(input clk, input reset, output [3:0] pc);

/***********************************
TOGA is a one instruction set computer.
TOGA a b: toggle a and branch to b

dm[a] <- ~dm[a] ;
if dm[a] then
  pc <- b
else pc <- pc + 1

dm : BV(4) -> BV(1)
pm : BV(4) -> BV(8)
pc : BV(4)
************************************/

// registers
reg[3:0] pc;

// program and data memories
reg[7:0] pm[15:0];
reg dm[15:0];

// intermediate wires
wire[7:0] instruction;
wire[3:0] a_addr;
wire[3:0] b_addr;
wire a_toggle;

// instruction fetch
assign instruction = pm[pc];

// decode
assign a_addr = instruction[3:0];
assign b_addr = instruction[7:4];

// toggle a
assign a_toggle = ~dm[a_addr];

// write toggled bit back to memory
always @(posedge clk) begin
  dm[a_addr] <= a_toggle;
end

// update pc
always @(posedge clk) begin
  if (reset)
    pc <= 0;
  else if (a_toggle == 1)
    pc <= b_addr;
  else
    pc <= pc + 1;
end
endmodule

[gussmith23]

See #144 , which should give you at least some of the functionality you're looking for!

[zsisco]

This is awesome, Gus. After adding a couple missing operators like ugte, sll, etc., I was able to even translate a tiny RISC-V CPU to the Racket DSL. Cool!

[zsisco]

A couple of my next steps here are:

• Run one of the tiny translated CPU designs with the symbolic interpreter
• Figure out how to pull out some pieces of state (like pc, mem, etc.)
• And then make some Rosette assumptions/assertions about those pieces of state
• And try solving for something? Like an unknown control signal as input

We'll see... I may be following up with some more questions

[gussmith23]

After ASPLOS deadline, I'd love to meet and talk about how you're using it!

It would also be really cool to see if we could get Rosette to write programs for the processor, once it gets the imported semantics. My entire thesis is to basically show that formal models of hardware (i.e. a Verilog implementation of a processor) can be automatically converted into compilers -- this would be a very literal realization of that idea!

[zsisco]

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 toga function that's returned after converting the design from BTOR->Racket, I get some output like this:

(hash 'pc (signal (bv #x0 4) (hash 'dm (vector (bv #b0 1) (bv #b0 1) (bv #b0 1) (bv #b0 1) (bv #b0 1) (bv #b0 1) (bv #b0 1) (bv #b0 1) (bv #b0 1) (bv #b0 1) (bv #b0 1) (bv #b0 1) (bv #b0 1) (bv #b0 1) (bv #b0 1) (bv #b0 1)) 'pm (vector (bv #x00 8) (bv #x00 8) (bv #x00 8) (bv #x00 8) (bv #x00 8) (bv #x00 8) (bv #x00 8) (bv #x00 8) (bv #x00 8) (bv #x00 8) (bv #x00 8) (bv #x00 8) (bv #x00 8) (bv #x00 8) (bv #x00 8) (bv #x00 8)) 'state24 (bv #x0 4) 'state25 (bv #b1 1) 'state27 (bv #b1 1) 'state28 clk$symbolic-constant 'state5 (bv #x0 4) 'state6 (bv #x0 4) 'state8 clk$symbolic-constant)))

This seems reasonable, but I see that a lot of the state such as pc and dm are concrete bitvectors. Ideally, I want these registers (and arrays of registers, even) to be symbolic values, so that I can formulate a Rosette synthesize query that quantifies over all possible values for pc.

In some of the generated state code I see this relevant warning: "Getting default value of 0 for bitvector, this may be a bad idea!"
Do you think it's a matter of changing this to return a fresh symbolic value instead of 0? Or might there be more to it than that? Thanks!

[gussmith23]

Okay! Luckily, I think it's a dead-simple fix. Unfortunately, it's once again caused by poor documentation and no runtime type-checking 😆

Basically, evaluating toga returns a hashmap prev of signal names (e.g. 'next_pc) to signal-typed values. When you call toga for the second time, you attempt to create a signal which contains the state from prev:

  (toga #:clk (signal (bv 1 1) prev) ; attempting to construct a new signal with the state from prev
	#:reset (bv->signal (bv 0 1))
	#:instruction (bv->signal inst)))

However, you can't just pass prev in to the signal constructor. prev is not a signal; it's a hashmap of symbols to signals. You need to get one of the signals out of prev, and then get the new state out of that signal. (All signals in prev will have the same new state; lots of unnecessary duplication, I know!) So the correct code is:

(let* ([prev (toga #:clk (signal (bv 0 1)
                                 (hash 'pc pc 'dm dm)))])
  (println prev)
  (toga #:clk (bv->signal (bv 1 1) (hash-ref prev 'next_pc))))

Note the use of bv->signal and not signal. bv->signal optionally takes a signal as its second argument, and pulls the state hashmap out of that signal. You could also do something like (signal (bv 1 1) (signal-state (hash-ref prev 'next_pc))))).

Sorry, again, this stuff is just not documented. At the very least, there should be runtime type checks on this stuff.

[zsisco]

Gus, thanks so much, this helps a lot!

With this, I'm now able to verify the "reference" TOGA function against the TOGA semantics, but not the BTOR-translated TOGA function. That could very well be a bug in my Verilog code! So, still poking around.

Thanks for this, I'm glad it was just a type mix up.

[gussmith23]

Great! Out of curiosity, can you explain the difference between the "TOGA semantics" and the "BTOR-translated TOGA function" here?

LMK what else I can help with!

[zsisco]

Sure, sorry, I was posting a lot of representations of very similar things here.

So the TOGA semantics is the architecture-level spec for the tiny processor. It asserts how the ISA-level state (PC, data memory) should be updated after executing an instruction.

The BTOR-translated TOGA function is my Verilog implementation using your signal construct. I want to symbolically evaluate this for one clock cycle (given an arbitrary instruction as input), and check against the semantics that the ISA-level state (PC, data memory) is updated according to spec.

(I also posted a reference implementation written directly in Racket to check against the BTOR-translated implementation.)

Does that clear things up?

[gussmith23]

That clears things up! Let me know if you think it's a bug in the Verilog-to-Racket importer -- I can take a crack at finding the bug.

[gussmith23]

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: ***@***.***>

[zsisco]

No worries, Gus! It's no rush. Thanks for the update 👍